[Git][ghc/ghc][wip/T22491] 3 commits: Fix decomposition of TyConApps
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Mon Nov 28 16:29:04 UTC 2022
Simon Peyton Jones pushed to branch wip/T22491 at Glasgow Haskell Compiler / GHC
Commits:
d10dc6bd by Simon Peyton Jones at 2022-11-25T22:31:27+00:00
Fix decomposition of TyConApps
Ticket #22331 showed that we were being too eager to decompose
a Wanted TyConApp, leading to incompleteness in the solver.
To understand all this I ended up doing a substantial rewrite
of the old Note [Decomposing equalities], now reborn as
Note [Decomposing TyConApp equalities]. Plus rewrites of other
related Notes.
The actual fix is very minor and actually simplifies the code: in
`can_decompose` in `GHC.Tc.Solver.Canonical.canTyConApp`, we now call
`noMatchableIrreds`. A closely related refactor: we stop trying to
use the same "no matchable givens" function here as in
`matchClassInst`. Instead split into two much simpler functions.
- - - - -
2da5c38a by Will Hawkins at 2022-11-26T04:05:04-05:00
Redirect output of musttail attribute test
Compilation output from test for support of musttail attribute leaked to
the console.
- - - - -
1abeda0d by Simon Peyton Jones at 2022-11-28T16:30:39+00:00
Add a missing varToCoreExpr in etaBodyForJoinPoint
This subtle bug showed up when compiling a library with 9.4.
See #22491. The bug is present in master, but it is hard to
trigger; the new regression test T22491 fails in 9.4.
The fix was easy: just add a missing varToCoreExpr in
etaBodyForJoinPoint.
The fix is definitely right though!
I also did some other minor refatoring:
* Moved the preInlineUnconditionally test in simplExprF1 to
before the call to joinPointBinding_maybe, to avoid fruitless
eta-expansion.
* Added a boolean from_lam flag to simplNonRecE, to avoid two
fruitless tests, and commented it a bit better.
These refactorings seem to save 0.1% on compile-time allocation in
perf/compiler; with a max saving of 1.4% in T9961
Metric Decrease:
T9961
- - - - -
11 changed files:
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/TyCon.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/Solver/InertSet.hs
- compiler/GHC/Tc/Solver/Interact.hs
- m4/fp_musttail.m4
- + testsuite/tests/simplCore/should_compile/T22491.hs
- testsuite/tests/simplCore/should_compile/all.T
- + testsuite/tests/typecheck/should_compile/T22331.hs
- testsuite/tests/typecheck/should_compile/all.T
Changes:
=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -3103,9 +3103,13 @@ etaBodyForJoinPoint need_args body
| Just (tv, res_ty) <- splitForAllTyCoVar_maybe ty
, let (subst', tv') = substVarBndr subst tv
= go (n-1) res_ty subst' (tv' : rev_bs) (e `App` varToCoreExpr tv')
+ -- The varToCoreExpr is important: `tv` might be a coercion variable
+
| Just (_, mult, arg_ty, res_ty) <- splitFunTy_maybe ty
, let (subst', b) = freshEtaId n subst (Scaled mult arg_ty)
- = go (n-1) res_ty subst' (b : rev_bs) (e `App` Var b)
+ = go (n-1) res_ty subst' (b : rev_bs) (e `App` varToCoreExpr b)
+ -- The varToCoreExpr is important: `b` might be a coercion variable
+
| otherwise
= pprPanic "etaBodyForJoinPoint" $ int need_args $$
ppr body $$ ppr (exprType body)
=====================================
compiler/GHC/Core/Opt/Simplify/Iteration.hs
=====================================
@@ -1227,11 +1227,23 @@ simplExprF1 env (Let (NonRec bndr rhs) body) cont
do { ty' <- simplType env ty
; simplExprF (extendTvSubst env bndr ty') body cont }
+ | Just env' <- preInlineUnconditionally env NotTopLevel bndr rhs env
+ -- Because of the let-can-float invariant, it's ok to
+ -- inline freely, or to drop the binding if it is dead.
+ = do { tick (PreInlineUnconditionally bndr)
+ ; simplExprF env' body cont }
+
+ -- Now check for a join point. It's better to do the preInlineUnconditionally
+ -- test first, because joinPointBinding_maybe has to eta-expand, so a trivial
+ -- binding like { j = j2 |> co } would first be eta-expanded and then inlined
+ -- Better to test preInlineUnconditionally first.
| Just (bndr', rhs') <- joinPointBinding_maybe bndr rhs
- = {-#SCC "simplNonRecJoinPoint" #-} simplNonRecJoinPoint env bndr' rhs' body cont
+ = {-#SCC "simplNonRecJoinPoint" #-}
+ simplNonRecJoinPoint env bndr' rhs' body cont
| otherwise
- = {-#SCC "simplNonRecE" #-} simplNonRecE env bndr (rhs, env) body cont
+ = {-#SCC "simplNonRecE" #-}
+ simplNonRecE env False bndr (rhs, env) body cont
{- Note [Avoiding space leaks in OutType]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1680,12 +1692,12 @@ simpl_lam env bndr body (ApplyToVal { sc_arg = arg, sc_env = arg_se
, sc_cont = cont, sc_dup = dup })
| isSimplified dup -- Don't re-simplify if we've simplified it once
-- See Note [Avoiding exponential behaviour]
- = do { tick (BetaReduction bndr)
- ; completeBindX env bndr arg body cont }
+ = do { tick (BetaReduction bndr)
+ ; completeBindX env bndr arg body cont }
| otherwise -- See Note [Avoiding exponential behaviour]
- = do { tick (BetaReduction bndr)
- ; simplNonRecE env bndr (arg, arg_se) body cont }
+ = do { tick (BetaReduction bndr)
+ ; simplNonRecE env True bndr (arg, arg_se) body cont }
-- Discard a non-counting tick on a lambda. This may change the
-- cost attribution slightly (moving the allocation of the
@@ -1717,6 +1729,8 @@ simplLamBndrs env bndrs = mapAccumLM simplLamBndr env bndrs
------------------
simplNonRecE :: SimplEnv
+ -> Bool -- True <=> from a lambda
+ -- False <=> from a let
-> InId -- The binder, always an Id
-- Never a join point
-> (InExpr, SimplEnv) -- Rhs of binding (or arg of lambda)
@@ -1735,34 +1749,46 @@ simplNonRecE :: SimplEnv
-- It deals with strict bindings, via the StrictBind continuation,
-- which may abort the whole process.
--
--- The RHS may not satisfy the let-can-float invariant yet
+-- from_lam=False => the RHS satisfies the let-can-float invariant
+-- Otherwise it may or may not satisfy it.
-simplNonRecE env bndr (rhs, rhs_se) body cont
+simplNonRecE env from_lam bndr (rhs, rhs_se) body cont
= assert (isId bndr && not (isJoinId bndr) ) $
do { (env1, bndr1) <- simplNonRecBndr env bndr
; let needs_case_binding = needsCaseBinding (idType bndr1) rhs
-- See Note [Dark corner with representation polymorphism]
- ; if | not needs_case_binding
- , Just env' <- preInlineUnconditionally env NotTopLevel bndr rhs rhs_se ->
- do { tick (PreInlineUnconditionally bndr)
- ; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
- simplLam env' body cont }
-
+ -- If from_lam=False then needs_case_binding is False,
+ -- because the binding started as a let, which must
+ -- satisfy let-can-float
+
+ ; if | from_lam && not needs_case_binding
+ -- If not from_lam we are coming from a (NonRec bndr rhs) binding
+ -- and preInlineUnconditionally has been done already;
+ -- no need to repeat it. But for lambdas we must be careful about
+ -- preInlineUndonditionally: consider (\(x:Int#). 3) (error "urk")
+ -- We must not drop the (error "urk").
+ , Just env' <- preInlineUnconditionally env NotTopLevel bndr rhs rhs_se
+ -> do { tick (PreInlineUnconditionally bndr)
+ ; -- pprTrace "preInlineUncond" (ppr bndr <+> ppr rhs) $
+ simplLam env' body cont }
-- Deal with strict bindings
- -- See Note [Dark corner with representation polymorphism]
- | isStrictId bndr1 && seCaseCase env
- || needs_case_binding ->
- simplExprF (rhs_se `setInScopeFromE` env) rhs
- (StrictBind { sc_bndr = bndr, sc_body = body
- , sc_env = env, sc_cont = cont, sc_dup = NoDup })
+ | isStrictId bndr1 && seCaseCase env
+ || from_lam && needs_case_binding
+ -- The important bit here is needs_case_binds; but no need to
+ -- test it if from_lam is False because then needs_case_binding is False too
+ -- NB: either way, the RHS may or may not satisfy let-can-float
+ -- but that's ok for StrictBind.
+ -> simplExprF (rhs_se `setInScopeFromE` env) rhs
+ (StrictBind { sc_bndr = bndr, sc_body = body
+ , sc_env = env, sc_cont = cont, sc_dup = NoDup })
-- Deal with lazy bindings
- | otherwise ->
- do { (env2, bndr2) <- addBndrRules env1 bndr bndr1 (BC_Let NotTopLevel NonRecursive)
- ; (floats1, env3) <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
- ; (floats2, expr') <- simplLam env3 body cont
- ; return (floats1 `addFloats` floats2, expr') } }
+ | otherwise
+ -> do { (env2, bndr2) <- addBndrRules env1 bndr bndr1 (BC_Let NotTopLevel NonRecursive)
+ ; (floats1, env3) <- simplLazyBind env2 NotTopLevel NonRecursive bndr bndr2 rhs rhs_se
+ ; (floats2, expr') <- simplLam env3 body cont
+ ; return (floats1 `addFloats` floats2, expr') } }
------------------
simplRecE :: SimplEnv
@@ -1806,7 +1832,7 @@ care here.
Note [Avoiding exponential behaviour]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
One way in which we can get exponential behaviour is if we simplify a
-big expression, and the re-simplify it -- and then this happens in a
+big expression, and then re-simplify it -- and then this happens in a
deeply-nested way. So we must be jolly careful about re-simplifying
an expression. That is why simplNonRecX does not try
preInlineUnconditionally (unlike simplNonRecE).
@@ -1864,13 +1890,8 @@ simplNonRecJoinPoint :: SimplEnv -> InId -> InExpr
-> InExpr -> SimplCont
-> SimplM (SimplFloats, OutExpr)
simplNonRecJoinPoint env bndr rhs body cont
- | assert (isJoinId bndr ) True
- , Just env' <- preInlineUnconditionally env NotTopLevel bndr rhs env
- = do { tick (PreInlineUnconditionally bndr)
- ; simplExprF env' body cont }
-
- | otherwise
- = wrapJoinCont env cont $ \ env cont ->
+ = assert (isJoinId bndr ) $
+ wrapJoinCont env cont $ \ env cont ->
do { -- We push join_cont into the join RHS and the body;
-- and wrap wrap_cont around the whole thing
; let mult = contHoleScaling cont
=====================================
compiler/GHC/Core/TyCon.hs
=====================================
@@ -2118,12 +2118,13 @@ isTypeDataTyCon (AlgTyCon {algTcRhs = DataTyCon {is_type_data = type_data }})
isTypeDataTyCon _ = False
-- | 'isInjectiveTyCon' is true of 'TyCon's for which this property holds
--- (where X is the role passed in):
--- If (T a1 b1 c1) ~X (T a2 b2 c2), then (a1 ~X1 a2), (b1 ~X2 b2), and (c1 ~X3 c2)
--- (where X1, X2, and X3, are the roles given by tyConRolesX tc X)
--- See also Note [Decomposing equality] in "GHC.Tc.Solver.Canonical"
+-- (where r is the role passed in):
+-- If (T a1 b1 c1) ~r (T a2 b2 c2), then (a1 ~r1 a2), (b1 ~r2 b2), and (c1 ~r3 c2)
+-- (where r1, r2, and r3, are the roles given by tyConRolesX tc r)
+-- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical"
isInjectiveTyCon :: TyCon -> Role -> Bool
-isInjectiveTyCon _ Phantom = False
+isInjectiveTyCon _ Phantom = True -- Vacuously; (t1 ~P t2) holes for all t1, t2!
+
isInjectiveTyCon (AlgTyCon {}) Nominal = True
isInjectiveTyCon (AlgTyCon {algTcRhs = rhs}) Representational
= isGenInjAlgRhs rhs
@@ -2139,9 +2140,9 @@ isInjectiveTyCon (TcTyCon {}) _ = True
-- See Note [How TcTyCons work] item (1) in GHC.Tc.TyCl
-- | 'isGenerativeTyCon' is true of 'TyCon's for which this property holds
--- (where X is the role passed in):
--- If (T tys ~X t), then (t's head ~X T).
--- See also Note [Decomposing equality] in "GHC.Tc.Solver.Canonical"
+-- (where r is the role passed in):
+-- If (T tys ~r t), then (t's head ~r T).
+-- See also Note [Decomposing TyConApp equalities] in "GHC.Tc.Solver.Canonical"
isGenerativeTyCon :: TyCon -> Role -> Bool
isGenerativeTyCon (FamilyTyCon { famTcFlav = DataFamilyTyCon _ }) Nominal = True
isGenerativeTyCon (FamilyTyCon {}) _ = False
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1073,7 +1073,8 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
-- See Note [Canonicalising type applications] about why we require rewritten types
-- Use tcSplitAppTy, not matching on AppTy, to catch oversaturated type families
--- NB: Only decompose AppTy for nominal equality. See Note [Decomposing equality]
+-- NB: Only decompose AppTy for nominal equality.
+-- See Note [Decomposing AppTy equalities]
can_eq_nc' True _rdr_env _envs ev NomEq ty1 _ ty2 _
| Just (t1, s1) <- tcSplitAppTy_maybe ty1
, Just (t2, s2) <- tcSplitAppTy_maybe ty2
@@ -1350,6 +1351,8 @@ zonk_eq_types = go
{- See Note [Unwrap newtypes first]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Decomposing newtype equalities]
+
Consider
newtype N m a = MkN (m a)
Then N will get a conservative, Nominal role for its second parameter 'a',
@@ -1463,7 +1466,7 @@ can_eq_app :: CtEvidence -- :: s1 t1 ~N s2 t2
-- AppTys only decompose for nominal equality, so this case just leads
-- to an irreducible constraint; see typecheck/should_compile/T10494
--- See Note [Decomposing AppTy at representational role]
+-- See Note [Decomposing AppTy equalities]
can_eq_app ev s1 t1 s2 t2
| CtWanted { ctev_dest = dest, ctev_rewriters = rewriters } <- ev
= do { co_s <- unifyWanted rewriters loc Nominal s1 s2
@@ -1530,8 +1533,9 @@ canTyConApp :: CtEvidence -> EqRel
-> TyCon -> [TcType]
-> TyCon -> [TcType]
-> TcS (StopOrContinue Ct)
--- See Note [Decomposing TyConApps]
--- Neither tc1 nor tc2 is a saturated funTyCon
+-- See Note [Decomposing TyConApp equalities]
+-- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family
+-- But they can be data families.
canTyConApp ev eq_rel tc1 tys1 tc2 tys2
| tc1 == tc2
, tys1 `equalLength` tys2
@@ -1561,13 +1565,17 @@ canTyConApp ev eq_rel tc1 tys1 tc2 tys2
ty1 = mkTyConApp tc1 tys1
ty2 = mkTyConApp tc2 tys2
- loc = ctEvLoc ev
- pred = ctEvPred ev
-
- -- See Note [Decomposing equality]
+ -- See Note [Decomposing TyConApp equalities]
+ -- Note [Decomposing newtypes a bit more aggressively]
can_decompose inerts
= isInjectiveTyCon tc1 (eqRelRole eq_rel)
- || (ctEvFlavour ev /= Given && isEmptyBag (matchableGivens loc pred inerts))
+ || (assert (eq_rel == ReprEq) $
+ -- assert: isInjectiveTyCon is always True for Nominal except
+ -- for type synonyms/families, neither of which happen here
+ -- Moreover isInjectiveTyCon is True for Representational
+ -- for algebraic data types. So we are down to newtypes
+ -- and data families.
+ ctEvFlavour ev == Wanted && noGivenIrreds inerts)
{-
Note [Use canEqFailure in canDecomposableTyConApp]
@@ -1601,219 +1609,329 @@ For example, see typecheck/should_compile/T10493, repeated here:
That should compile, but only because we use canEqFailure and not
canEqHardFailure.
-Note [Decomposing equality]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we have a constraint (of any flavour and role) that looks like
-T tys1 ~ T tys2, what can we conclude about tys1 and tys2? The answer,
-of course, is "it depends". This Note spells it all out.
-
-In this Note, "decomposition" refers to taking the constraint
- [fl] (T tys1 ~X T tys2)
-(for some flavour fl and some role X) and replacing it with
- [fls'] (tys1 ~Xs' tys2)
-where that notation indicates a list of new constraints, where the
-new constraints may have different flavours and different roles.
-
-The key property to consider is injectivity. When decomposing a Given, the
-decomposition is sound if and only if T is injective in all of its type
-arguments. When decomposing a Wanted, the decomposition is sound (assuming the
-correct roles in the produced equality constraints), but it may be a guess --
-that is, an unforced decision by the constraint solver. Decomposing Wanteds
-over injective TyCons does not entail guessing. But sometimes we want to
-decompose a Wanted even when the TyCon involved is not injective! (See below.)
-
-So, in broad strokes, we want this rule:
-
-(*) Decompose a constraint (T tys1 ~X T tys2) if and only if T is injective
-at role X.
-
-Pursuing the details requires exploring three axes:
-* Flavour: Given vs. Wanted
-* Role: Nominal vs. Representational
-* TyCon species: datatype vs. newtype vs. data family vs. type family vs. type variable
-
-(A type variable isn't a TyCon, of course, but it's convenient to put the AppTy case
-in the same table.)
-
-Here is a table (discussion following) detailing where decomposition of
- (T s1 ... sn) ~r (T t1 .. tn)
-is allowed. The first four lines (Data types ... type family) refer
-to TyConApps with various TyCons T; the last line is for AppTy, covering
-both where there is a type variable at the head and the case for an over-
-saturated type family.
-
-NOMINAL GIVEN WANTED WHERE
-
-Datatype YES YES canTyConApp
-Newtype YES YES canTyConApp
-Data family YES YES canTyConApp
-Type family NO{1} YES, in injective args{1} canEqCanLHS2
-AppTy YES YES can_eq_app
-
-REPRESENTATIONAL GIVEN WANTED
-
-Datatype YES YES canTyConApp
-Newtype NO{2} MAYBE{2} canTyConApp(can_decompose)
-Data family NO{3} MAYBE{3} canTyConApp(can_decompose)
-Type family NO NO canEqCanLHS2
-AppTy NO{4} NO{4} can_eq_nc'
-
-{1}: Type families can be injective in some, but not all, of their arguments,
-so we want to do partial decomposition. This is quite different than the way
-other decomposition is done, where the decomposed equalities replace the original
-one. We thus proceed much like we do with superclasses, emitting new Wanteds
-when "decomposing" a partially-injective type family Wanted. Injective type
-families have no corresponding evidence of their injectivity, so we cannot
-decompose an injective-type-family Given.
-
-{2}: See Note [Decomposing newtypes at representational role]
-
-{3}: Because of the possibility of newtype instances, we must treat
-data families like newtypes. See also
-Note [Decomposing newtypes at representational role]. See #10534 and
-test case typecheck/should_fail/T10534.
-
-{4}: See Note [Decomposing AppTy at representational role]
-
- Because type variables can stand in for newtypes, we conservatively do not
- decompose AppTys over representational equality. Here are two examples that
- demonstrate why we can't:
-
- 4a: newtype Phant a = MkPhant Int
- [W] alpha Int ~R beta Bool
-
- If we eventually solve alpha := Phant and beta := Phant, then we can solve
- this equality by unwrapping. But it would have been disastrous to decompose
- the wanted to produce Int ~ Bool, which is definitely insoluble.
-
- 4b: newtype Age = MkAge Int
- [W] alpha Age ~R Maybe Int
-
- First, a question: if we know that ty1 ~R ty2, can we conclude that
- a ty1 ~R a ty2? Not for all a. This is precisely why we need role annotations
- on type constructors. So, if we were to decompose, we would need to
- decompose to [W] alpha ~R Maybe and [W] Age ~ Int. On the other hand, if we
- later solve alpha := Maybe, then we would decompose to [W] Age ~R Int, and
- that would be soluble.
-
-In the implementation of can_eq_nc and friends, we don't directly pattern
-match using lines like in the tables above, as those tables don't cover
-all cases (what about PrimTyCon? tuples?). Instead we just ask about injectivity,
-boiling the tables above down to rule (*). The exceptions to rule (*) are for
-injective type families, which are handled separately from other decompositions,
-and the MAYBE entries above.
-
-Note [Decomposing newtypes at representational role]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-This note discusses the 'newtype' line in the REPRESENTATIONAL table
-in Note [Decomposing equality]. (At nominal role, newtypes are fully
-decomposable.)
+Note [Fast path when decomposing TyConApps]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
+ (s1 ~ s2, t1 ~ t2)
+and push those back into the work list. But if
+ s1 = K k1 s2 = K k2
+then we will just decompose s1~s2, and it might be better to
+do so on the spot. An important special case is where s1=s2,
+and we get just Refl.
-Here is a representative example of why representational equality over
-newtypes is tricky:
+So canDecomposableTyConAppOK uses unifyWanted etc to short-cut that work.
- 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
+Note [Decomposing TyConApp equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have
+ [G/W] T ty1 ~r T ty2
+Can we decompose it, and replace it by
+ [G/W] ty1 ~r' ty2
+and if so what role is r'? (In this Note, all the "~" are primitive
+equalities "~#", but I have dropped the noisy "#" symbols.) Lots of
+background in the paper "Safe zero-cost coercions for Haskell".
+
+This Note covers the topic for
+ * Datatypes
+ * Newtypes
+ * Data families
+For the rest:
+ * Type synonyms: are always expanded
+ * Type families: see Note [Decomposing type family applications]
+ * AppTy: see Note [Decomposing AppTy equalities].
+
+---- Roles of the decomposed constraints ----
+For a start, the role r' will always be defined like this:
+ * If r=N then r' = N
+ * If r=R then r' = role of T's first argument
+
+For example:
+ data TR a = MkTR a -- Role of T's first arg is Representational
+ data TN a = MkTN (F a) -- Role of T's first arg is Nominal
+
+The function tyConRolesX :: Role -> TyCon -> [Role] gets the argument
+role r' for a TyCon T at role r. E.g.
+ tyConRolesX Nominal TR = [Nominal]
+ tyConRolesX Representational TR = [Representational]
+
+---- Soundness and completeness ----
+For Givens, for /soundness/ of decomposition we need, forall ty1,ty2:
+ T ty1 ~r T ty2 ===> ty1 ~r' ty2
+Here "===>" means "implies". That is, given evidence for (co1 : T ty1 ~r T co2)
+we can produce evidence for (co2 : ty1 ~r' ty2). But in the solver we
+/replace/ co1 with co2 in the inert set, and we don't want to lose any proofs
+thereby. So for /completeness/ of decomposition we also need the reverse:
+ ty1 ~r' ty2 ===> T ty1 ~r T ty2
+
+For Wanteds, for /soundness/ of decomposition we need:
+ ty1 ~r' ty2 ===> T ty1 ~r T ty2
+because if we do decompose we'll get evidence (co2 : ty1 ~r' ty2) and
+from that we want to derive evidence (T co2 : T ty1 ~r T ty2).
+For /completeness/ of decomposition we need the reverse implication too,
+else we may decompose to a new proof obligation that is stronger than
+the one we started with. See Note [Decomposing newtype equalities].
+
+---- Injectivity ----
+When do these bi-implications hold? In one direction it is easy.
+We /always/ have
+ ty1 ~r' ty2 ===> T ty1 ~r T ty2
+This is the CO_TYCONAPP rule of the paper (Fig 5); see also the
+TyConAppCo case of GHC.Core.Lint.lintCoercion.
+
+In the other direction, we have
+ T ty1 ~r T ty2 ==> ty1 ~r' ty2 if T is /injective at role r/
+This is the very /definition/ of injectivity: injectivity means result
+is the same => arguments are the same, modulo the role shift.
+See comments on GHC.Core.TyCon.isInjectiveTyCon. This is also
+the CO_NTH rule in Fig 5 of the paper, except in the paper only
+newtypes are non-injective at representation role, so the rule says "H
+is not a newtype".
+
+Injectivity is a bit subtle:
+ Nominal Representational
+ Datatype YES YES
+ Newtype YES NO{1}
+ Data family YES NO{2}
+
+{1} Consider newtype N a = MkN (F a) -- Arg has Nominal role
+ Is it true that (N t1) ~R (N t2) ==> t1 ~N t2 ?
+ No, absolutely not. E.g.
+ type instance F Int = Int; type instance F Bool = Char
+ Then (N Int) ~R (N Bool), by unwrapping, but we don't want Int~Char!
+
+ See Note [Decomposing newtype equalities]
+
+{2} We must treat data families precisely like newtypes, because of the
+ possibility of newtype instances. See also
+ Note [Decomposing newtype equalities]. See #10534 and
+ test case typecheck/should_fail/T10534.
+
+---- Takeaway summary -----
+For sound and complete decomposition, we simply need injectivity;
+that is for isInjectiveTyCon to be true:
+
+* At Nominal role, isInjectiveTyCon is True for all the TyCons we are
+ considering in this Note: datatypes, newtypes, and data families.
+
+* For Givens, injectivity is necessary for soundness; completeness has no
+ side conditions.
+
+* For Wanteds, soundness has no side conditions; but injectivity is needed
+ for completeness. See Note [Decomposing newtype equalities]
+
+This is implemented in `can_decompose` in `canTyConApp`; it looks at
+injectivity, just as specified above.
+
+
+Note [Decomposing type family applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supose we have
+ [G/W] (F ty1) ~r (F ty2)
+This is handled by the TyFamLHS/TyFamLHS case of canEqCanLHS2.
+
+We never decompose to
+ [G/W] ty1 ~r' ty2
+
+Instead
+
+* For Givens we do nothing. Injective type families have no corresponding
+ evidence of their injectivity, so we cannot decompose an
+ injective-type-family Given.
+
+* For Wanteds, for the Nominal role only, we emit new Wanteds rather like
+ functional dependencies, for each injective argument position.
+
+ E.g type family F a b -- injective in first arg, but not second
+ [W] (F s1 t1) ~N (F s2 t2)
+ Emit new Wanteds
+ [W] s1 ~N s2
+ But retain the existing, unsolved constraint.
+
+Note [Decomposing newtype equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+This Note also applies to data families, which we treat like
+newtype in case of 'newtype instance'.
+
+As Note [Decomposing TyConApp equalities] describes, if N is injective
+at role r, we can do this decomposition?
+ [G/W] (N ty1) ~r (N ty2) to [G/W] ty1 ~r' ty2
+
+For a Given with r=R, the answer is a solid NO: newtypes are not injective at
+representational role, and we must not decompose, or we lose soundness.
+Example is wrinkle {1} in Note [Decomposing TyConApp equalities].
+
+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.
+
+Conclusion: decompose newtypes (at role R) only if there are no usable Givens.
+
+* Incompleteness example (EX1)
+ newtype Nt a = MkNt (Id a)
+ type family Id a where Id a = a
+
+ [W] Nt Int ~R Nt Age
+
+ Because of its use of a type family, Nt's parameter will get inferred to
+ have a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age,
+ which is unsatisfiable. Unwrapping, though, leads to a solution.
-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. Here's another example.
+ Conclusion: always unwrap newtypes before attempting to decompose
+ them. This is done in can_eq_nc'. Of course, we can't unwrap if the data
+ constructor isn't in scope. See See Note [Unwrap newtypes first].
- newtype Nt a = MkNt (Id a)
- type family Id a where Id a = a
+* Incompleteness example (EX2)
+ 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
- [W] Nt Int ~R Nt Age
+ 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.
-Because of its use of a type family, Nt's parameter will get inferred to have
-a nominal role. Thus, decomposing the wanted will yield [W] Int ~N Age, which
-is unsatisfiable. Unwrapping, though, leads to a solution.
+ 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.
-Conclusion:
- * Unwrap newtypes before attempting to decompose them.
- This is done in can_eq_nc'.
+ Conclusion: don't decompose [W] N s ~R N t, if there are any Given
+ equalities that could later solve it.
-It all comes from the fact that newtypes aren't necessarily injective
-w.r.t. representational equality.
+ But what does "any Given equalities that could later solve it" mean, precisely?
+ It must be a Given constraint that could turn into N s ~ N t. But that
+ could include [G] (a b) ~ (c d), or even just [G] c. But it'll definitely
+ be an CIrredCan. So we settle for having no CIrredCans at all, which is
+ conservative but safe. See noGivenIrreds and #22331.
-Furthermore, as explained in Note [SelCo and newtypes] in GHC.Core.TyCo.Rep, we can't use
-SelCo on representational coercions over newtypes. SelCo comes into play
-only when decomposing givens.
+ Well not 100.0% safe. There could be a CDictCan with some un-expanded
+ superclasses; but only in some very obscure recursive-superclass
+ situations.
-Conclusion:
- * Do not decompose [G] N s ~R N t
+If there are no Irred Givens (which is quite common) then we will
+successfuly decompose [W] (IO Age) ~R (IO Int), and solve it. But
+that won't happen and [W] (IO Age) ~R (IO Int) will be stuck.
+We /could/, however, be a bit more aggressive about decomposition;
+see Note [Decomposing newtypes a bit more aggressively].
-Is it sensible to decompose *Wanted* constraints over newtypes? Yes!
-It's the only way we could ever prove (IO Int ~R IO Age), recalling
-that IO is a newtype.
+Remember: decomposing Wanteds is always /sound/. This Note is
+only about /completeness/.
-However we must be careful. Consider
+Note [Decomposing newtypes a bit more aggressively]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+c.f. https://github.com/ghc-proposals/ghc-proposals/pull/549
+and discussion on !9282.
+
+Consider [G] c, [W] (IO Int) ~R (IO Age)
+where IO is abstract, and
+ newtype Age = MkAge Int -- Not abstract
+With the above rules, if there any Given Irreds,
+the Wanted is insoluble because we can't decompose it. But in fact,
+if we look at the defn of IO, roughly,
+ newtype IO a = State# -> (State#, a)
+we can see that decomposing [W] (IO Int) ~R (IO Age) to
+ [W] Int ~R Age
+definitely does not lose completeness. Why not? Because the role of
+IO's argment is representational. Hence:
+
+ DecomposeNewtypeIdea:
+ decompose [W] (N s1 .. sn) ~R (N t1 .. tn)
+ if the roles of all N's arguments are representational
+
+If N's arguments really /are/ representational this will not lose
+completeness. Here "really are representational" means "if you expand
+all newtypes in N's RHS, we'd infer a representational role for each
+of N's type variables in that expansion". See Note [Role inference]
+in GHC.Tc.TyCl.Utils.
+
+But the user might /override/ a phantom role with an explicit role
+annotation, and then we could (obscurely) get incompleteness.
+Consider
- type role Nt representational
+ module A( silly, T ) where
+ newtype T a = MkT Int
+ type role T representational -- Override phantom role
- [G] Nt a ~R Nt b (1)
- [W] NT alpha ~R Nt b (2)
- [W] alpha ~ a (3)
+ silly :: Coercion (T Int) (T Bool)
+ silly = Coercion -- Typechecks by unwrapping the newtype
-If we focus on (3) first, we'll substitute in (2), and now it's
-identical to the given (1), so we succeed. But if we focus on (2)
-first, and decompose it, we'll get (alpha ~R b), which is not soluble.
-This is exactly like the question of overlapping Givens for class
-constraints: see Note [Instance and Given overlap] in GHC.Tc.Solver.Interact.
+ data Coercion a b where -- Actually defined in Data.Type.Coercion
+ Coercion :: Coercible a b => Coercion a b
-Conclusion:
- * Decompose [W] N s ~R N t iff there no given constraint that could
- later solve it.
+ module B where
+ import A
+ f :: T Int -> T Bool
+ f = case silly of Coercion -> coerce
-Note [Decomposing AppTy at representational role]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We never decompose AppTy at a representational role. For Givens, doing
-so is simply unsound: the LRCo coercion former requires a nominal-roled
-arguments. (See (1) for an example of why.) For Wanteds, decomposing
-would be sound, but it would be a guess, and a non-confluent one at that.
+Here the `coerce` gives [W] (T Int) ~R (T Bool) which, if we decompose,
+we'll get stuck with (Int ~R Bool). Instead we want to use the
+[G] (T Int) ~R (T Bool), which will be in the Irreds.
-Here is an example:
+Summary: we could adopt (DecomposeNewtypeIdea), at the cost of a very
+obscure incompleteness (above). But no one is reporting a problem from
+the lack of decompostion, so we'll just leave it for now. This long
+Note is just to record the thinking for our future selves.
+
+Note [Decomposing AppTy equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For AppTy all the same questions arise as in
+Note [Decomposing TyConApp equalities]. We have
+
+ s1 ~r s2, t1 ~N t2 ==> s1 t1 ~r s2 t2 (rule CO_APP)
+ s1 t1 ~N s2 t2 ==> s1 ~N s2, t1 ~N t2 (CO_LEFT, CO_RIGHT)
+
+In the first of these, why do we need Nominal equality in (t1 ~N t2)?
+See {2} below.
+
+For sound and complete solving, we need both directions to decompose. So:
+* At nominal role, all is well: we have both directions.
+* At representational role, decomposition of Givens is unsound (see {1} below),
+ and decomposition of Wanteds is incomplete.
+
+Here is an example of the incompleteness for Wanteds:
[G] g1 :: a ~R b
[W] w1 :: Maybe b ~R alpha a
- [W] w2 :: alpha ~ Maybe
+ [W] w2 :: alpha ~N Maybe
-Suppose we see w1 before w2. If we were to decompose, we would decompose
-this to become
+Suppose we see w1 before w2. If we decompose, using AppCo to prove w1, we get
+ w1 := AppCo w3 w4
[W] w3 :: Maybe ~R alpha
- [W] w4 :: b ~ a
+ [W] w4 :: b ~N a
Note that w4 is *nominal*. A nominal role here is necessary because AppCo
-requires a nominal role on its second argument. (See (2) for an example of
-why.) If we decomposed w1 to w3,w4, we would then get stuck, because w4
-is insoluble. On the other hand, if we see w2 first, setting alpha := Maybe,
-all is well, as we can decompose Maybe b ~R Maybe a into b ~R a.
+requires a nominal role on its second argument. (See {2} for an example of
+why.) Now we are stuck, because w4 is insoluble. On the other hand, if we
+see w2 first, setting alpha := Maybe, all is well, as we can decompose
+Maybe b ~R Maybe a into b ~R a.
Another example:
-
newtype Phant x = MkPhant Int
-
[W] w1 :: Phant Int ~R alpha Bool
[W] w2 :: alpha ~ Phant
If we see w1 first, decomposing would be disastrous, as we would then try
to solve Int ~ Bool. Instead, spotting w2 allows us to simplify w1 to become
-
[W] w1' :: Phant Int ~R Phant Bool
which can then (assuming MkPhant is in scope) be simplified to Int ~R Int,
and all will be well. See also Note [Unwrap newtypes first].
-Bottom line: never decompose AppTy with representational roles.
+Bottom line:
+* Always decompose AppTy at nominal role: can_eq_app
+* Never decompose AppTy at representational role (neither Given nor Wanted):
+ the lack of an equation in can_eq_nc'
-(1) Decomposing a Given AppTy over a representational role is simply
-unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
-the newtype Phant, above), then we surely don't want any relationship
-between Int and Bool, lest we also have co2 :: Phant ~ a around.
+Extra points
+{1} Decomposing a Given AppTy over a representational role is simply
+ unsound. For example, if we have co1 :: Phant Int ~R a Bool (for
+ the newtype Phant, above), then we surely don't want any relationship
+ between Int and Bool, lest we also have co2 :: Phant ~ a around.
-(2) The role on the AppCo coercion is a conservative choice, because we don't
-know the role signature of the function. For example, let's assume we could
-have a representational role on the second argument of AppCo. Then, consider
+{2} The role on the AppCo coercion is a conservative choice, because we don't
+ know the role signature of the function. For example, let's assume we could
+ have a representational role on the second argument of AppCo. Then, consider
data G a where -- G will have a nominal role, as G is a GADT
MkG :: G Int
@@ -1823,9 +1941,8 @@ have a representational role on the second argument of AppCo. Then, consider
co2 :: Age ~R Int -- by newtype axiom
co3 = AppCo co1 co2 :: G Age ~R a Int -- by our broken AppCo
-and now co3 can be used to cast MkG to have type G Age, in violation of
-the way GADTs are supposed to work (which is to use nominal equality).
-
+ and now co3 can be used to cast MkG to have type G Age, in violation of
+ the way GADTs are supposed to work (which is to use nominal equality).
-}
canDecomposableTyConAppOK :: CtEvidence -> EqRel
@@ -1842,6 +1959,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-- we are guaranteed that cos has the same length
-- as tys1 and tys2
-> do { cos <- zipWith4M (unifyWanted rewriters) new_locs tc_roles tys1 tys2
+ -- See Note [Fast path when decomposing TyConApps]
; setWantedEq dest (mkTyConAppCo role tc cos) }
CtGiven { ctev_evar = evar }
@@ -1945,19 +2063,6 @@ canEqHardFailure ev ty1 ty2
; continueWith (mkIrredCt ShapeMismatchReason new_ev) }
{-
-Note [Decomposing TyConApps]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-If we see (T s1 t1 ~ T s2 t2), then we can just decompose to
- (s1 ~ s2, t1 ~ t2)
-and push those back into the work list. But if
- s1 = K k1 s2 = K k2
-then we will just decompose s1~s2, and it might be better to
-do so on the spot. An important special case is where s1=s2,
-and we get just Refl.
-
-So canDecomposableTyCon is a fast-path decomposition that uses
-unifyWanted etc to short-cut that work.
-
Note [Canonicalising type applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Given (s1 t1) ~ ty2, how should we proceed?
@@ -2192,6 +2297,7 @@ canEqCanLHS2 ev eq_rel swapped lhs1 ps_xi1 lhs2 ps_xi2 mco
| TyFamLHS fun_tc1 fun_args1 <- lhs1
, TyFamLHS fun_tc2 fun_args2 <- lhs2
+ -- See Note [Decomposing type family applications]
= do { traceTcS "canEqCanLHS2 two type families" (ppr lhs1 $$ ppr lhs2)
-- emit wanted equalities for injective type families
=====================================
compiler/GHC/Tc/Solver/InertSet.hs
=====================================
@@ -20,7 +20,8 @@ module GHC.Tc.Solver.InertSet (
emptyInert,
addInertItem,
- matchableGivens,
+ noMatchableGivenDicts,
+ noGivenIrreds,
mightEqualLater,
prohibitedSuperClassSolve,
@@ -53,6 +54,7 @@ import GHC.Core.Reduction
import GHC.Core.Predicate
import GHC.Core.TyCo.FVs
import qualified GHC.Core.TyCo.Rep as Rep
+import GHC.Core.Class( Class )
import GHC.Core.TyCon
import GHC.Core.Unify
@@ -1535,25 +1537,20 @@ isOuterTyVar tclvl tv
-- becomes "outer" even though its level numbers says it isn't.
| otherwise = False -- Coercion variables; doesn't much matter
--- | Returns Given constraints that might,
--- potentially, match the given pred. This is used when checking to see if a
+noGivenIrreds :: InertSet -> Bool
+noGivenIrreds (IS { inert_cans = inert_cans })
+ = isEmptyBag (inert_irreds inert_cans)
+
+-- | Returns True iff there are no Given constraints that might,
+-- potentially, match the given class consraint. This is used when checking to see if a
-- Given might overlap with an instance. See Note [Instance and Given overlap]
-- in "GHC.Tc.Solver.Interact"
-matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
-matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
- = filterBag matchable_given all_relevant_givens
+noMatchableGivenDicts :: InertSet -> CtLoc -> Class -> [TcType] -> Bool
+noMatchableGivenDicts inerts@(IS { inert_cans = inert_cans }) loc_w clas tys
+ = not $ anyBag matchable_given $
+ findDictsByClass (inert_dicts inert_cans) clas
where
- -- just look in class constraints and irreds. matchableGivens does get called
- -- for ~R constraints, but we don't need to look through equalities, because
- -- canonical equalities are used for rewriting. We'll only get caught by
- -- non-canonical -- that is, irreducible -- equalities.
- all_relevant_givens :: Cts
- all_relevant_givens
- | Just (clas, _) <- getClassPredTys_maybe pred_w
- = findDictsByClass (inert_dicts inert_cans) clas
- `unionBags` inert_irreds inert_cans
- | otherwise
- = inert_irreds inert_cans
+ pred_w = mkClassPred clas tys
matchable_given :: Ct -> Bool
matchable_given ct
=====================================
compiler/GHC/Tc/Solver/Interact.hs
=====================================
@@ -1391,7 +1391,7 @@ We generate these Wanteds in three places, depending on how we notice the
injectivity.
1. When we have a [W] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and
-described in Note [Decomposing equality] in GHC.Tc.Solver.Canonical.
+described in Note [Decomposing type family applications] in GHC.Tc.Solver.Canonical.
2. When we have [W] F tys1 ~ T and [W] F tys2 ~ T. Note that neither of these
constraints rewrites the other, as they have different LHSs. This is done
@@ -2283,11 +2283,9 @@ matchClassInst dflags inerts clas tys loc
-- See Note [Instance and Given overlap]
| not (xopt LangExt.IncoherentInstances dflags)
, not (naturallyCoherentClass clas)
- , let matchable_givens = matchableGivens loc pred inerts
- , not (isEmptyBag matchable_givens)
+ , not (noMatchableGivenDicts inerts loc clas tys)
= do { traceTcS "Delaying instance application" $
- vcat [ text "Work item=" <+> pprClassPred clas tys
- , text "Potential matching givens:" <+> ppr matchable_givens ]
+ vcat [ text "Work item=" <+> pprClassPred clas tys ]
; return NotSure }
| otherwise
=====================================
m4/fp_musttail.m4
=====================================
@@ -5,7 +5,7 @@ AC_DEFUN([FP_MUSTTAIL],
[
AC_MSG_CHECKING([whether __attribute__((musttail)) is supported])
echo 'extern int foo(void); int bar(void) { __attribute__((musttail)) return foo(); }' > conftest.c
- if $CC -c conftest.c -o conftest.o
+ if $CC -c conftest.c -o conftest.o > /dev/null 2>&1
then
AC_MSG_RESULT([yes])
AC_DEFINE(HAS_MUSTTAIL, 1, [Has musttail])
=====================================
testsuite/tests/simplCore/should_compile/T22491.hs
=====================================
@@ -0,0 +1,319 @@
+{-# LANGUAGE Haskell2010 #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+module T22491 (heapster_add_block_hints) where
+
+import qualified Control.Exception as X
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Catch (MonadThrow(..), MonadCatch(..), catches, Handler(..))
+import Control.Monad.IO.Class
+import qualified Control.Monad.Fail as Fail
+import Control.Monad.Trans.Class (MonadTrans(..))
+import Control.Monad.Trans.Reader (ReaderT)
+import Data.Coerce (Coercible, coerce)
+import Data.IORef
+import Data.Kind (Type)
+import Data.Monoid
+import GHC.Exts (build)
+
+failOnNothing :: Fail.MonadFail m => String -> Maybe a -> m a
+failOnNothing err_str Nothing = Fail.fail err_str
+failOnNothing _ (Just a) = return a
+
+lookupLLVMSymbolModAndCFG :: HeapsterEnv -> String -> IO (Maybe (AnyCFG LLVM))
+lookupLLVMSymbolModAndCFG _ _ = pure Nothing
+
+heapster_add_block_hints :: HeapsterEnv -> String -> [Int] ->
+ (forall ext blocks ret.
+ CFG ext blocks ret ->
+ TopLevel Hint) ->
+ TopLevel ()
+heapster_add_block_hints henv nm blks hintF =
+ do env <- liftIO $ readIORef $ heapsterEnvPermEnvRef henv
+ AnyCFG cfg <-
+ failOnNothing ("Could not find symbol definition: " ++ nm) =<<
+ io (lookupLLVMSymbolModAndCFG henv nm)
+ let blocks = fmapFC blockInputs $ cfgBlockMap cfg
+ block_idxs = fmapFC (blockIDIndex . blockID) $ cfgBlockMap cfg
+ blkIDs <- case blks of
+ [] -> pure $ toListFC (Some . BlockID) block_idxs
+ _ -> forM blks $ \blk ->
+ failOnNothing ("Block ID " ++ show blk ++
+ " not found in function " ++ nm)
+ (fmapF BlockID <$> intIndex blk (size blocks))
+ env' <- foldM (\env' _ ->
+ permEnvAddHint env' <$>
+ hintF cfg)
+ env blkIDs
+ liftIO $ writeIORef (heapsterEnvPermEnvRef henv) env'
+
+-----
+
+data Some (f:: k -> Type) = forall x . Some (f x)
+
+class FunctorF m where
+ fmapF :: (forall x . f x -> g x) -> m f -> m g
+
+mapSome :: (forall tp . f tp -> g tp) -> Some f -> Some g
+mapSome f (Some x) = Some $! f x
+
+instance FunctorF Some where fmapF = mapSome
+
+type SingleCtx x = EmptyCtx ::> x
+
+data Ctx k
+ = EmptyCtx
+ | Ctx k ::> k
+
+type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k where
+ x <+> EmptyCtx = x
+ x <+> (y ::> e) = (x <+> y) ::> e
+
+data Height = Zero | Succ Height
+
+data BalancedTree h (f :: k -> Type) (p :: Ctx k) where
+ BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x)
+ BalPair :: !(BalancedTree h f x)
+ -> !(BalancedTree h f y)
+ -> BalancedTree ('Succ h) f (x <+> y)
+
+data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where
+ Empty :: BinomialTree h f EmptyCtx
+
+ PlusOne :: !Int
+ -> !(BinomialTree ('Succ h) f x)
+ -> !(BalancedTree h f y)
+ -> BinomialTree h f (x <+> y)
+
+ PlusZero :: !Int
+ -> !(BinomialTree ('Succ h) f x)
+ -> BinomialTree h f x
+
+tsize :: BinomialTree h f a -> Int
+tsize Empty = 0
+tsize (PlusOne s _ _) = 2*s+1
+tsize (PlusZero s _) = 2*s
+
+fmap_bin :: (forall tp . f tp -> g tp)
+ -> BinomialTree h f c
+ -> BinomialTree h g c
+fmap_bin _ Empty = Empty
+fmap_bin f (PlusOne s t x) = PlusOne s (fmap_bin f t) (fmap_bal f x)
+fmap_bin f (PlusZero s t) = PlusZero s (fmap_bin f t)
+{-# INLINABLE fmap_bin #-}
+
+fmap_bal :: (forall tp . f tp -> g tp)
+ -> BalancedTree h f c
+ -> BalancedTree h g c
+fmap_bal = go
+ where go :: (forall tp . f tp -> g tp)
+ -> BalancedTree h f c
+ -> BalancedTree h g c
+ go f (BalLeaf x) = BalLeaf (f x)
+ go f (BalPair x y) = BalPair (go f x) (go f y)
+{-# INLINABLE fmap_bal #-}
+
+traverse_bin :: Applicative m
+ => (forall tp . f tp -> m (g tp))
+ -> BinomialTree h f c
+ -> m (BinomialTree h g c)
+traverse_bin _ Empty = pure Empty
+traverse_bin f (PlusOne s t x) = PlusOne s <$> traverse_bin f t <*> traverse_bal f x
+traverse_bin f (PlusZero s t) = PlusZero s <$> traverse_bin f t
+{-# INLINABLE traverse_bin #-}
+
+traverse_bal :: Applicative m
+ => (forall tp . f tp -> m (g tp))
+ -> BalancedTree h f c
+ -> m (BalancedTree h g c)
+traverse_bal = go
+ where go :: Applicative m
+ => (forall tp . f tp -> m (g tp))
+ -> BalancedTree h f c
+ -> m (BalancedTree h g c)
+ go f (BalLeaf x) = BalLeaf <$> f x
+ go f (BalPair x y) = BalPair <$> go f x <*> go f y
+{-# INLINABLE traverse_bal #-}
+
+data Assignment (f :: k -> Type) (ctx :: Ctx k)
+ = Assignment (BinomialTree 'Zero f ctx)
+
+newtype Index (ctx :: Ctx k) (tp :: k) = Index { indexVal :: Int }
+
+newtype Size (ctx :: Ctx k) = Size Int
+
+intIndex :: Int -> Size ctx -> Maybe (Some (Index ctx))
+intIndex i n | 0 <= i && i < sizeInt n = Just (Some (Index i))
+ | otherwise = Nothing
+
+size :: Assignment f ctx -> Size ctx
+size (Assignment t) = Size (tsize t)
+
+sizeInt :: Size ctx -> Int
+sizeInt (Size n) = n
+
+class FunctorFC (t :: (k -> Type) -> l -> Type) where
+ fmapFC :: forall f g. (forall x. f x -> g x) ->
+ (forall x. t f x -> t g x)
+
+(#.) :: Coercible b c => (b -> c) -> (a -> b) -> (a -> c)
+(#.) _f = coerce
+
+class FoldableFC (t :: (k -> Type) -> l -> Type) where
+ foldMapFC :: forall f m. Monoid m => (forall x. f x -> m) -> (forall x. t f x -> m)
+ foldMapFC f = foldrFC (mappend . f) mempty
+
+ foldrFC :: forall f b. (forall x. f x -> b -> b) -> (forall x. b -> t f x -> b)
+ foldrFC f z t = appEndo (foldMapFC (Endo #. f) t) z
+
+ toListFC :: forall f a. (forall x. f x -> a) -> (forall x. t f x -> [a])
+ toListFC f t = build (\c n -> foldrFC (\e v -> c (f e) v) n t)
+
+foldMapFCDefault :: (TraversableFC t, Monoid m) => (forall x. f x -> m) -> (forall x. t f x -> m)
+foldMapFCDefault = \f -> getConst . traverseFC (Const . f)
+{-# INLINE foldMapFCDefault #-}
+
+class (FunctorFC t, FoldableFC t) => TraversableFC (t :: (k -> Type) -> l -> Type) where
+ traverseFC :: forall f g m. Applicative m
+ => (forall x. f x -> m (g x))
+ -> (forall x. t f x -> m (t g x))
+
+instance FunctorFC Assignment where
+ fmapFC = \f (Assignment x) -> Assignment (fmap_bin f x)
+ {-# INLINE fmapFC #-}
+
+instance FoldableFC Assignment where
+ foldMapFC = foldMapFCDefault
+ {-# INLINE foldMapFC #-}
+
+instance TraversableFC Assignment where
+ traverseFC = \f (Assignment x) -> Assignment <$> traverse_bin f x
+ {-# INLINE traverseFC #-}
+
+data CrucibleType
+
+data TypeRepr (tp::CrucibleType) where
+
+type CtxRepr = Assignment TypeRepr
+
+data CFG (ext :: Type)
+ (blocks :: Ctx (Ctx CrucibleType))
+ (ret :: CrucibleType)
+ = CFG { cfgBlockMap :: !(BlockMap ext blocks ret)
+ }
+
+type BlockMap ext blocks ret = Assignment (Block ext blocks ret) blocks
+
+data Block ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ctx
+ = Block { blockID :: !(BlockID blocks ctx)
+ , blockInputs :: !(CtxRepr ctx)
+ }
+
+newtype BlockID (blocks :: Ctx (Ctx CrucibleType)) (tp :: Ctx CrucibleType)
+ = BlockID { blockIDIndex :: Index blocks tp }
+
+data LLVM
+
+data AnyCFG ext where
+ AnyCFG :: CFG ext blocks ret
+ -> AnyCFG ext
+
+newtype StateContT s r m a
+ = StateContT { runStateContT :: (a -> s -> m r)
+ -> s
+ -> m r
+ }
+
+fmapStateContT :: (a -> b) -> StateContT s r m a -> StateContT s r m b
+fmapStateContT = \f m -> StateContT $ \c -> runStateContT m (\v s -> (c $! f v) s)
+{-# INLINE fmapStateContT #-}
+
+applyStateContT :: StateContT s r m (a -> b) -> StateContT s r m a -> StateContT s r m b
+applyStateContT = \mf mv ->
+ StateContT $ \c ->
+ runStateContT mf (\f -> runStateContT mv (\v s -> (c $! f v) s))
+{-# INLINE applyStateContT #-}
+
+returnStateContT :: a -> StateContT s r m a
+returnStateContT = \v -> seq v $ StateContT $ \c -> c v
+{-# INLINE returnStateContT #-}
+
+bindStateContT :: StateContT s r m a -> (a -> StateContT s r m b) -> StateContT s r m b
+bindStateContT = \m n -> StateContT $ \c -> runStateContT m (\a -> runStateContT (n a) c)
+{-# INLINE bindStateContT #-}
+
+instance Functor (StateContT s r m) where
+ fmap = fmapStateContT
+
+instance Applicative (StateContT s r m) where
+ pure = returnStateContT
+ (<*>) = applyStateContT
+
+instance Monad (StateContT s r m) where
+ (>>=) = bindStateContT
+
+instance MonadFail m => MonadFail (StateContT s r m) where
+ fail = \msg -> StateContT $ \_ _ -> fail msg
+
+instance MonadTrans (StateContT s r) where
+ lift = \m -> StateContT $ \c s -> m >>= \v -> seq v (c v s)
+
+instance MonadIO m => MonadIO (StateContT s r m) where
+ liftIO = lift . liftIO
+
+instance MonadThrow m => MonadThrow (StateContT s r m) where
+ throwM e = StateContT (\_k _s -> throwM e)
+
+instance MonadCatch m => MonadCatch (StateContT s r m) where
+ catch m hdl =
+ StateContT $ \k s ->
+ catch
+ (runStateContT m k s)
+ (\e -> runStateContT (hdl e) k s)
+
+data TopLevelRO
+data TopLevelRW
+data Value
+
+newtype TopLevel a =
+ TopLevel_ (ReaderT TopLevelRO (StateContT TopLevelRW (Value, TopLevelRW) IO) a)
+ deriving (Applicative, Functor, Monad, MonadFail, MonadThrow, MonadCatch)
+
+instance MonadIO TopLevel where
+ liftIO = io
+
+io :: IO a -> TopLevel a
+io f = TopLevel_ (liftIO f) `catches` [Handler handleIO]
+ where
+ rethrow :: X.Exception ex => ex -> TopLevel a
+ rethrow ex = throwM (X.SomeException ex)
+
+ handleIO :: X.IOException -> TopLevel a
+ handleIO = rethrow
+
+data HeapsterEnv = HeapsterEnv {
+ heapsterEnvPermEnvRef :: IORef PermEnv
+ }
+
+data Hint where
+
+data PermEnv = PermEnv {
+ permEnvHints :: [Hint]
+ }
+
+permEnvAddHint :: PermEnv -> Hint -> PermEnv
+permEnvAddHint env hint = env { permEnvHints = hint : permEnvHints env }
+
+type family CtxToRList (ctx :: Ctx k) :: RList k where
+ CtxToRList EmptyCtx = RNil
+ CtxToRList (ctx' ::> x) = CtxToRList ctx' :> x
+
+data RList a
+ = RNil
+ | (RList a) :> a
=====================================
testsuite/tests/simplCore/should_compile/all.T
=====================================
@@ -452,3 +452,5 @@ test('T22375', normal, compile, ['-O -ddump-simpl -dsuppress-uniques -dno-typeab
test('T21851_2', [grep_errmsg(r'wwombat') ], multimod_compile, ['T21851_2', '-O -dno-typeable-binds -dsuppress-uniques'])
# Should not inline m, so there shouldn't be a single YES
test('T22317', [grep_errmsg(r'ANSWER = YES') ], compile, ['-O -dinline-check m -ddebug-output'])
+
+test('T22491', normal, compile, ['-O2'])
=====================================
testsuite/tests/typecheck/should_compile/T22331.hs
=====================================
@@ -0,0 +1,15 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T22331 where
+
+import Data.Coerce
+
+data family Fool a
+
+-- This works
+joe :: Coercible (Fool a) (Fool b) => Fool a -> Fool b
+joe = coerce
+
+-- This does not
+bob :: Coercible (Fool a) (Fool b) => Fool b -> Fool a
+bob = coerce
=====================================
testsuite/tests/typecheck/should_compile/all.T
=====================================
@@ -850,3 +850,4 @@ test('T21951a', normal, compile, ['-Wredundant-strictness-flags'])
test('T21951b', normal, compile, ['-Wredundant-strictness-flags'])
test('T21550', normal, compile, [''])
test('T22310', normal, compile, [''])
+test('T22331', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4726ad42ba02dd94ab815bf278d01bb3d7f07543...1abeda0d0dde9cbc552d558aaa5ee7d83ff903b6
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/4726ad42ba02dd94ab815bf278d01bb3d7f07543...1abeda0d0dde9cbc552d558aaa5ee7d83ff903b6
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/20221128/f7c7725f/attachment-0001.html>
More information about the ghc-commits
mailing list