Look both ways when looking for quantified equalities

When looking up (t1 ~# t2) in the quantified constraints,
check both orientations.  Forgetting this led to #23333.

6 files changed, 78 insertions, 52 deletions

diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs
index a9b6f00464..c0f7dc7a49 100644
--- a/compiler/GHC/Tc/Solver/Dict.hs
+++ b/compiler/GHC/Tc/Solver/Dict.hs
@@ -69,7 +69,7 @@ doTopReactDict inerts work_item@(CDictCan { cc_ev = ev, cc_class = cls
                OneInst { cir_what = what }
                   -> do { insertSafeOverlapFailureTcS what work_item
                         ; addSolvedDict what ev cls xis
-                        ; chooseInstance work_item lkup_res }
+                        ; chooseInstance ev lkup_res }
                _  -> -- NoInstance or NotSure
                      -- We didn't solve it; so try functional dependencies
                      tryFunDeps work_item }
@@ -113,28 +113,24 @@ tryLastResortProhibitedSuperclass inerts
 tryLastResortProhibitedSuperclass _ work_item
   = continueWith work_item
 
-chooseInstance :: Ct -> ClsInstResult -> TcS (StopOrContinue Ct)
+chooseInstance :: CtEvidence -> ClsInstResult -> TcS (StopOrContinue Ct)
 chooseInstance work_item
                (OneInst { cir_new_theta   = theta
                         , cir_what        = what
                         , cir_mk_ev       = mk_ev
                         , cir_coherence   = coherence })
-  = do { traceTcS "doTopReact/found instance for" $ ppr ev
+  = do { traceTcS "doTopReact/found instance for" $ ppr work_item
        ; deeper_loc <- checkInstanceOK loc what pred
        ; checkReductionDepth deeper_loc pred
-       ; evb <- getTcEvBindsVar
-       ; if isCoEvBindsVar evb
-         then continueWith work_item
-                  -- See Note [Instances in no-evidence implications]
-         else
-           do { evc_vars <- mapM (newWanted deeper_loc (ctRewriters work_item)) theta
-              ; setEvBindIfWanted ev coherence (mk_ev (map getEvExpr evc_vars))
-              ; emitWorkNC (freshGoals evc_vars)
-              ; stopWith ev "Dict/Top (solved wanted)" }}
+       ; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar)
+                    (ppr work_item)
+       ; evc_vars <- mapM (newWanted deeper_loc (ctEvRewriters work_item)) theta
+       ; setEvBindIfWanted work_item coherence (mk_ev (map getEvExpr evc_vars))
+       ; emitWorkNC (freshGoals evc_vars)
+       ; stopWith work_item "Dict/Top (solved wanted)" }
   where
-     ev         = ctEvidence work_item
-     pred       = ctEvPred ev
-     loc        = ctEvLoc ev
+     pred = ctEvPred work_item
+     loc  = ctEvLoc work_item
 
 chooseInstance work_item lookup_res
   = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
@@ -160,27 +156,6 @@ checkInstanceOK loc what pred
        | otherwise
        = loc
 
-{- Note [Instances in no-evidence implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-In #15290 we had
-  [G] forall p q. Coercible p q => Coercible (m p) (m q))
-  [W] forall <no-ev> a. m (Int, IntStateT m a)
-                          ~R#
-                        m (Int, StateT Int m a)
-
-The Given is an ordinary quantified constraint; the Wanted is an implication
-equality that arises from
-  [W] (forall a. t1) ~R# (forall a. t2)
-
-But because the (t1 ~R# t2) is solved "inside a type" (under that forall a)
-we can't generate any term evidence.  So we can't actually use that
-lovely quantified constraint.  Alas!
-
-This test arranges to ignore the instance-based solution under these
-(rare) circumstances.   It's sad, but I  really don't see what else we can do.
--}
-
-
 matchClassInst :: DynFlags -> InertSet
                -> Class -> [Type]
                -> CtLoc -> TcS ClsInstResult
diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index 82185535d2..bb2a9aa6d5 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/compiler/GHC/Tc/Solver/Equality.hs
@@ -2672,23 +2672,45 @@ finishEqCt work_item@(EqCt { eq_lhs = lhs, eq_rhs = rhs, eq_eq_rel = eq_rel })
 final_qci_check :: Ct -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct)
 -- The "final QCI check" checks to see if we have
 --    [W] t1 ~# t2
--- and a Given quantified contraint like (forall a b. blah => a :~: b)
+-- and a Given quantified contraint like (forall a b. blah => a ~ b)
 -- Why?  See Note [Looking up primitive equalities in quantified constraints]
 final_qci_check work_ct eq_rel lhs rhs
