[Git][ghc/ghc][wip/T22924] Furher work
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Thu Feb 9 09:41:50 UTC 2023
Simon Peyton Jones pushed to branch wip/T22924 at Glasgow Haskell Compiler / GHC
Commits:
e93b07a5 by Simon Peyton Jones at 2023-02-09T09:40:27+00:00
Furher work
* Restore noGivenNewtypeReprEqs
* Revert most of !9623
* Lots of documentation
* New test cases T22924a, T22924b for recursive newtypes
(One of these is regressed by !9623 which is why we are reverting it)
- - - - -
8 changed files:
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/Rewrite.hs
- + testsuite/tests/typecheck/should_fail/T22924a.hs
- + testsuite/tests/typecheck/should_fail/T22924a.stderr
- + testsuite/tests/typecheck/should_fail/T22924b.hs
- + testsuite/tests/typecheck/should_fail/T22924b.stderr
- testsuite/tests/typecheck/should_fail/all.T
Changes:
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -1974,7 +1974,7 @@ isInjectiveTyCon :: TyCon -> Role -> Bool
isInjectiveTyCon (TyCon { tyConDetails = details }) role
= go details role
where
- go _ Phantom = True -- Vacuously; (t1 ~P t2) holes for all t1, t2!
+ go _ Phantom = True -- Vacuously; (t1 ~P t2) holds for all t1, t2!
go (AlgTyCon {}) Nominal = True
go (AlgTyCon {algTcRhs = rhs}) Representational
= isGenInjAlgRhs rhs
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1084,7 +1084,7 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
-- Decompose type constructor applications
-- NB: we have expanded type synonyms already
-can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
+can_eq_nc' _rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
| Just (tc1, tys1) <- tcSplitTyConApp_maybe ty1
, Just (tc2, tys2) <- tcSplitTyConApp_maybe ty2
-- we want to catch e.g. Maybe Int ~ (Int -> Int) here for better
@@ -1092,7 +1092,7 @@ can_eq_nc' rewritten _rdr_env _envs ev eq_rel ty1 _ ty2 _
-- hence no direct match on TyConApp
, not (isTypeFamilyTyCon tc1)
, not (isTypeFamilyTyCon tc2)
- = canTyConApp rewritten ev eq_rel tc1 tys1 tc2 tys2
+ = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
s1@(ForAllTy (Bndr _ vis1) _) _
@@ -1114,8 +1114,12 @@ can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
-------------------
-- No similarity in type structure detected. Rewrite and try again.
-can_eq_nc' False _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
- = rewrite_and_try_again ev eq_rel ps_ty1 ps_ty2
+can_eq_nc' False rdr_env envs ev eq_rel _ ps_ty1 _ ps_ty2
+ = -- Rewrite the two types and try again
+ do { (redn1@(Reduction _ xi1), rewriters1) <- rewrite ev ps_ty1
+ ; (redn2@(Reduction _ xi2), rewriters2) <- rewrite ev ps_ty2
+ ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
+ ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
----------------------------
-- Look for a canonical LHS. See Note [Canonical LHS].
@@ -1153,15 +1157,6 @@ can_eq_nc' True _rdr_env _envs ev eq_rel _ ps_ty1 _ ps_ty2
-- No need to call canEqFailure/canEqHardFailure because they
-- rewrite, and the types involved here are already rewritten
--- Rewrite the two types and try again
-rewrite_and_try_again :: CtEvidence -> EqRel -> TcType -> TcType -> TcS (StopOrContinue Ct)
-rewrite_and_try_again ev eq_rel ty1 ty2
- = do { (redn1@(Reduction _ xi1), rewriters1) <- rewrite ev ty1
- ; (redn2@(Reduction _ xi2), rewriters2) <- rewrite ev ty2
- ; new_ev <- rewriteEqEvidence (rewriters1 S.<> rewriters2) ev NotSwapped redn1 redn2
- ; rdr_env <- getGlobalRdrEnvTcS
- ; envs <- getFamInstEnvs
- ; can_eq_nc' True rdr_env envs new_ev eq_rel xi1 xi1 xi2 xi2 }
{- Note [Unsolved equalities]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1407,62 +1402,40 @@ which is easier to satisfy.
Conclusion: we must unwrap newtypes before decomposing them. This happens
in `can_eq_newtype_nc`
-But even this is challenging. Here are two cases to consider:
+We did flirt with making the /rewriter/ expand newtypes, rather than
+doing it in `can_eq_newtype_nc`. But with recursive newtypes we want
+to be super-careful about expanding!
-Case 1 (extremely contrived):
+ newtype A = MkA [A] -- Recursive!
- newtype Age = MkAge Int
- [G] IO s ~ IO t -- where s,t ane not Age,Int
- [W] w1 :: IO Age ~R# IO Int
+ f :: A -> [A]
+ f = coerce
-Case 2:
+We have [W] A ~R# [A]. If we rewrite [A], it'll expand to
+ [[[[[...]]]]]
+and blow the reduction stack. See Note [Newtypes can blow the stack]
+in GHC.Tc.Solver.Rewrite. But if we expand only the /top level/ of
+both sides, we get
+ [W] [A] ~R# [A]
+which we can, just, solve by reflexivity.
- newtype A = MkA [A]
- [W] A ~R# [A]
+So we simply unwrap, on-demand, at top level, in `can_eq_newtype_nc`.
-For Case 1, recall that IO is an abstract newtype. Then read Note
-[Decomposing newtype equalities]. According to that Note, we should not
-decompose w1, because we have an Irred Given that stops decomposition.
-Yet we still want to solve the wanted! We can do so by unwrapping the
-(non-abstract) Age newtype underneath the IO, giving
- [W] w2 :: IO Int ~R# IO Int
- w1 = (IO unwrap-Age ; w2)
-where unwrap-Age :: Age ~R# Int. Now we case solve w2 by reflexivity;
-see Note [Eager reflexivity check].
+This is all very delicate. There is a real risk of a loop in the type checker
+with recursive newtypes -- but I think we're doomed to do *something*
+delicate, as we're really trying to solve for equirecursive type
+equality. Bottom line for users: recursive newtypes are dangerous. See also
+Section 5.3.1 and 5.3.4 of "Safe Zero-cost Coercions for Haskell" (JFP 2016).
-Conclusion: unwrap newtypes (deeply, inside types) in the rewriter:
-specifically in GHC.Tc.Solver.Rewrite.rewrite_newtype_app.
+See also Note [Decomposing newtype equalities].
-Yet for Case 2, deep rewriting would be a disaster: we would loop.
- [W] A ~R# [A] ---> {unwrap}
- [W] [A] ~R# [[A]]
- ---> {decompose}
- [W] A ~R# [A]
+--- Historical side note ---
-In this case, we just want to unwrap newtypes /at the top level/, allowing us
-to succeed via Note [Eager reflexivity check]:
- [W] A ~R# [A] ---> {unwrap at top level only}
- [W] [A] ~R# [A]
- ---> {reflexivity} success
-
-Conclusion: to satisfy Case 1 and Case 2, we unwrap
-* /both/ at top level, in can_eq_nc'
-* /and/ deeply, in the rewriter, rewrite_newtype_app
-
-The former unwraps outer newtypes (when the data constructor is in scope).
-The latter unwraps deeply -- but it won't be invoked in Case 2, when we can
-recognize an equality between the types [A] and [A] before rewriting
-deeply.
-
-This "before" business is delicate -- there is still a real risk of a loop
-in the type checker with recursive newtypes -- but I think we're doomed to do
-*something* delicate, as we're really trying to solve for equirecursive
-type equality. Bottom line for users: recursive newtypes are dangerous.
-See also Section 5.3.1 and 5.3.4 of
-"Safe Zero-cost Coercions for Haskell" (JFP 2016).
-
-Another approach -- which we ultimately decided against -- is described in
-Note [Decomposing newtypes a bit more aggressively].
+We flirted with doing /both/ unwrap-at-top-level /and/ rewrite-deeply;
+see #22519. But that didn't work: see discussion in #22924. Specifically
+we got a loop with a minor variation:
+ f2 :: a -> [A]
+ f2 = coerce
Note [Eager reflexivity check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1492,6 +1465,24 @@ we do a reflexivity check.
(This would be sound in the nominal case, but unnecessary, and I [Richard
E.] am worried that it would slow down the common case.)
+
+ Note [Newtypes can blow the stack]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+
+ newtype X = MkX (Int -> X)
+ newtype Y = MkY (Int -> Y)
+
+and now wish to prove
+
+ [W] X ~R Y
+
+This Wanted will loop, expanding out the newtypes ever deeper looking
+for a solid match or a solid discrepancy. Indeed, there is something
+appropriate to this looping, because X and Y *do* have the same representation,
+in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
+coercion will ever witness it. This loop won't actually cause GHC to hang,
+though, because we check our depth in `can_eq_newtype_nc`.
-}
------------------------
@@ -1598,8 +1589,7 @@ canEqCast rewritten ev eq_rel swapped ty1 co1 ty2 ps_ty2
role = eqRelRole eq_rel
------------------------
-canTyConApp :: Bool -- True <=> the types have been rewritten
- -> CtEvidence -> EqRel
+canTyConApp :: CtEvidence -> EqRel
-> TyCon -> [TcType]
-> TyCon -> [TcType]
-> TcS (StopOrContinue Ct)
@@ -1607,17 +1597,13 @@ canTyConApp :: Bool -- True <=> the types have been rewritten
-- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
-- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family
-- But they can be data families.
-canTyConApp rewritten ev eq_rel tc1 tys1 tc2 tys2
+canTyConApp ev eq_rel tc1 tys1 tc2 tys2
| tc1 == tc2
, tys1 `equalLength` tys2
= do { inerts <- getTcSInerts
; if can_decompose inerts
then canDecomposableTyConAppOK ev eq_rel tc1 tys1 tys2
- else if rewritten
- then canEqFailure ev eq_rel ty1 ty2
- else rewrite_and_try_again ev eq_rel ty1 ty2 }
- -- Why rewrite and try again? See Case 1
- -- of Note [Unwrap newtypes first]
+ else canEqFailure ev eq_rel ty1 ty2 }
-- See Note [Skolem abstract data] in GHC.Core.Tycon
| tyConSkolem tc1 || tyConSkolem tc2
@@ -1650,8 +1636,7 @@ canTyConApp rewritten ev eq_rel tc1 tys1 tc2 tys2
-- Moreover isInjectiveTyCon is True for Representational
-- for algebraic data types. So we are down to newtypes
-- and data families.
- ctEvFlavour ev == Wanted
- -- COMMENTING OUT; see !22924: && noGivenNewtypeReprEqs tc1 inerts)
+ ctEvFlavour ev == Wanted && noGivenNewtypeReprEqs tc1 inerts)
-- See Note [Decomposing newtype equalities] (EX2)
{-
@@ -1842,11 +1827,11 @@ For a Wanted with r=R, since newtypes are not injective at representational
role, decomposition is sound, but we may lose completeness. Nevertheless,
if the newtype is abstraction (so can't be unwrapped) we can only solve
the equality by (a) using a Given or (b) decomposition. If (a) is impossible
-(e.g. no Givens) then (b) is safe.
+(e.g. no Givens) then (b) is safe albeit potentially incomplete.
-Conclusion: decompose newtypes (at role R) only if there are no usable Givens.
+There are two ways in which decomposing (N ty1) ~r (N ty2) could be incomplete:
-* Incompleteness example (EX1)
+* Incompleteness example (EX1): unwrap first
newtype Nt a = MkNt (Id a)
type family Id a where Id a = a
@@ -1860,34 +1845,45 @@ Conclusion: decompose newtypes (at role R) only if there are no usable Givens.
them. This is done in can_eq_nc'. Of course, we can't unwrap if the data
constructor isn't in scope. See Note [Unwrap newtypes first].
-* Incompleteness example (EX2)
+* Incompleteness example (EX2): available Givens
newtype Nt a = Mk Bool -- NB: a is not used in the RHS,
type role Nt representational -- but the user gives it an R role anyway
- If we have [W] Nt alpha ~R Nt beta, we *don't* want to decompose to
- [W] alpha ~R beta, because it's possible that alpha and beta aren't
- representationally equal. And maybe there is a Given (Nt t1 ~R Nt t2),
- just waiting to be used, if we figure out (elsewhere) that alpha:=t1
- and beta:=t2. This is somewhat similar to the question of overlapping
- Givens for class constraints: see Note [Instance and Given overlap]
- in GHC.Tc.Solver.Interact.
+ [G] Nt t1 ~R Nt t2
+ [W] Nt alpha ~R Nt beta
+
+ We *don't* want to decompose to [W] alpha ~R beta, because it's possible
+ that alpha and beta aren't representationally equal. And if we figure
+ out (elsewhere) that alpha:=t1 and beta:=t2, we can solve the Wanted
+ from the Given. This is somewhat similar to the question of overlapping
+ Givens for class constraints: see Note [Instance and Given overlap] in
+ GHC.Tc.Solver.Interact.
Conclusion: don't decompose [W] N s ~R N t, if there are any Given
equalities that could later solve it.
- But what precisely does "any Given equalities that could later solve it" mean?
+ But what precisely does it mean to say "any Given equalities that could
+ later solve it"?
- It must be a Given constraint that could turn into N s ~ N t.
- That could /in principle/ include [G] (a b) ~ (c d), or even just [G] c.
- But since the free vars of a Given are skolems, or at least untouchable
- unification variables, it is extremely unlikely that such Givens
- will "turn into" [G] N s ~ N t.
-
- Moreover, in #22908 we had
+ In #22924 we had
[G] f a ~R# a [W] Const (f a) a ~R# Const a a
- where Const is a newtype. If we decomposed the newtype, we could solve.
- Not-decomposing on the grounds that (f a ~R# a) might turn into
- (Const (f a) a ~R# Const a a) seems a bit silly.
+ where Const is an abstract newtype. If we decomposed the newtype, we
+ could solve. Not-decomposing on the grounds that (f a ~R# a) might turn
+ into (Const (f a) a ~R# Const a a) seems a bit silly.
+
+ In #22331 we had
+ [G] N a ~R# N b [W] N b ~R# N a
+ (where N is abstract so we can't unwrap). Here we really /don't/ want to
+ decompose, because the /only/ way to solve the Wanted is from that Given
+ (with a Sym).
+
+ In #22519 we had
+ [G] a <= b [W] IO Age ~R# IO Int
+ (where IO is abstract so we can't unwrap, and newtype Age = Int). Here
+ we /must/ decompose. (Side note: We flirted with deep-rewriting of
+ newtypes (see discussion on #22519 and !9623) but that turned out not to
+ solve #22924, and also makes type inference loop more often on recursive
+ newtypes.)
The currently-implemented compromise is this:
@@ -1896,19 +1892,15 @@ Conclusion: decompose newtypes (at role R) only if there are no usable Givens.
that is, a Given Irred equality with both sides headed with N.
See the call to noGivenNewtypeReprEqs in canTyConApp.
- This is still incomplete but only just, and there is no perfect answer.
- See #22331 and #22908.
+ This is not perfect. In principle a Given like [G] (a b) ~ (c d), or
+ even just [G] c, could later turn into N s ~ N t. But since the free
+ vars of a Given are skolems, or at least untouchable unification
+ variables, this is extremely unlikely to happen.
- We only look at Irreds. There could, just, be a CDictCan with some
+ Another worry: there could, just, be a CDictCan with some
un-expanded equality superclasses; but only in some very obscure
recursive-superclass situations.
- Now suppose we have [G] IO t1 ~R# IO t2, [W] IO Age ~R# IO Int,
- where t1, t2 are not actually Age, Int. Then noGiveNewtypeReprEqs
- will stop us decomposing the Wanted (IO is a newtype). But we
- can /still/ win by unwrapping the newtype Age in the rewriter:
- see Note [Unwrap newtypes first]
-
Yet another approach (!) is desribed in
Note [Decomposing newtypes a bit more aggressively].
=====================================
compiler/GHC/Tc/Solver/Rewrite.hs
=====================================
@@ -42,7 +42,6 @@ import GHC.Builtin.Types (tYPETyCon)
import Data.List ( find )
import GHC.Data.List.Infinite (Infinite)
import qualified GHC.Data.List.Infinite as Inf
-import GHC.Tc.Instance.Family (tcTopNormaliseNewTypeTF_maybe)
{-
************************************************************************
@@ -225,10 +224,10 @@ rewrite ev ty
; return result }
-- | See Note [Rewriting]
--- This variant of 'rewrite' rewrites w.r.t. nominal equality only,
--- as this is better than full rewriting for error messages. Specifically,
--- we want to avoid unwrapping newtypes, as doing so can end up causing
--- an otherwise-unnecessary stack overflow.
+-- `rewriteForErrors` is a variant of 'rewrite' that rewrites
+-- w.r.t. nominal equality only, as this is better than full rewriting
+-- for error messages. (This was important when we flirted with rewriting
+-- newtypes but perhaps less so now.)
rewriteForErrors :: CtEvidence -> TcType
-> TcS (Reduction, RewriterSet)
rewriteForErrors ev ty
@@ -504,22 +503,9 @@ rewrite_one ty@(TyConApp tc tys)
| isTypeFamilyTyCon tc
= rewrite_fam_app tc tys
- | otherwise
- = do { eq_rel <- getEqRel
- ; if eq_rel == ReprEq
-
- then -- Rewriting w.r.t. representational equality requires
- -- unwrapping newtypes; see GHC.Tc.Solver.Canonical.
- -- Note [Unwrap newtypes first]
- -- NB: try rewrite_newtype_app even when tc isn't a newtype;
- -- the allows the possibility of having a newtype buried under
- -- a synonym. Needed for e.g. T12067.
- rewrite_newtype_app ty
-
- else -- For * a normal data type application
- -- * data family application
- -- we just recursively rewrite the arguments.
- rewrite_ty_con_app tc tys }
+ | otherwise -- We just recursively rewrite the arguments.
+ -- See Note [Do not rewrite newtypes]
+ = rewrite_ty_con_app tc tys
rewrite_one (FunTy { ft_af = vis, ft_mult = mult, ft_arg = ty1, ft_res = ty2 })
= do { arg_redn <- rewrite_one ty1
@@ -678,42 +664,12 @@ rewrite_vector ki roles tys
fvs = tyCoVarsOfType ki
{-# INLINE rewrite_vector #-}
--- Rewrite a (potential) newtype application
--- Precondition: the ambient EqRel is ReprEq
--- Precondition: the type is a TyConApp
--- See Note [Newtypes can blow the stack]
-rewrite_newtype_app :: TcType -> RewriteM Reduction
-rewrite_newtype_app ty@(TyConApp tc tys)
- = do { rdr_env <- liftTcS getGlobalRdrEnvTcS
- ; tf_envs <- liftTcS getFamInstEnvs
- ; case (tcTopNormaliseNewTypeTF_maybe tf_envs rdr_env ty) of
- Nothing -> -- Non-newtype or abstract newtype
- rewrite_ty_con_app tc tys
-
- Just ((used_ctors, co), ty') -- co :: ty ~ ty'
- -> do { liftTcS $ recordUsedGREs used_ctors
- ; checkStackDepth ty
- ; rewrite_reduction (Reduction co ty') } }
-
-rewrite_newtype_app other_ty = pprPanic "rewrite_newtype_app" (ppr other_ty)
-
-{- Note [Newtypes can blow the stack]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have
-
- newtype X = MkX (Int -> X)
- newtype Y = MkY (Int -> Y)
-
-and now wish to prove
-
- [W] X ~R Y
-This Wanted will loop, expanding out the newtypes ever deeper looking
-for a solid match or a solid discrepancy. Indeed, there is something
-appropriate to this looping, because X and Y *do* have the same representation,
-in the limit -- they're both (Fix ((->) Int)). However, no finitely-sized
-coercion will ever witness it. This loop won't actually cause GHC to hang,
-though, because we check our depth when unwrapping newtypes.
+{- Note [Do not rewrite newtypes]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We flirted with unwrapping newtypes in the rewriter -- see GHC.Tc.Solver.Canonical
+Note [Unwrap newtypes first]. But that turned out to be a bad idea because
+of recursive newtypes, as that Note says. So be careful if you re-add it!
Note [Rewriting synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
testsuite/tests/typecheck/should_fail/T22924a.hs
=====================================
@@ -0,0 +1,9 @@
+module T22924a where
+
+import Data.Coerce
+
+newtype R = MkR [R]
+
+f :: a -> [R]
+-- Should give a civilised error
+f = coerce
=====================================
testsuite/tests/typecheck/should_fail/T22924a.stderr
=====================================
@@ -0,0 +1,11 @@
+
+T22924a.hs:9:5: error: [GHC-10283]
+ • Couldn't match representation of type ‘a’ with that of ‘[R]’
+ arising from a use of ‘coerce’
+ ‘a’ is a rigid type variable bound by
+ the type signature for:
+ f :: forall a. a -> [R]
+ at T22924a.hs:7:1-13
+ • In the expression: coerce
+ In an equation for ‘f’: f = coerce
+ • Relevant bindings include f :: a -> [R] (bound at T22924a.hs:9:1)
=====================================
testsuite/tests/typecheck/should_fail/T22924b.hs
=====================================
@@ -0,0 +1,10 @@
+module T22924b where
+
+import Data.Coerce
+
+newtype R = MkR [R]
+newtype S = MkS [S]
+
+f :: R -> S
+-- Blows the typechecker reduction stack
+f = coerce
=====================================
testsuite/tests/typecheck/should_fail/T22924b.stderr
=====================================
@@ -0,0 +1,10 @@
+
+T22924b.hs:10:5: error:
+ • Reduction stack overflow; size = 201
+ When simplifying the following type: R
+ Use -freduction-depth=0 to disable this check
+ (any upper bound you could choose might fail unpredictably with
+ minor updates to GHC, so disabling the check is recommended if
+ you're sure that type checking should terminate)
+ • In the expression: coerce
+ In an equation for ‘f’: f = coerce
=====================================
testsuite/tests/typecheck/should_fail/all.T
=====================================
@@ -667,3 +667,5 @@ test('T22570', normal, compile_fail, [''])
test('T22645', normal, compile_fail, [''])
test('T20666', normal, compile_fail, [''])
test('T20666a', normal, compile_fail, [''])
+test('T22924a', normal, compile_fail, [''])
+test('T22924b', normal, compile_fail, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e93b07a578adab9e6c8c7bb5cad1be4015733ef3
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e93b07a578adab9e6c8c7bb5cad1be4015733ef3
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/20230209/8b807b74/attachment-0001.html>
More information about the ghc-commits
mailing list