[Git][ghc/ghc][master] Look both ways when looking for quantified equalities
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Thu May 11 08:11:49 UTC 2023
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
40c7daed by Simon Peyton Jones at 2023-05-11T04:11:30-04:00
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 changed files:
- compiler/GHC/Tc/Solver/Dict.hs
- compiler/GHC/Tc/Solver/Equality.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/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
=====================================
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.
+-}
+
+
{-
**********************************************************************
* *
=====================================
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
=====================================
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 (...)
=====================================
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
=====================================
@@ -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, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/40c7daed0c971e58e86a8189f82f72e9213af8b6
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/40c7daed0c971e58e86a8189f82f72e9213af8b6
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/20230511/7017c767/attachment-0001.html>
More information about the ghc-commits
mailing list