-  | isWanted ev
-  , Just (cls, tys) <- boxEqPred eq_rel lhs rhs
-  = do { res <- matchLocalInst (mkClassPred cls tys) loc
-       ; case res of
-           OneInst { cir_mk_ev = mk_ev }
-             -> chooseInstance work_ct
-                    (res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
-           _ -> continueWith work_ct }
-
-  | otherwise
-  = continueWith work_ct
+  = do { ev_binds_var <- getTcEvBindsVar
+       ; ics <- getInertCans
+       ; if isWanted ev                       -- Never look up Givens in quantified constraints
+         && not (null (inert_insts ics))      -- Shortcut common case
+         && not (isCoEvBindsVar ev_binds_var) -- See Note [Instances in no-evidence implications]
+         then try_for_qci
+         else continueWith work_ct }
   where
     ev  = ctEvidence work_ct
     loc = ctEvLoc ev
+    role = eqRelRole eq_rel
+
+    try_for_qci  -- First try looking for (lhs ~ rhs)
+       | Just (cls, tys) <- boxEqPred eq_rel lhs rhs
+       = do { res <- matchLocalInst (mkClassPred cls tys) loc
+            ; traceTcS "final_qci_check:1" (ppr (mkClassPred cls tys))
+            ; case res of
+                OneInst { cir_mk_ev = mk_ev }
+                  -> chooseInstance ev (res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
+                _ -> try_swapping }
+       | otherwise
+       = continueWith work_ct
+
+    try_swapping  -- Now try looking for (rhs ~ lhs)  (see #23333)
+       | Just (cls, tys) <- boxEqPred eq_rel rhs lhs
+       = do { res <- matchLocalInst (mkClassPred cls tys) loc
+            ; traceTcS "final_qci_check:2" (ppr (mkClassPred cls tys))
+            ; case res of
+                OneInst { cir_mk_ev = mk_ev }
+                  -> do { ev' <- rewriteEqEvidence emptyRewriterSet ev IsSwapped
+                                      (mkReflRedn role rhs) (mkReflRedn role lhs)
+                        ; chooseInstance ev' (res { cir_mk_ev = mk_eq_ev cls tys mk_ev }) }
+                _ -> do { traceTcS "final_qci_check:3" (ppr work_ct)
+                        ; continueWith work_ct }}
+       | otherwise
+       = continueWith work_ct
 
     mk_eq_ev cls tys mk_ev evs
       | sc_id : rest <- classSCSelIds cls  -- Just one superclass for this
@@ -2697,6 +2719,27 @@ final_qci_check work_ct eq_rel lhs rhs
           ev       -> pprPanic "mk_eq_ev" (ppr ev)
       | otherwise = pprPanic "finishEqCt" (ppr work_ct)
 
+{- Note [Instances in no-evidence implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In #15290 we had
+  [G] forall p q. Coercible p q => Coercible (m p) (m q))   -- Quantified
+  [W] forall <no-ev> a. m (Int, IntStateT m a)
+                          ~R#
+                        m (Int, StateT Int m a)
+
+The Given is an ordinary quantified constraint; the Wanted is an implication
+equality that arises from
+  [W] (forall a. t1) ~R# (forall a. t2)
+
+But because the (t1 ~R# t2) is solved "inside a type" (under that forall a)
+we can't generate any term evidence.  So we can't actually use that
+lovely quantified constraint.  Alas!
+
+This test arranges to ignore the instance-based solution under these
+(rare) circumstances.   It's sad, but I  really don't see what else we can do.
+-}
+
+
 {-
 **********************************************************************
 *                                                                    *
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index ce34045f70..e40478279c 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -1264,7 +1264,7 @@ doTopReactOther work_item
   | otherwise
   = do { res <- matchLocalInst pred loc
        ; case res of
-           OneInst {} -> chooseInstance work_item res
+           OneInst {} -> chooseInstance ev res
            _          -> continueWith work_item }
 
   where
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 512ee5c437..bfbba18a11 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -1736,8 +1736,8 @@ just a coercion? i.e. evTermCoercion_maybe returns Nothing.
 Consider [G] forall a. blah => a ~ T
          [W] S ~# T
 
-Then doTopReactEqPred carefully looks up the (boxed) constraint (S ~
-T) in the quantified constraints, and wraps the (boxed) evidence it
+Then doTopReactEqPred carefully looks up the (boxed) constraint (S ~ T)
+in the quantified constraints, and wraps the (boxed) evidence it
 gets back in an eq_sel to extract the unboxed (S ~# T).  We can't put
 that term into a coercion, so we add a value binding
     h = eq_sel (...)
diff --git a/testsuite/tests/quantified-constraints/T23333.hs b/testsuite/tests/quantified-constraints/T23333.hs
new file mode 100644
index 0000000000..c8fde6d608
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T23333.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+module T23333 where
+
+foo1 :: (forall y. Bool ~ y) => z -> Bool
+foo1 x = not x
+
+foo2 :: (forall y. y ~ Bool) => z -> Bool
+foo2 x = not x
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index d3bfe6e07e..bea86c5e8f 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -41,4 +41,4 @@ test('T22216d', normal, compile, [''])
 test('T22216e', normal, compile, [''])
 test('T22223', normal, compile, [''])
 test('T19690', normal, compile_fail, [''])
-
+test('T23333', normal, compile, [''])