[Git][ghc/ghc][wip/cfuneqcan-refactor] Add Detail (7) to the Note
Richard Eisenberg
gitlab at gitlab.haskell.org
Tue Oct 27 21:13:18 UTC 2020
Richard Eisenberg pushed to branch wip/cfuneqcan-refactor at Glasgow Haskell Compiler / GHC
Commits:
c1caf60c by Richard Eisenberg at 2020-10-27T17:13:03-04:00
Add Detail (7) to the Note
- - - - -
4 changed files:
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Utils/TcType.hs
- testsuite/tests/typecheck/should_fail/ContextStack2.hs
- + testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
Changes:
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -2303,6 +2303,7 @@ canEqCanLHSFinish ev eq_rel swapped lhs rhs
| OtherCIS <- status
, Given <- ctEvFlavour ev
, TyVarLHS lhs_tv <- lhs
+ , not (isCycleBreakerTyVar lhs_tv) -- See Detail (7) of Note
, NomEq <- eq_rel
-> do { traceTcS "canEqCanLHSFinish breaking a cycle" (ppr lhs $$ ppr rhs)
; new_rhs <- breakTyVarCycle (ctEvLoc ev) rhs
@@ -2711,6 +2712,41 @@ Details:
breaker variables are all zonked away by the time we examine the
evidence.
+ (7) We don't wish to apply this magic to CycleBreakerTvs themselves.
+ Consider this, from typecheck/should_compile/ContextStack2:
+
+ type instance TF (a, b) = (TF a, TF b)
+ t :: (a ~ TF (a, Int)) => ...
+
+ [G] a ~ TF (a, Int)
+
+ The RHS reduces, so we get
+
+ [G] a ~ (TF a, TF Int)
+
+ We then break cycles, to get
+
+ [G] g1 :: a ~ (cbv1, cbv2)
+ [G] g2 :: TF a ~ cbv1
+ [G] g3 :: TF Int ~ cbv2
+
+ g1 gets added to the inert set, as written. But then g2 becomes
+ the work item. g1 rewrites g2 to become
+
+ [G] TF (cbv1, cbv2) ~ cbv1
+
+ which then uses the type instance to become
+
+ [G] (TF cbv1, TF cbv2) ~ cbv1
+
+ which looks remarkably like the Given we started with. If left
+ unchecked, this will end up breaking cycles again, looping ad
+ infinitum (and resulting in a context-stack reduction error,
+ not an outright loop). The solution is easy: don't break cycles
+ if the var is already a CycleBreakerTv. This makes sense, because
+ we only want to break cycles for user-written loopy Givens, and
+ a CycleBreakerTv certainly isn't user-written.
+
-}
{-
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -39,7 +39,7 @@ module GHC.Tc.Utils.TcType (
MetaDetails(Flexi, Indirect), MetaInfo(..),
isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isMetaTyVarTy, isTyVarTy,
tcIsTcTyVar, isTyVarTyVar, isOverlappableTyVar, isTyConableTyVar,
- isAmbiguousTyVar, metaTyVarRef, metaTyVarInfo,
+ isAmbiguousTyVar, isCycleBreakerTyVar, metaTyVarRef, metaTyVarInfo,
isFlexi, isIndirect, isRuntimeUnkSkol,
metaTyVarTcLevel, setMetaTyVarTcLevel, metaTyVarTcLevel_maybe,
isTouchableMetaTyVar,
@@ -1019,7 +1019,7 @@ isImmutableTyVar :: TyVar -> Bool
isImmutableTyVar tv = isSkolemTyVar tv
isTyConableTyVar, isSkolemTyVar, isOverlappableTyVar,
- isMetaTyVar, isAmbiguousTyVar :: TcTyVar -> Bool
+ isMetaTyVar, isAmbiguousTyVar, isCycleBreakerTyVar :: TcTyVar -> Bool
isTyConableTyVar tv
-- True of a meta-type variable that can be filled in
@@ -1064,6 +1064,14 @@ isAmbiguousTyVar tv
_ -> False
| otherwise = False
+isCycleBreakerTyVar tv
+ | isTyVar tv -- See Note [Coercion variables in free variable lists]
+ , MetaTv { mtv_info = CycleBreakerTv } <- tcTyVarDetails tv
+ = True
+
+ | otherwise
+ = False
+
isMetaTyVarTy :: TcType -> Bool
isMetaTyVarTy (TyVarTy tv) = isMetaTyVar tv
isMetaTyVarTy _ = False
=====================================
testsuite/tests/typecheck/should_fail/ContextStack2.hs
=====================================
@@ -12,11 +12,11 @@ type instance TF (a,b) = (TF a, TF b)
t :: (a ~ TF (a,Int)) => Int
t = undefined
-{- a ~ TF (a,Int)
+{- a ~ TF (a,Int)
~ (TF a, TF Int)
~ (TF (TF (a,Int)), TF Int)
~ (TF (TF a, TF Int), TF Int)
- ~ ((TF (TF a), TF (TF Int)), TF Int)
+ ~ ((TF (TF a), TF (TF Int)), TF Int)
fsk ~ a
@@ -28,7 +28,7 @@ t = undefined
a ~ (TF a, TF Int)
(flatten rhs)
a ~ (fsk1, TF Int)
-(wk) TF a ~ fsk1
+(wk) TF a ~ fsk1
--> (rewrite inert)
@@ -43,7 +43,7 @@ t = undefined
* TF (fsk1, fsk2) ~ fsk1
(wk) TF Tnt ~ fsk2
--->
+-->
fsk ~ (fsk1, TF Int)
a ~ (fsk1, TF Int)
@@ -51,7 +51,7 @@ t = undefined
(flatten rhs)
fsk1 ~ (fsk3, TF fsk2)
-
+
(wk) TF Int ~ fsk2
TF fsk1 ~ fsk3
-}
=====================================
testsuite/tests/typecheck/should_fail/GivenForallLoop.stderr
=====================================
@@ -0,0 +1,20 @@
+
+GivenForallLoop.hs:8:11: error:
+ • Could not deduce: a ~ b
+ from the context: a ~ (forall b1. F a b1)
+ bound by the type signature for:
+ loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+ at GivenForallLoop.hs:7:1-42
+ ‘a’ is a rigid type variable bound by
+ the type signature for:
+ loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+ at GivenForallLoop.hs:7:1-42
+ ‘b’ is a rigid type variable bound by
+ the type signature for:
+ loopy :: forall a b. (a ~ (forall b1. F a b1)) => a -> b
+ at GivenForallLoop.hs:7:1-42
+ • In the expression: x
+ In an equation for ‘loopy’: loopy x = x
+ • Relevant bindings include
+ x :: a (bound at GivenForallLoop.hs:8:7)
+ loopy :: a -> b (bound at GivenForallLoop.hs:8:1)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c1caf60c9e2eff957f0ebf3136194da1c36361e8
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c1caf60c9e2eff957f0ebf3136194da1c36361e8
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/20201027/ab02b198/attachment-0001.html>
More information about the ghc-commits
mailing list