diff options
author | Simon Peyton Jones <simon.peytonjones@gmail.com> | 2023-05-05 13:18:28 +0100 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2023-05-11 04:11:30 -0400 |
commit | 40c7daed0c971e58e86a8189f82f72e9213af8b6 (patch) | |
tree | 86626dbe410954fb6ead7ed1bde80a612d4d287e /compiler/GHC | |
parent | 29be39ba3f187279b19cf451f2d8f58822edab4f (diff) | |
download | haskell-40c7daed0c971e58e86a8189f82f72e9213af8b6.tar.gz |
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.
Diffstat (limited to 'compiler/GHC')
-rw-r--r-- | compiler/GHC/Tc/Solver/Dict.hs | 47 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Equality.hs | 67 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Interact.hs | 2 | ||||
-rw-r--r-- | compiler/GHC/Tc/Solver/Monad.hs | 4 |
4 files changed, 69 insertions, 51 deletions
diff --git a/compiler/GHC/Tc/Solver/Dict.hs b/compiler/GHC/Tc/Solver/Dict.hs index 75635a4c89..6893322f9a 100644 --- a/compiler/GHC/Tc/Solver/Dict.hs +++ b/compiler/GHC/Tc/Solver/Dict.hs @@ -67,7 +67,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 with -- the instance environment @@ -100,28 +100,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) @@ -147,27 +143,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 2a76792790..ed4cd500aa 100644 --- a/compiler/GHC/Tc/Solver/Equality.hs +++ b/compiler/GHC/Tc/Solver/Equality.hs @@ -2647,23 +2647,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 @@ -2672,6 +2694,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 a46bccac79..809c71100b 100644 --- a/compiler/GHC/Tc/Solver/Interact.hs +++ b/compiler/GHC/Tc/Solver/Interact.hs @@ -1303,7 +1303,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 bd2e48682f..befc9e212e 100644 --- a/compiler/GHC/Tc/Solver/Monad.hs +++ b/compiler/GHC/Tc/Solver/Monad.hs @@ -1713,8 +1713,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 (...) |