[Git][ghc/ghc][wip/ghc-9.6-backports] Look both ways when looking for quantified equalities
Zubin (@wz1000)
gitlab at gitlab.haskell.org
Wed Sep 13 12:23:38 UTC 2023
Zubin pushed to branch wip/ghc-9.6-backports at Glasgow Haskell Compiler / GHC
Commits:
f939a7f7 by Simon Peyton Jones at 2023-09-13T17:53:09+05:30
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.
(cherry picked from commit 40c7daed0c971e58e86a8189f82f72e9213af8b6)
- - - - -
5 changed files:
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Interact.hs
- compiler/GHC/Tc/Solver/Monad.hs
- + testsuite/tests/quantified-constraints/T23333.hs
- testsuite/tests/quantified-constraints/all.T
Changes:
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -8,6 +8,7 @@ module GHC.Tc.Solver.Canonical(
unifyWanted,
makeSuperClasses,
StopOrContinue(..), stopWith, continueWith, andWhenContinue,
+ rewriteEqEvidence,
solveCallStack -- For GHC.Tc.Solver
) where
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -35,6 +35,7 @@ import GHC.Core.Type as Type
import GHC.Core.InstEnv ( DFunInstType )
import GHC.Core.Class
import GHC.Core.TyCon
+import GHC.Core.Reduction
import GHC.Core.Predicate
import GHC.Core.Coercion
import GHC.Core.FamInstEnv
@@ -2010,7 +2011,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
@@ -2025,22 +2026,45 @@ doTopReactOther work_item
********************************************************************-}
doTopReactEqPred :: Ct -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct)
-doTopReactEqPred work_item eq_rel t1 t2
+doTopReactEqPred work_item eq_rel lhs rhs
-- See Note [Looking up primitive equalities in quantified constraints]
- | Just (cls, tys) <- boxEqPred eq_rel t1 t2
- = do { res <- matchLocalInst (mkClassPred cls tys) loc
- ; case res of
- OneInst { cir_mk_ev = mk_ev }
- -> chooseInstance work_item
- (res { cir_mk_ev = mk_eq_ev cls tys mk_ev })
- _ -> continueWith work_item }
-
- | otherwise
- = continueWith work_item
+ = 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_item }
where
ev = ctEvidence work_item
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_item
+
+ 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_item)
+ ; continueWith work_item }}
+ | otherwise
+ = continueWith work_item
+
mk_eq_ev cls tys mk_ev evs
= case (mk_ev evs) of
EvExpr e -> EvExpr (Var sc_id `mkTyApps` tys `App` e)
@@ -2279,7 +2303,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
@@ -2312,27 +2336,23 @@ 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 })
- = 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 (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 (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)
=====================================
compiler/GHC/Tc/Solver/Monad.hs
=====================================
@@ -1723,8 +1723,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 (...)
=====================================
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
=====================================
testsuite/tests/quantified-constraints/all.T
=====================================
@@ -43,3 +43,4 @@ test('T22223', normal, compile, [''])
test('T19690', normal, compile_fail, [''])
test('T23143', normal, compile, [''])
test('T23323', normal, compile, [''])
+test('T23333', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f939a7f7031695843aaff33039449b5b1509ffb5
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/f939a7f7031695843aaff33039449b5b1509ffb5
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20230913/4f68b035/attachment-0001.html>
More information about the ghc-commits
mailing list