diff --git a/compiler/GHC/Core/Coercion.hs b/compiler/GHC/Core/Coercion.hs
index 21d537112e43a6235ae8b0f827edcce0fcabb124..9000e7a399e94578b5db79732563769f503be94c 100644
--- a/compiler/GHC/Core/Coercion.hs
+++ b/compiler/GHC/Core/Coercion.hs
@@ -41,7 +41,7 @@ module GHC.Core.Coercion (
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
mkFunCo, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
mkNakedFunCo,
- mkForAllCo, mkForAllCos, mkHomoForAllCos,
+ mkNakedForAllCo, mkForAllCo, mkHomoForAllCos,
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
mkAxiomInstCo, mkProofIrrelCo,
@@ -74,7 +74,7 @@ module GHC.Core.Coercion (
mkCoherenceRightMCo,
coToMCo, mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo,
- mkHomoForAllMCo, mkFunResMCo, mkPiMCos,
+ mkFunResMCo, mkPiMCos,
isReflMCo, checkReflexiveMCo,
-- ** Coercion variables
@@ -138,7 +138,7 @@ import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Tidy
-import GHC.Core.TyCo.Compare( eqType, eqTypeX )
+import GHC.Core.TyCo.Compare
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Core.TyCon.RecWalk
@@ -169,6 +169,7 @@ import Control.Monad (foldM, zipWithM)
import Data.Function ( on )
import Data.Char( isDigit )
import qualified Data.Monoid as Monoid
+import Control.DeepSeq
{-
%************************************************************************
@@ -361,10 +362,6 @@ mkCastTyMCo :: Type -> MCoercion -> Type
mkCastTyMCo ty MRefl = ty
mkCastTyMCo ty (MCo co) = ty `mkCastTy` co
-mkHomoForAllMCo :: TyCoVar -> MCoercion -> MCoercion
-mkHomoForAllMCo _ MRefl = MRefl
-mkHomoForAllMCo tcv (MCo co) = MCo (mkHomoForAllCos [tcv] co)
-
mkPiMCos :: [Var] -> MCoercion -> MCoercion
mkPiMCos _ MRefl = MRefl
mkPiMCos vs (MCo co) = MCo (mkPiCos Representational vs co)
@@ -555,22 +552,29 @@ splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitFunCo_maybe (FunCo { fco_arg = arg, fco_res = res }) = Just (arg, res)
splitFunCo_maybe _ = Nothing
-splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
-splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
-splitForAllCo_maybe _ = Nothing
+splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
+splitForAllCo_maybe (ForAllCo { fco_tcv = tv, fco_visL = vL, fco_visR = vR
+ , fco_kind = k_co, fco_body = co })
+ = Just (tv, vL, vR, k_co, co)
+splitForAllCo_maybe _ = Nothing
-- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
-splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
-splitForAllCo_ty_maybe (ForAllCo tv k_co co)
- | isTyVar tv = Just (tv, k_co, co)
+splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
+splitForAllCo_ty_maybe co
+ | Just stuff@(tv, _, _, _, _) <- splitForAllCo_maybe co
+ , isTyVar tv
+ = Just stuff
splitForAllCo_ty_maybe _ = Nothing
-- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
-splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
-splitForAllCo_co_maybe (ForAllCo cv k_co co)
- | isCoVar cv = Just (cv, k_co, co)
+splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
+splitForAllCo_co_maybe co
+ | Just stuff@(cv, _, _, _, _) <- splitForAllCo_maybe co
+ , isCoVar cv
+ = Just stuff
splitForAllCo_co_maybe _ = Nothing
+
-------------------------------------------------------
-- and some coercion kind stuff
@@ -919,101 +923,86 @@ mkAppCos :: Coercion
-> Coercion
mkAppCos co1 cos = foldl' mkAppCo co1 cos
-{- Note [Unused coercion variable in ForAllCo]
- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See Note [Unused coercion variable in ForAllTy] in GHC.Core.TyCo.Rep for the
-motivation for checking coercion variable in types.
-To lift the design choice to (ForAllCo cv kind_co body_co), we have two options:
-
-(1) In mkForAllCo, we check whether cv is a coercion variable
- and whether it is not used in body_co. If so we construct a FunCo.
-(2) We don't do this check in mkForAllCo.
- In coercionKind, we use mkTyCoForAllTy to perform the check and construct
- a FunTy when necessary.
-
-We chose (2) for two reasons:
-
-* for a coercion, all that matters is its kind, So ForAllCo or FunCo does not
- make a difference.
-* even if cv occurs in body_co, it is possible that cv does not occur in the kind
- of body_co. Therefore the check in coercionKind is inevitable.
-
-The last wrinkle is that there are restrictions around the use of the cv in the
-coercion, as described in Section 5.8.5.2 of Richard's thesis. The idea is that
-we cannot prove that the type system is consistent with unrestricted use of this
-cv; the consistency proof uses an untyped rewrite relation that works over types
-with all coercions and casts removed. So, we can allow the cv to appear only in
-positions that are erased. As an approximation of this (and keeping close to the
-published theory), we currently allow the cv only within the type in a Refl node
-and under a GRefl node (including in the Coercion stored in a GRefl). It's
-possible other places are OK, too, but this is a safe approximation.
-
-Sadly, with heterogeneous equality, this restriction might be able to be violated;
-Richard's thesis is unable to prove that it isn't. Specifically, the liftCoSubst
-function might create an invalid coercion. Because a violation of the
-restriction might lead to a program that "goes wrong", it is checked all the time,
-even in a production compiler and without -dcore-lint. We *have* proved that the
-problem does not occur with homogeneous equality, so this check can be dropped
-once ~# is made to be homogeneous.
--}
-
-- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.
--- The kind of the tycovar should be the left-hand kind of the kind coercion.
--- See Note [Unused coercion variable in ForAllCo]
-mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
-mkForAllCo v kind_co co
- | assert (varType v `eqType` (coercionLKind kind_co)) True
- , assert (isTyVar v || almostDevoidCoVarOfCo v co) True
- , Just (ty, r) <- isReflCo_maybe co
- , isGReflCo kind_co
- = mkReflCo r (mkTyCoInvForAllTy v ty)
- | otherwise
- = ForAllCo v kind_co co
+mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
+mkForAllCo v visL visR kind_co co
+ | Just (ty, r) <- isReflCo_maybe co
+ , isReflCo kind_co
+ , visL `eqForAllVis` visR
+ = mkReflCo r (mkTyCoForAllTy v visL ty)
--- | Like 'mkForAllCo', but the inner coercion shouldn't be an obvious
--- reflexive coercion. For example, it is guaranteed in 'mkForAllCos'.
--- The kind of the tycovar should be the left-hand kind of the kind coercion.
-mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
-mkForAllCo_NoRefl v kind_co co
- | assert (varType v `eqType` (coercionLKind kind_co)) True
- , assert (not (isReflCo co)) True
- , isCoVar v
- , assert (almostDevoidCoVarOfCo v co) True
- , not (v `elemVarSet` tyCoVarsOfCo co)
- = mkFunCoNoFTF (coercionRole co) (multToCo ManyTy) kind_co co
- -- Functions from coercions are always unrestricted
- | otherwise
- = ForAllCo v kind_co co
-
--- | Make nested ForAllCos
-mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
-mkForAllCos bndrs co
- | Just (ty, r ) <- isReflCo_maybe co
- = let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
- foldl' (flip $ uncurry mkForAllCo_NoRefl)
- (mkReflCo r (mkTyCoInvForAllTys (reverse (map fst refls_rev'd)) ty))
- non_refls_rev'd
| otherwise
- = foldr (uncurry mkForAllCo_NoRefl) co bndrs
+ = mkForAllCo_NoRefl v visL visR kind_co co
-- | Make a Coercion quantified over a type/coercion variable;
--- the variable has the same type in both sides of the coercion
-mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
-mkHomoForAllCos vs co
- | Just (ty, r) <- isReflCo_maybe co
- = mkReflCo r (mkTyCoInvForAllTys vs ty)
+-- the variable has the same kind and visibility in both sides of the coercion
+mkHomoForAllCos :: [ForAllTyBinder] -> Coercion -> Coercion
+mkHomoForAllCos vs orig_co
+ | Just (ty, r) <- isReflCo_maybe orig_co
+ = mkReflCo r (mkTyCoForAllTys vs ty)
+ | otherwise
+ = foldr go orig_co vs
+ where
+ go (Bndr var vis) co
+ = mkForAllCo_NoRefl var vis vis (mkNomReflCo (varType var)) co
+
+-- | Like 'mkForAllCo', but there is no need to check that the inner coercion isn't Refl;
+-- the caller has done that. (For example, it is guaranteed in 'mkHomoForAllCos'.)
+-- The kind of the tycovar should be the left-hand kind of the kind coercion.
+mkForAllCo_NoRefl :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
+mkForAllCo_NoRefl tcv visL visR kind_co co
+ = assertGoodForAllCo tcv visL visR kind_co co $
+ assertPpr (not (isReflCo co && isReflCo kind_co && visL == visR)) (ppr co) $
+ ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co }
+
+assertGoodForAllCo :: HasDebugCallStack
+ => TyCoVar -> ForAllTyFlag -> ForAllTyFlag
+ -> CoercionN -> Coercion -> a -> a
+-- Check ForAllCo invariants; see Note [ForAllCo] in GHC.Core.TyCo.Rep
+assertGoodForAllCo tcv visL visR kind_co co
+ | isTyVar tcv
+ = assertPpr (tcv_type `eqType` kind_co_lkind) doc
+
| otherwise
- = mkHomoForAllCos_NoRefl vs co
-
--- | Like 'mkHomoForAllCos', but the inner coercion shouldn't be an obvious
--- reflexive coercion. For example, it is guaranteed in 'mkHomoForAllCos'.
-mkHomoForAllCos_NoRefl :: [TyCoVar] -> Coercion -> Coercion
-mkHomoForAllCos_NoRefl vs orig_co
- = assert (not (isReflCo orig_co))
- foldr go orig_co vs
+ = assertPpr (tcv_type `eqType` kind_co_lkind) doc
+ -- The kind of the tycovar should be the left-hand kind of the kind coercion.
+ . assertPpr (almostDevoidCoVarOfCo tcv co) doc
+ -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep
+ . assertPpr (visL == coreTyLamForAllTyFlag
+ && visR == coreTyLamForAllTyFlag) doc
+ -- See (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep
where
- go v co = mkForAllCo_NoRefl v (mkNomReflCo (varType v)) co
+ tcv_type = varType tcv
+ kind_co_lkind = coercionLKind kind_co
+
+ doc = vcat [ text "Var:" <+> ppr tcv <+> dcolon <+> ppr tcv_type
+ , text "Vis:" <+> ppr visL <+> ppr visR
+ , text "kind_co:" <+> ppr kind_co
+ , text "kind_co_lkind" <+> ppr kind_co_lkind
+ , text "body_co" <+> ppr co ]
+
+
+mkNakedForAllCo :: TyVar -- Never a CoVar
+ -> ForAllTyFlag -> ForAllTyFlag
+ -> CoercionN -> Coercion -> Coercion
+-- This version lacks the assertion checks.
+-- Used during type checking when the arguments may (legitimately) not be zonked
+-- and so the assertions might (bogusly) fail
+-- NB: since the coercions are un-zonked, we can't really deal with
+-- (FC6) and (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep.
+-- Fortunately we don't have to: this function is needed only for /type/ variables.
+mkNakedForAllCo tv visL visR kind_co co
+ | assertPpr (isTyVar tv) (ppr tv) True
+ , Just (ty, r) <- isReflCo_maybe co
+ , isReflCo kind_co
+ , visL `eqForAllVis` visR
+ = mkReflCo r (mkForAllTy (Bndr tv visL) ty)
+ | otherwise
+ = ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co }
+
mkCoVarCo :: CoVar -> Coercion
-- cv :: s ~# t
@@ -1163,7 +1152,7 @@ mkSelCo_maybe cs co
| Just (ty, r) <- isReflCo_maybe co
= Just (mkReflCo r (getNthFromType cs ty))
- go SelForAll (ForAllCo _ kind_co _)
+ go SelForAll (ForAllCo { fco_kind = kind_co })
= Just kind_co
-- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
-- then (nth SelForAll co :: k1 ~N k2)
@@ -1231,7 +1220,7 @@ mkLRCo lr co
-- | Instantiates a 'Coercion'.
mkInstCo :: Coercion -> CoercionN -> Coercion
-mkInstCo (ForAllCo tcv _kind_co body_co) co
+mkInstCo (ForAllCo { fco_tcv = tcv, fco_body = body_co }) co
| Just (arg, _) <- isReflCo_maybe co
-- works for both tyvar and covar
= substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
@@ -1383,8 +1372,10 @@ setNominalRole_maybe r co
= TransCo <$> setNominalRole_maybe_helper co1 <*> setNominalRole_maybe_helper co2
setNominalRole_maybe_helper (AppCo co1 co2)
= AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
- setNominalRole_maybe_helper (ForAllCo tv kind_co co)
- = ForAllCo tv kind_co <$> setNominalRole_maybe_helper co
+ setNominalRole_maybe_helper co@(ForAllCo { fco_visL = visL, fco_visR = visR, fco_body = body_co })
+ | visL `eqForAllVis` visR -- See (FC3) in Note [ForAllCo] in GHC.Core.TyCo.Rep
+ = do { body_co' <- setNominalRole_maybe_helper body_co
+ ; return (co { fco_body = body_co' }) }
setNominalRole_maybe_helper (SelCo cs co) =
-- NB, this case recurses via setNominalRole_maybe, not
-- setNominalRole_maybe_helper!
@@ -1404,6 +1395,7 @@ setNominalRole_maybe r co
| case prov of PhantomProv _ -> False -- should always be phantom
ProofIrrelProv _ -> True -- it's always safe
PluginProv _ -> False -- who knows? This choice is conservative.
+
CorePrepProv _ -> True
= Just $ UnivCo prov Nominal co1 co2
setNominalRole_maybe_helper _ = Nothing
@@ -1474,7 +1466,7 @@ ltRole Nominal _ = True
-- | like mkKindCo, but aggressively & recursively optimizes to avoid using
-- a KindCo constructor. The output role is nominal.
-promoteCoercion :: Coercion -> CoercionN
+promoteCoercion :: HasDebugCallStack => Coercion -> CoercionN
-- First cases handles anything that should yield refl.
promoteCoercion co = case co of
@@ -1504,7 +1496,7 @@ promoteCoercion co = case co of
| otherwise
-> mkKindCo co
- ForAllCo tv _ g
+ ForAllCo { fco_tcv = tv, fco_body = g }
| isTyVar tv
-> promoteCoercion g
@@ -1515,7 +1507,7 @@ promoteCoercion co = case co of
-- a coercion variable. So both sides have kind Type
-- (Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep).
-- So the result is Refl, and that should have been caught by
- -- the first equation above
+ -- the first equation above. Hence `assert False`
mkNomReflCo liftedTypeKind
FunCo {} -> mkKindCo co
@@ -1659,7 +1651,7 @@ mkPiCos r vs co = foldr (mkPiCo r) co vs
-- | Make a forall 'Coercion', where both types related by the coercion
-- are quantified over the same variable.
mkPiCo :: Role -> Var -> Coercion -> Coercion
-mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
+mkPiCo r v co | isTyVar v = mkHomoForAllCos [Bndr v coreTyLamForAllTyFlag] co
| isCoVar v = assert (not (v `elemVarSet` tyCoVarsOfCo co)) $
-- We didn't call mkForAllCo here because if v does not appear
-- in co, the argument coercion will be nominal. But here we
@@ -2083,17 +2075,17 @@ ty_co_subst !lc role ty
go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2)
go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRoleListX r tc) tys)
go r (FunTy af w t1 t2) = mkFunCo r af (go Nominal w) (go r t1) (go r t2)
- go r t@(ForAllTy (Bndr v _) ty)
+ go r t@(ForAllTy (Bndr v vis) ty)
= let (lc', v', h) = liftCoSubstVarBndr lc v
body_co = ty_co_subst lc' r ty in
if isTyVar v' || almostDevoidCoVarOfCo v' body_co
-- Lifting a ForAllTy over a coercion variable could fail as ForAllCo
- -- imposes an extra restriction on where a covar can appear. See last
- -- wrinkle in Note [Unused coercion variable in ForAllCo].
- -- We specifically check for this and panic because we know that
- -- there's a hole in the type system here, and we'd rather panic than
- -- fall into it.
- then mkForAllCo v' h body_co
+ -- imposes an extra restriction on where a covar can appear. See
+ -- (FC6) of Note [ForAllCo] in GHC.Tc.TyCo.Rep
+ -- We specifically check for this and panic because we know that
+ -- there's a hole in the type system here (see (FC6), and we'd rather
+ -- panic than fall into it.
+ then mkForAllCo v' vis vis h body_co
else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
go r ty@(LitTy {}) = assert (r == Nominal) $
mkNomReflCo ty
@@ -2331,8 +2323,9 @@ seqCo (Refl ty) = seqType ty
seqCo (GRefl r ty mco) = r `seq` seqType ty `seq` seqMCo mco
seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos
seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
-seqCo (ForAllCo tv k co) = seqType (varType tv) `seq` seqCo k
- `seq` seqCo co
+seqCo (ForAllCo tv visL visR k co) = seqType (varType tv) `seq`
+ rnf visL `seq` rnf visR `seq`
+ seqCo k `seq` seqCo co
seqCo (FunCo r af1 af2 w co1 co2) = r `seq` af1 `seq` af2 `seq`
seqCo w `seq` seqCo co1 `seq` seqCo co2
seqCo (CoVarCo cv) = cv `seq` ()
@@ -2397,7 +2390,8 @@ coercionLKind co
go (GRefl _ ty _) = ty
go (TyConAppCo _ tc cos) = mkTyConApp tc (map go cos)
go (AppCo co1 co2) = mkAppTy (go co1) (go co2)
- go (ForAllCo tv1 _ co1) = mkTyCoInvForAllTy tv1 (go co1)
+ go (ForAllCo { fco_tcv = tv1, fco_visL = visL, fco_body = co1 })
+ = mkTyCoForAllTy tv1 visL (go co1)
go (FunCo { fco_afl = af, fco_mult = mult, fco_arg = arg, fco_res = res})
{- See Note [FunCo] -} = FunTy { ft_af = af, ft_mult = go mult
, ft_arg = go arg, ft_res = go res }
@@ -2476,8 +2470,9 @@ coercionRKind co
go (AxiomRuleCo ax cos) = pSnd $ expectJust "coercionKind" $
coaxrProves ax $ map coercionKind cos
- go co@(ForAllCo tv1 k_co co1) -- works for both tyvar and covar
- | isGReflCo k_co = mkTyCoInvForAllTy tv1 (go co1)
+ go co@(ForAllCo { fco_tcv = tv1, fco_visR = visR
+ , fco_kind = k_co, fco_body = co1 }) -- works for both tyvar and covar
+ | isGReflCo k_co = mkTyCoForAllTy tv1 visR (go co1)
-- kind_co always has kind @Type@, thus @isGReflCo@
| otherwise = go_forall empty_subst co
where
@@ -2500,10 +2495,11 @@ coercionRKind co
go_app (InstCo co arg) args = go_app co (go arg:args)
go_app co args = piResultTys (go co) args
- go_forall subst (ForAllCo tv1 k_co co)
+ go_forall subst (ForAllCo { fco_tcv = tv1, fco_visR = visR
+ , fco_kind = k_co, fco_body = co })
-- See Note [Nested ForAllCos]
| isTyVar tv1
- = mkInfForAllTy tv2 (go_forall subst' co)
+ = mkForAllTy (Bndr tv2 visR) (go_forall subst' co)
where
k2 = coercionRKind k_co
tv2 = setTyVarKind tv1 (substTy subst k2)
@@ -2512,9 +2508,10 @@ coercionRKind co
| otherwise = extendTvSubst (extendSubstInScope subst tv2) tv1 $
TyVarTy tv2 `mkCastTy` mkSymCo k_co
- go_forall subst (ForAllCo cv1 k_co co)
+ go_forall subst (ForAllCo { fco_tcv = cv1, fco_visR = visR
+ , fco_kind = k_co, fco_body = co })
| isCoVar cv1
- = mkTyCoInvForAllTy cv2 (go_forall subst' co)
+ = mkTyCoForAllTy cv2 visR (go_forall subst' co)
where
k2 = coercionRKind k_co
r = coVarRole cv1
@@ -2562,26 +2559,26 @@ change reduces /total/ compile time by a factor of more than ten.
coercionRole :: Coercion -> Role
coercionRole = go
where
- go (Refl _) = Nominal
- go (GRefl r _ _) = r
- go (TyConAppCo r _ _) = r
- go (AppCo co1 _) = go co1
- go (ForAllCo _ _ co) = go co
- go (FunCo { fco_role = r }) = r
- go (CoVarCo cv) = coVarRole cv
- go (HoleCo h) = coVarRole (coHoleCoVar h)
- go (AxiomInstCo ax _ _) = coAxiomRole ax
- go (UnivCo _ r _ _) = r
- go (SymCo co) = go co
- go (TransCo co1 _co2) = go co1
- go (SelCo SelForAll _co) = Nominal
- go (SelCo (SelTyCon _ r) _co) = r
- go (SelCo (SelFun fs) co) = funRole (coercionRole co) fs
- go (LRCo {}) = Nominal
- go (InstCo co _) = go co
- go (KindCo {}) = Nominal
- go (SubCo _) = Representational
- go (AxiomRuleCo ax _) = coaxrRole ax
+ go (Refl _) = Nominal
+ go (GRefl r _ _) = r
+ go (TyConAppCo r _ _) = r
+ go (AppCo co1 _) = go co1
+ go (ForAllCo { fco_body = co }) = go co
+ go (FunCo { fco_role = r }) = r
+ go (CoVarCo cv) = coVarRole cv
+ go (HoleCo h) = coVarRole (coHoleCoVar h)
+ go (AxiomInstCo ax _ _) = coAxiomRole ax
+ go (UnivCo _ r _ _) = r
+ go (SymCo co) = go co
+ go (TransCo co1 _co2) = go co1
+ go (SelCo SelForAll _co) = Nominal
+ go (SelCo (SelTyCon _ r) _co) = r
+ go (SelCo (SelFun fs) co) = funRole (coercionRole co) fs
+ go (LRCo {}) = Nominal
+ go (InstCo co _) = go co
+ go (KindCo {}) = Nominal
+ go (SubCo _) = Representational
+ go (AxiomRuleCo ax _) = coaxrRole ax
{-
Note [Nested InstCos]
@@ -2686,19 +2683,19 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
| Just (ty1a, ty1b) <- splitAppTyNoView_maybe ty1
= mkAppCo (go ty1a ty2a) (go ty1b ty2b)
- go (ForAllTy (Bndr tv1 _flag1) ty1) (ForAllTy (Bndr tv2 _flag2) ty2)
+ go (ForAllTy (Bndr tv1 flag1) ty1) (ForAllTy (Bndr tv2 flag2) ty2)
| isTyVar tv1
= assert (isTyVar tv2) $
- mkForAllCo tv1 kind_co (go ty1 ty2')
+ mkForAllCo tv1 flag1 flag2 kind_co (go ty1 ty2')
where kind_co = go (tyVarKind tv1) (tyVarKind tv2)
in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
ty2' = substTyWithInScope in_scope [tv2]
[mkTyVarTy tv1 `mkCastTy` kind_co]
ty2
- go (ForAllTy (Bndr cv1 _flag1) ty1) (ForAllTy (Bndr cv2 _flag2) ty2)
+ go (ForAllTy (Bndr cv1 flag1) ty1) (ForAllTy (Bndr cv2 flag2) ty2)
= assert (isCoVar cv1 && isCoVar cv2) $
- mkForAllCo cv1 kind_co (go ty1 ty2')
+ mkForAllCo cv1 flag1 flag2 kind_co (go ty1 ty2')
where s1 = varType cv1
s2 = varType cv2
kind_co = go s1 s2
diff --git a/compiler/GHC/Core/Coercion.hs-boot b/compiler/GHC/Core/Coercion.hs-boot
index 276a48cf81811e3ad8afba8f22be01d67aaea1bd..b2a11c603da7812c61e6a6a49820e42096dd397e 100644
--- a/compiler/GHC/Core/Coercion.hs-boot
+++ b/compiler/GHC/Core/Coercion.hs-boot
@@ -16,7 +16,7 @@ import GHC.Utils.Misc
mkReflCo :: Role -> Type -> Coercion
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkAppCo :: Coercion -> Coercion -> Coercion
-mkForAllCo :: TyCoVar -> Coercion -> Coercion -> Coercion
+mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
diff --git a/compiler/GHC/Core/Coercion/Opt.hs b/compiler/GHC/Core/Coercion/Opt.hs
index 98506c444e323fea25d972c220916be0138cb8d5..44a381259801ac697dd8c2142eb384523fb71544 100644
--- a/compiler/GHC/Core/Coercion/Opt.hs
+++ b/compiler/GHC/Core/Coercion/Opt.hs
@@ -14,13 +14,14 @@ import GHC.Tc.Utils.TcType ( exactTyCoVarsOfType )
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.Subst
-import GHC.Core.TyCo.Compare( eqType )
+import GHC.Core.TyCo.Compare( eqType, eqForAllVis )
import GHC.Core.Coercion
import GHC.Core.Type as Type hiding( substTyVarBndr, substTy )
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Core.Unify
+import GHC.Types.Var
import GHC.Types.Var.Set
import GHC.Types.Var.Env
import GHC.Types.Unique.Set
@@ -289,11 +290,14 @@ opt_co4 env sym rep r (AppCo co1 co2)
= mkAppCo (opt_co4_wrap env sym rep r co1)
(opt_co4_wrap env sym False Nominal co2)
-opt_co4 env sym rep r (ForAllCo tv k_co co)
+opt_co4 env sym rep r (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR
+ , fco_kind = k_co, fco_body = co })
= case optForAllCoBndr env sym tv k_co of
- (env', tv', k_co') -> mkForAllCo tv' k_co' $
+ (env', tv', k_co') -> mkForAllCo tv' visL' visR' k_co' $
opt_co4_wrap env' sym rep r co
-- Use the "mk" functions to check for nested Refls
+ where
+ !(visL', visR') = swapSym sym (visL, visR)
opt_co4 env sym rep r (FunCo _r afl afr cow co1 co2)
= assert (r == _r) $
@@ -304,8 +308,7 @@ opt_co4 env sym rep r (FunCo _r afl afr cow co1 co2)
cow' = opt_co1 env sym cow
!r' | rep = Representational
| otherwise = r
- !(afl', afr') | sym = (afr,afl)
- | otherwise = (afl,afr)
+ !(afl', afr') = swapSym sym (afl, afr)
opt_co4 env sym rep r (CoVarCo cv)
| Just co <- lookupCoVar (lcSubst env) cv
@@ -375,7 +378,7 @@ opt_co4 env sym rep r (SelCo (SelTyCon n r1) (TyConAppCo _ _ cos))
opt_co4 env sym rep r (SelCo (SelFun fs) (FunCo _r2 _afl _afr w co1 co2))
= opt_co4_wrap env sym rep r (getNthFun fs w co1 co2)
-opt_co4 env sym rep _ (SelCo SelForAll (ForAllCo _ eta _))
+opt_co4 env sym rep _ (SelCo SelForAll (ForAllCo { fco_kind = eta }))
-- works for both tyvar and covar
= opt_co4_wrap env sym rep Nominal eta
@@ -383,7 +386,7 @@ opt_co4 env sym rep r (SelCo n co)
| Just nth_co <- case (co', n) of
(TyConAppCo _ _ cos, SelTyCon n _) -> Just (cos `getNth` n)
(FunCo _ _ _ w co1 co2, SelFun fs) -> Just (getNthFun fs w co1 co2)
- (ForAllCo _ eta _, SelForAll) -> Just eta
+ (ForAllCo { fco_kind = eta }, SelForAll) -> Just eta
_ -> Nothing
= if rep && (r == Nominal)
-- keep propagating the SubCo
@@ -415,7 +418,7 @@ opt_co4 env sym rep r (LRCo lr co)
-- See Note [Optimising InstCo]
opt_co4 env sym rep r (InstCo co1 arg)
-- forall over type...
- | Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
+ | Just (tv, _visL, _visR, kind_co, co_body) <- splitForAllCo_ty_maybe co1
= opt_co4_wrap (extendLiftingContext env tv
(mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg))
-- mkSymCo kind_co :: k1 ~ k2
@@ -424,7 +427,7 @@ opt_co4 env sym rep r (InstCo co1 arg)
sym rep r co_body
-- forall over coercion...
- | Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1
+ | Just (cv, _visL, _visR, kind_co, co_body) <- splitForAllCo_co_maybe co1
, CoercionTy h1 <- t1
, CoercionTy h2 <- t2
= let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2
@@ -434,13 +437,13 @@ opt_co4 env sym rep r (InstCo co1 arg)
-- If so, do an inefficient one-variable substitution, then re-optimize
-- forall over type...
- | Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
+ | Just (tv', _visL, _visR, kind_co', co_body') <- splitForAllCo_ty_maybe co1'
= opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
(mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg'))
False False r' co_body'
-- forall over coercion...
- | Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
+ | Just (cv', _visL, _visR, kind_co', co_body') <- splitForAllCo_co_maybe co1'
, CoercionTy h1' <- t1'
, CoercionTy h2' <- t2'
= let new_co = mk_new_co cv' kind_co' h1' h2'
@@ -574,8 +577,10 @@ opt_univ env sym prov role oty1 oty2
-- can't optimize the AppTy case because we can't build the kind coercions.
- | Just (tv1, ty1) <- splitForAllTyVar_maybe oty1
- , Just (tv2, ty2) <- splitForAllTyVar_maybe oty2
+ | Just (Bndr tv1 vis1, ty1) <- splitForAllForAllTyBinder_maybe oty1
+ , isTyVar tv1
+ , Just (Bndr tv2 vis2, ty2) <- splitForAllForAllTyBinder_maybe oty2
+ , isTyVar tv2
-- NB: prov isn't interesting here either
= let k1 = tyVarKind tv1
k2 = tyVarKind tv2
@@ -584,11 +589,14 @@ opt_univ env sym prov role oty1 oty2
ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
(env', tv1', eta') = optForAllCoBndr env sym tv1 eta
+ !(vis1', vis2') = swapSym sym (vis1, vis2)
in
- mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2')
+ mkForAllCo tv1' vis1' vis2' eta' (opt_univ env' sym prov' role ty1 ty2')
- | Just (cv1, ty1) <- splitForAllCoVar_maybe oty1
- , Just (cv2, ty2) <- splitForAllCoVar_maybe oty2
+ | Just (Bndr cv1 vis1, ty1) <- splitForAllForAllTyBinder_maybe oty1
+ , isCoVar cv1
+ , Just (Bndr cv2 vis2, ty2) <- splitForAllForAllTyBinder_maybe oty2
+ , isCoVar cv2
-- NB: prov isn't interesting here either
= let k1 = varType cv1
k2 = varType cv2
@@ -602,8 +610,9 @@ opt_univ env sym prov role oty1 oty2
ty2' = substTyWithCoVars [cv2] [n_co] ty2
(env', cv1', eta') = optForAllCoBndr env sym cv1 eta
+ !(vis1', vis2') = swapSym sym (vis1, vis2)
in
- mkForAllCo cv1' eta' (opt_univ env' sym prov' role ty1 ty2')
+ mkForAllCo cv1' vis1' vis2' eta' (opt_univ env' sym prov' role ty1 ty2')
| otherwise
= let ty1 = substTyUnchecked (lcSubstLeft env) oty1
@@ -747,23 +756,23 @@ opt_trans_rule is co1 co2@(AppCo co2a co2b)
-- Push transitivity inside forall
-- forall over types.
opt_trans_rule is co1 co2
- | Just (tv1, eta1, r1) <- splitForAllCo_ty_maybe co1
- , Just (tv2, eta2, r2) <- etaForAllCo_ty_maybe co2
- = push_trans tv1 eta1 r1 tv2 eta2 r2
+ | Just (tv1, visL1, _visR1, eta1, r1) <- splitForAllCo_ty_maybe co1
+ , Just (tv2, _visL2, visR2, eta2, r2) <- etaForAllCo_ty_maybe co2
+ = push_trans tv1 eta1 r1 tv2 eta2 r2 visL1 visR2
- | Just (tv2, eta2, r2) <- splitForAllCo_ty_maybe co2
- , Just (tv1, eta1, r1) <- etaForAllCo_ty_maybe co1
- = push_trans tv1 eta1 r1 tv2 eta2 r2
+ | Just (tv2, _visL2, visR2, eta2, r2) <- splitForAllCo_ty_maybe co2
+ , Just (tv1, visL1, _visR1, eta1, r1) <- etaForAllCo_ty_maybe co1
+ = push_trans tv1 eta1 r1 tv2 eta2 r2 visL1 visR2
where
- push_trans tv1 eta1 r1 tv2 eta2 r2
+ push_trans tv1 eta1 r1 tv2 eta2 r2 visL visR
-- Given:
- -- co1 = /\ tv1 : eta1. r1
- -- co2 = /\ tv2 : eta2. r2
+ -- co1 = /\ tv1 : eta1 <visL, visM>. r1
+ -- co2 = /\ tv2 : eta2 <visM, visR>. r2
-- Wanted:
- -- /\tv1 : (eta1;eta2). (r1; r2[tv2 |-> tv1 |> eta1])
+ -- /\tv1 : (eta1;eta2) <visL, visR>. (r1; r2[tv2 |-> tv1 |> eta1])
= fireTransRule "EtaAllTy_ty" co1 co2 $
- mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
+ mkForAllCo tv1 visL visR (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
where
is' = is `extendInScopeSet` tv1
r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
@@ -771,25 +780,25 @@ opt_trans_rule is co1 co2
-- Push transitivity inside forall
-- forall over coercions.
opt_trans_rule is co1 co2
- | Just (cv1, eta1, r1) <- splitForAllCo_co_maybe co1
- , Just (cv2, eta2, r2) <- etaForAllCo_co_maybe co2
- = push_trans cv1 eta1 r1 cv2 eta2 r2
+ | Just (cv1, visL1, _visR1, eta1, r1) <- splitForAllCo_co_maybe co1
+ , Just (cv2, _visL2, visR2, eta2, r2) <- etaForAllCo_co_maybe co2
+ = push_trans cv1 eta1 r1 cv2 eta2 r2 visL1 visR2
- | Just (cv2, eta2, r2) <- splitForAllCo_co_maybe co2
- , Just (cv1, eta1, r1) <- etaForAllCo_co_maybe co1
- = push_trans cv1 eta1 r1 cv2 eta2 r2
+ | Just (cv2, _visL2, visR2, eta2, r2) <- splitForAllCo_co_maybe co2
+ , Just (cv1, visL1, _visR1, eta1, r1) <- etaForAllCo_co_maybe co1
+ = push_trans cv1 eta1 r1 cv2 eta2 r2 visL1 visR2
where
- push_trans cv1 eta1 r1 cv2 eta2 r2
+ push_trans cv1 eta1 r1 cv2 eta2 r2 visL visR
-- Given:
- -- co1 = /\ cv1 : eta1. r1
- -- co2 = /\ cv2 : eta2. r2
+ -- co1 = /\ (cv1 : eta1) <visL, visM>. r1
+ -- co2 = /\ (cv2 : eta2) <visM, visR>. r2
-- Wanted:
-- n1 = nth 2 eta1
-- n2 = nth 3 eta1
-- nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
= fireTransRule "EtaAllTy_co" co1 co2 $
- mkForAllCo cv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
+ mkForAllCo cv1 visL visR (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
where
is' = is `extendInScopeSet` cv1
role = coVarRole cv1
@@ -1087,6 +1096,10 @@ The problem described here was first found in dependent/should_compile/dynamic-p
-}
-----------
+swapSym :: SymFlag -> (a,a) -> (a,a)
+swapSym sym (x,y) | sym = (y,x)
+ | otherwise = (x,y)
+
wrapSym :: SymFlag -> Coercion -> Coercion
wrapSym sym co | sym = mkSymCo co
| otherwise = co
@@ -1186,31 +1199,39 @@ Here,
eta2 = mkSelCo (SelTyCon 3 r) h1 :: (s2 ~ s4)
h2 = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
-}
-etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
+etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-- Try to make the coercion be of form (forall tv:kind_co. co)
etaForAllCo_ty_maybe co
- | Just (tv, kind_co, r) <- splitForAllCo_ty_maybe co
- = Just (tv, kind_co, r)
-
- | Pair ty1 ty2 <- coercionKind co
- , Just (tv1, _) <- splitForAllTyVar_maybe ty1
- , isForAllTy_ty ty2
+ | Just (tv, visL, visR, kind_co, r) <- splitForAllCo_ty_maybe co
+ = Just (tv, visL, visR, kind_co, r)
+
+ | (Pair ty1 ty2, role) <- coercionKindRole co
+ , Just (Bndr tv1 vis1, _) <- splitForAllForAllTyBinder_maybe ty1
+ , isTyVar tv1
+ , Just (Bndr tv2 vis2, _) <- splitForAllForAllTyBinder_maybe ty2
+ , isTyVar tv2
+ -- can't eta-expand at nominal role unless visibilities match
+ , (role /= Nominal) || (vis1 `eqForAllVis` vis2)
, let kind_co = mkSelCo SelForAll co
- = Just ( tv1, kind_co
+ = Just ( tv1, vis1, vis2, kind_co
, mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
| otherwise
= Nothing
-etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
+etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
-- Try to make the coercion be of form (forall cv:kind_co. co)
etaForAllCo_co_maybe co
- | Just (cv, kind_co, r) <- splitForAllCo_co_maybe co
- = Just (cv, kind_co, r)
-
- | Pair ty1 ty2 <- coercionKind co
- , Just (cv1, _) <- splitForAllCoVar_maybe ty1
- , isForAllTy_co ty2
+ | Just (cv, visL, visR, kind_co, r) <- splitForAllCo_co_maybe co
+ = Just (cv, visL, visR, kind_co, r)
+
+ | (Pair ty1 ty2, role) <- coercionKindRole co
+ , Just (Bndr cv1 vis1, _) <- splitForAllForAllTyBinder_maybe ty1
+ , isCoVar cv1
+ , Just (Bndr cv2 vis2, _) <- splitForAllForAllTyBinder_maybe ty2
+ , isCoVar cv2
+ -- can't eta-expand at nominal role unless visibilities match
+ , (role /= Nominal)
= let kind_co = mkSelCo SelForAll co
r = coVarRole cv1
l_co = mkCoVarCo cv1
@@ -1218,7 +1239,7 @@ etaForAllCo_co_maybe co
r_co = mkSymCo (mkSelCo (SelTyCon 2 r) kind_co')
`mkTransCo` l_co
`mkTransCo` mkSelCo (SelTyCon 3 r) kind_co'
- in Just ( cv1, kind_co
+ in Just ( cv1, vis1, vis2, kind_co
, mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co))
| otherwise
diff --git a/compiler/GHC/Core/FVs.hs b/compiler/GHC/Core/FVs.hs
index 175091086d327adf8cb2f2168e79841b0164aa0d..225bc05960297712d8e09adf1198a937e632277b 100644
--- a/compiler/GHC/Core/FVs.hs
+++ b/compiler/GHC/Core/FVs.hs
@@ -386,8 +386,9 @@ orphNamesOfCo (Refl ty) = orphNamesOfType ty
orphNamesOfCo (GRefl _ ty mco) = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco
orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
orphNamesOfCo (AppCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
-orphNamesOfCo (ForAllCo _ kind_co co) = orphNamesOfCo kind_co
- `unionNameSet` orphNamesOfCo co
+orphNamesOfCo (ForAllCo { fco_kind = kind_co, fco_body = co })
+ = orphNamesOfCo kind_co
+ `unionNameSet` orphNamesOfCo co
orphNamesOfCo (FunCo { fco_mult = co_mult, fco_arg = co1, fco_res = co2 })
= orphNamesOfCo co_mult
`unionNameSet` orphNamesOfCo co1
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 1dd782172bea9d8d1c80ce65337c4d32812c45fd..bc49d1183620b4dccc9ea1be42477b970d21380f 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -48,7 +48,7 @@ import GHC.Core.Type as Type
import GHC.Core.Multiplicity
import GHC.Core.UsageEnv
import GHC.Core.TyCo.Rep -- checks validity of types/coercions
-import GHC.Core.TyCo.Compare( eqType )
+import GHC.Core.TyCo.Compare ( eqType, eqForAllVis )
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr
@@ -1842,7 +1842,6 @@ lintType ty@(ForAllTy (Bndr tcv vis) body_ty)
lintL (tcv `elemVarSet` tyCoVarsOfType body_ty) $
text "Covar does not occur in the body:" <+> (ppr tcv $$ ppr body_ty)
-- See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
- -- and cf GHC.Core.Coercion Note [Unused coercion variable in ForAllCo]
; return (ForAllTy (Bndr tcv' vis) body_ty') }
@@ -2230,9 +2229,14 @@ lintCoercion co@(AppCo co1 co2)
; return (AppCo co1' co2') }
----------
-lintCoercion co@(ForAllCo tcv kind_co body_co)
+lintCoercion co@(ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = body_co })
+-- See Note [ForAllCo] in GHC.Core.TyCo.Rep,
+-- including the typing rule for ForAllCo
+
| not (isTyCoVar tcv)
= failWithL (text "Non tyco binder in ForAllCo:" <+> ppr co)
+
| otherwise
= do { kind_co' <- lintStarCoercion kind_co
; lintTyCoBndr tcv $ \tcv' ->
@@ -2246,18 +2250,24 @@ lintCoercion co@(ForAllCo tcv kind_co body_co)
-- (forall (tcv:k2). rty[(tcv:k2) |> sym kind_co/tcv])
-- are both well formed. Easiest way is to call lintForAllBody
-- for each; there is actually no need to do the funky substitution
- ; let Pair lty rty = coercionKind body_co'
+ ; let (Pair lty rty, body_role) = coercionKindRole body_co'
; lintForAllBody tcv' lty
; lintForAllBody tcv' rty
; when (isCoVar tcv) $
- lintL (almostDevoidCoVarOfCo tcv body_co) $
- text "Covar can only appear in Refl and GRefl: " <+> ppr co
- -- See "last wrinkle" in GHC.Core.Coercion
- -- Note [Unused coercion variable in ForAllCo]
- -- and c.f. GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
+ do { lintL (visL == coreTyLamForAllTyFlag && visR == coreTyLamForAllTyFlag) $
+ text "Invalid visibility flags in CoVar ForAllCo" <+> ppr co
+ -- See (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep
+ ; lintL (almostDevoidCoVarOfCo tcv body_co) $
+ text "Covar can only appear in Refl and GRefl: " <+> ppr co
+ -- See (FC6) in Note [ForAllCo] in GHC.Core.TyCo.Rep
+ }
+
+ ; when (body_role == Nominal) $
+ lintL (visL `eqForAllVis` visR) $
+ text "Nominal ForAllCo has mismatched visibilities: " <+> ppr co
- ; return (ForAllCo tcv' kind_co' body_co') } }
+ ; return (co { fco_tcv = tcv', fco_kind = kind_co', fco_body = body_co' }) } }
lintCoercion co@(FunCo { fco_role = r, fco_afl = afl, fco_afr = afr
, fco_mult = cow, fco_arg = co1, fco_res = co2 })
diff --git a/compiler/GHC/Core/Opt/Arity.hs b/compiler/GHC/Core/Opt/Arity.hs
index 85309063698ee7033ed52146c36b28400d4af10b..c3d5ea41c3f9d62bc86d38339aa65accff1b5fdd 100644
--- a/compiler/GHC/Core/Opt/Arity.hs
+++ b/compiler/GHC/Core/Opt/Arity.hs
@@ -68,6 +68,7 @@ import GHC.Core.TyCo.Compare( eqType )
import GHC.Types.Demand
import GHC.Types.Cpr( CprSig, mkCprSig, botCpr )
import GHC.Types.Id
+import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Basic
@@ -2037,8 +2038,8 @@ This what eta_expand does. We do it in two steps:
Note that the /same/ EtaInfo drives both etaInfoAbs and etaInfoApp
-To a first approximation EtaInfo is just [Var]. But
-casts complicate the question. If we have
+To a first approximation EtaInfo is just [Var]. But casts complicate
+the question. If we have
newtype N a = MkN (S -> a)
axN :: N a ~ S -> a
and
@@ -2054,6 +2055,20 @@ nested newtypes. This is expressed by the EtaInfo type:
data EtaInfo = EI [Var] MCoercionR
+Precisely, here is the (EtaInfo Invariant):
+
+ EI bs co :: EtaInfo
+
+describes a particular eta-expansion, thus:
+
+ Abstraction: (\b1 b2 .. bn. []) |> sym co
+ Application: ([] |> co) b1 b2 .. bn
+
+ e :: T
+ co :: T ~R (t1 -> t2 -> .. -> tn -> tr)
+ e = (\b1 b2 ... bn. (e |> co) b1 b2 .. bn) |> sym co
+
+
Note [Check for reflexive casts in eta expansion]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It turns out that the casts created by the above mechanism are often Refl.
@@ -2109,13 +2124,7 @@ Now, when we push that eta_co inward in etaInfoApp:
--------------
data EtaInfo = EI [Var] MCoercionR
-
--- (EI bs co) describes a particular eta-expansion, as follows:
--- Abstraction: (\b1 b2 .. bn. []) |> sym co
--- Application: ([] |> co) b1 b2 .. bn
---
--- e :: T co :: T ~ (t1 -> t2 -> .. -> tn -> tr)
--- e = (\b1 b2 ... bn. (e |> co) b1 b2 .. bn) |> sym co
+ -- See Note [The EtaInfo mechanism]
instance Outputable EtaInfo where
ppr (EI vs mco) = text "EI" <+> ppr vs <+> parens (ppr mco)
@@ -2229,14 +2238,14 @@ mkEtaWW orig_oss ppr_orig_expr in_scope orig_ty
go n oss@(one_shot:oss1) subst ty
----------- Forall types (forall a. ty)
- | Just (tcv,ty') <- splitForAllTyCoVar_maybe ty
+ | Just (Bndr tcv vis, ty') <- splitForAllForAllTyBinder_maybe ty
, (subst', tcv') <- Type.substVarBndr subst tcv
, let oss' | isTyVar tcv = oss
| otherwise = oss1
-- A forall can bind a CoVar, in which case
-- we consume one of the [OneShotInfo]
, (in_scope, EI bs mco) <- go n oss' subst' ty'
- = (in_scope, EI (tcv' : bs) (mkHomoForAllMCo tcv' mco))
+ = (in_scope, EI (tcv' : bs) (mkEtaForAllMCo (Bndr tcv' vis) ty' mco))
----------- Function types (t1 -> t2)
| Just (_af, mult, arg_ty, res_ty) <- splitFunTy_maybe ty
@@ -2279,6 +2288,19 @@ mkEtaWW orig_oss ppr_orig_expr in_scope orig_ty
-- So we simply decline to eta-expand. Otherwise we'd end up
-- with an explicit lambda having a non-function type
+mkEtaForAllMCo :: ForAllTyBinder -> Type -> MCoercion -> MCoercion
+mkEtaForAllMCo (Bndr tcv vis) ty mco
+ = case mco of
+ MRefl | vis == coreTyLamForAllTyFlag -> MRefl
+ | otherwise -> mk_fco (mkRepReflCo ty)
+ MCo co -> mk_fco co
+ where
+ mk_fco co = MCo (mkForAllCo tcv vis coreTyLamForAllTyFlag
+ (mkNomReflCo (varType tcv)) co)
+ -- coreTyLamForAllTyFlag: See Note [The EtaInfo mechanism], particularly
+ -- the (EtaInfo Invariant). (sym co) wraps a lambda that always has
+ -- a ForAllTyFlag of coreTyLamForAllTyFlag; see wrinkle (FC4) in
+ -- Note [ForAllCo] in GHC.Core.TyCo.Rep
{-
************************************************************************
@@ -2706,9 +2728,14 @@ tryEtaReduce rec_ids bndrs body eval_sd
-- (and similarly for tyvars, coercion args)
, [CoreTickish])
-- See Note [Eta reduction with casted arguments]
- ok_arg bndr (Type ty) co _
- | Just tv <- getTyVar_maybe ty
- , bndr == tv = Just (mkHomoForAllCos [tv] co, [])
+ ok_arg bndr (Type arg_ty) co fun_ty
+ | Just tv <- getTyVar_maybe arg_ty
+ , bndr == tv = case splitForAllForAllTyBinder_maybe fun_ty of
+ Just (Bndr _ vis, _) -> Just (mkHomoForAllCos [Bndr tv vis] co, [])
+ Nothing -> pprPanic "tryEtaReduce: type arg to non-forall type"
+ (text "fun:" <+> ppr bndr
+ $$ text "arg:" <+> ppr arg_ty
+ $$ text "fun_ty:" <+> ppr fun_ty)
ok_arg bndr (Var v) co fun_ty
| bndr == v
, let mult = idMult bndr
diff --git a/compiler/GHC/Core/Reduction.hs b/compiler/GHC/Core/Reduction.hs
index a4f1df4f703d6c1d99a493c61d62d32cc6d3726b..71402aa383cb7eee33b56793110cc50cdb3a984d 100644
--- a/compiler/GHC/Core/Reduction.hs
+++ b/compiler/GHC/Core/Reduction.hs
@@ -376,7 +376,7 @@ mkForAllRedn :: ForAllTyFlag
-> Reduction
mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
= mkReduction
- (mkForAllCo tv1 h co)
+ (mkForAllCo tv1 vis vis h co)
(mkForAllTy (Bndr tv2 vis) ty)
where
tv2 = setTyVarKind tv1 ki'
@@ -389,7 +389,7 @@ mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn bndrs (Reduction co ty)
= mkReduction
- (mkHomoForAllCos (binderVars bndrs) co)
+ (mkHomoForAllCos bndrs co)
(mkForAllTys bndrs ty)
{-# INLINE mkHomoForAllRedn #-}
diff --git a/compiler/GHC/Core/TyCo/Compare.hs b/compiler/GHC/Core/TyCo/Compare.hs
index c0a87d34ffb363b52acc03eb186df8e496b1f451..b03729e21c256b5880ba7836daa00532e8bbf595 100644
--- a/compiler/GHC/Core/TyCo/Compare.hs
+++ b/compiler/GHC/Core/TyCo/Compare.hs
@@ -173,7 +173,7 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
go env (ForAllTy (Bndr tv1 vis1) ty1)
(ForAllTy (Bndr tv2 vis2) ty2)
- = vis1 `eqForAllVis` vis2
+ = vis1 `eqForAllVis` vis2 -- See Note [ForAllTy and type equality]
&& (vis_only || go env (varType tv1) (varType tv2))
&& go (rnBndr2 env tv1 tv2) ty1 ty2
@@ -230,7 +230,6 @@ tc_eq_type keep_syns vis_only orig_ty1 orig_ty2
-- equates 'Specified' and 'Inferred'. Used for printing.
eqForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Bool
-- See Note [ForAllTy and type equality]
--- If you change this, see IMPORTANT NOTE in the above Note
eqForAllVis Required Required = True
eqForAllVis (Invisible _) (Invisible _) = True
eqForAllVis _ _ = False
@@ -240,7 +239,6 @@ eqForAllVis _ _ = False
-- equates 'Specified' and 'Inferred'. Used for printing.
cmpForAllVis :: ForAllTyFlag -> ForAllTyFlag -> Ordering
-- See Note [ForAllTy and type equality]
--- If you change this, see IMPORTANT NOTE in the above Note
cmpForAllVis Required Required = EQ
cmpForAllVis Required (Invisible {}) = LT
cmpForAllVis (Invisible _) Required = GT
@@ -251,12 +249,58 @@ cmpForAllVis (Invisible _) (Invisible _) = EQ
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When we compare (ForAllTy (Bndr tv1 vis1) ty1)
and (ForAllTy (Bndr tv2 vis2) ty2)
-what should we do about `vis1` vs `vis2`.
-
-First, we always compare with `eqForAllVis` and `cmpForAllVis`.
-But what decision do we make?
-
-Should GHC type-check the following program (adapted from #15740)?
+what should we do about `vis1` vs `vis2`?
+
+We had a long debate about this: see #22762 and GHC Proposal 558.
+Here is the conclusion.
+
+* In Haskell, we really do want (forall a. ty) and (forall a -> ty) to be
+ distinct types, not interchangeable. The latter requires a type argument,
+ but the former does not. See GHC Proposal 558.
+
+* We /really/ do not want the typechecker and Core to have different notions of
+ equality. That is, we don't want `tcEqType` and `eqType` to differ. Why not?
+ Not so much because of code duplication but because it is virtually impossible
+ to cleave the two apart. Here is one particularly awkward code path:
+ The type checker calls `substTy`, which calls `mkAppTy`,
+ which calls `mkCastTy`, which calls `isReflexiveCo`, which calls `eqType`.
+
+* Moreover the resolution of the TYPE vs CONSTRAINT story was to make the
+ typechecker and Core have a single notion of equality.
+
+* So in GHC:
+ - `tcEqType` and `eqType` implement the same equality
+ - (forall a. ty) and (forall a -> ty) are distinct types in both Core and typechecker
+ - That is, both `eqType` and `tcEqType` distinguish them.
+
+* But /at representational role/ we can relate the types. That is,
+ (forall a. ty) ~R (forall a -> ty)
+ After all, since types are erased, they are represented the same way.
+ See Note [ForAllCo] and the typing rule for ForAllCo given there
+
+* What about (forall a. ty) and (forall {a}. ty)? See Note [Comparing visibility].
+
+Note [Comparing visibility]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We are sure that we want to distinguish (forall a. ty) and (forall a -> ty); see
+Note [ForAllTy and type equality]. But we have /three/ settings for the ForAllTyFlag:
+ * Specified: forall a. ty
+ * Inferred: forall {a}. ty
+ * Required: forall a -> ty
+
+We could (and perhaps should) distinguish all three. But for now we distinguish
+Required from Specified/Inferred, and ignore the distinction between Specified
+and Inferred.
+
+The answer doesn't matter too much, provided we are consistent. And we are consistent
+because we always compare ForAllTyFlags with
+ * `eqForAllVis`
+ * `cmpForAllVis`.
+(You can only really check this by inspecting all pattern matches on ForAllTyFlags.)
+So if we change the decision, we just need to change those functions.
+
+Why don't we distinguish all three? Should GHC type-check the following program
+(adapted from #15740)?
{-# LANGUAGE PolyKinds, ... #-}
data D a
@@ -303,15 +347,11 @@ That is, we have the following:
| | forall k -> <...> | Yes |
--------------------------------------------------
-IMPORTANT NOTE: if we want to change this decision, ForAllCo will need to carry
-visiblity (by taking a ForAllTyBinder rathre than a TyCoVar), so that
-coercionLKind/RKind build forall types that match (are equal to) the desired
-ones. Otherwise we get an infinite loop in the solver via canEqCanLHSHetero.
Examples: T16946, T15079.
Historical Note [Typechecker equality vs definitional equality]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-This Note describes some history, in case there are vesitges of this
+This Note describes some history, in case there are vestiges of this
history lying around in the code.
Summary: prior to summer 2022, GHC had have two notions of equality
@@ -514,7 +554,7 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
go env (TyVarTy tv1) (TyVarTy tv2)
= liftOrdering $ rnOccL env tv1 `nonDetCmpVar` rnOccR env tv2
go env (ForAllTy (Bndr tv1 vis1) t1) (ForAllTy (Bndr tv2 vis2) t2)
- = liftOrdering (vis1 `cmpForAllVis` vis2)
+ = liftOrdering (vis1 `cmpForAllVis` vis2) -- See Note [ForAllTy and type equality]
`thenCmpTy` go env (varType tv1) (varType tv2)
`thenCmpTy` go (rnBndr2 env tv1 tv2) t1 t2
diff --git a/compiler/GHC/Core/TyCo/FVs.hs b/compiler/GHC/Core/TyCo/FVs.hs
index aa9c04c46bfaa3840e95475125091d1bf3f2a8b8..3dd1759a347a529061c3cd713cc55f86f700666b 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs
+++ b/compiler/GHC/Core/TyCo/FVs.hs
@@ -631,7 +631,7 @@ tyCoFVsOfCo (GRefl _ ty mco) fv_cand in_scope acc
tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
= (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
-tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc
+tyCoFVsOfCo (ForAllCo { fco_tcv = tv, fco_kind = kind_co, fco_body = co }) fv_cand in_scope acc
= (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc
tyCoFVsOfCo (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) fv_cand in_scope acc
= (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2 `unionFV` tyCoFVsOfCo w) fv_cand in_scope acc
@@ -672,7 +672,7 @@ tyCoFVsOfCos (co:cos) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOf
-- | Given a covar and a coercion, returns True if covar is almost devoid in
-- the coercion. That is, covar can only appear in Refl and GRefl.
--- See last wrinkle in Note [Unused coercion variable in ForAllCo] in "GHC.Core.Coercion"
+-- See (FC6) in Note [ForAllCo] in "GHC.Core.TyCo.Rep"
almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo cv co =
almost_devoid_co_var_of_co co cv
@@ -686,7 +686,7 @@ almost_devoid_co_var_of_co (TyConAppCo _ _ cos) cv
almost_devoid_co_var_of_co (AppCo co arg) cv
= almost_devoid_co_var_of_co co cv
&& almost_devoid_co_var_of_co arg cv
-almost_devoid_co_var_of_co (ForAllCo v kind_co co) cv
+almost_devoid_co_var_of_co (ForAllCo { fco_tcv = v, fco_kind = kind_co, fco_body = co }) cv
= almost_devoid_co_var_of_co kind_co cv
&& (v == cv || almost_devoid_co_var_of_co co cv)
almost_devoid_co_var_of_co (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 }) cv
@@ -1109,7 +1109,8 @@ tyConsOfType ty
go_co (GRefl _ ty mco) = go ty `unionUniqSets` go_mco mco
go_co (TyConAppCo _ tc args) = go_tc tc `unionUniqSets` go_cos args
go_co (AppCo co arg) = go_co co `unionUniqSets` go_co arg
- go_co (ForAllCo _ kind_co co) = go_co kind_co `unionUniqSets` go_co co
+ go_co (ForAllCo { fco_kind = kind_co, fco_body = co })
+ = go_co kind_co `unionUniqSets` go_co co
go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r })
= go_co m `unionUniqSets` go_co a `unionUniqSets` go_co r
go_co (AxiomInstCo ax _ args) = go_ax ax `unionUniqSets` go_cos args
@@ -1293,14 +1294,14 @@ occCheckExpand vs_to_avoid ty
go_co cxt (AppCo co arg) = do { co' <- go_co cxt co
; arg' <- go_co cxt arg
; return (AppCo co' arg') }
- go_co cxt@(as, env) (ForAllCo tv kind_co body_co)
+ go_co cxt@(as, env) co@(ForAllCo { fco_tcv = tv, fco_kind = kind_co, fco_body = body_co })
= do { kind_co' <- go_co cxt kind_co
; let tv' = setVarType tv $
coercionLKind kind_co'
env' = extendVarEnv env tv tv'
as' = as `delVarSet` tv
; body' <- go_co (as', env') body_co
- ; return (ForAllCo tv' kind_co' body') }
+ ; return (co { fco_tcv = tv', fco_kind = kind_co', fco_body = body' }) }
go_co cxt co@(FunCo { fco_mult = w, fco_arg = co1 ,fco_res = co2 })
= do { co1' <- go_co cxt co1
; co2' <- go_co cxt co2
diff --git a/compiler/GHC/Core/TyCo/FVs.hs-boot b/compiler/GHC/Core/TyCo/FVs.hs-boot
index bc890c9784655d51c8e0fa2d0bd93a57ebeb8222..af9555fdec672c4884f62cd038b53df4200c3964 100644
--- a/compiler/GHC/Core/TyCo/FVs.hs-boot
+++ b/compiler/GHC/Core/TyCo/FVs.hs-boot
@@ -1,6 +1,8 @@
module GHC.Core.TyCo.FVs where
import GHC.Prelude ( Bool )
+import GHC.Types.Var.Set( TyCoVarSet )
import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type )
noFreeVarsOfType :: Type -> Bool
+tyCoVarsOfType :: Type -> TyCoVarSet
\ No newline at end of file
diff --git a/compiler/GHC/Core/TyCo/Rep.hs b/compiler/GHC/Core/TyCo/Rep.hs
index 245a1c507b89bd5569590a1af2ecd89c5c792c3e..af86de998f5bd70068f2337f301e1ab7044443cb 100644
--- a/compiler/GHC/Core/TyCo/Rep.hs
+++ b/compiler/GHC/Core/TyCo/Rep.hs
@@ -71,12 +71,14 @@ import GHC.Prelude
import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprCo, pprTyLit )
import {-# SOURCE #-} GHC.Builtin.Types
+import {-# SOURCE #-} GHC.Core.TyCo.FVs( tyCoVarsOfType ) -- Use in assertions
import {-# SOURCE #-} GHC.Core.Type( chooseFunTyFlag, typeKind, typeTypeOrConstraint )
-- Transitively pulls in a LOT of stuff, better to break the loop
-- friends:
import GHC.Types.Var
+import GHC.Types.Var.Set( elemVarSet )
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
@@ -152,13 +154,13 @@ data Type
-- for example unsaturated type synonyms
-- can appear as the right hand side of a type synonym.
- | ForAllTy
+ | ForAllTy -- See Note [ForAllTy]
{-# UNPACK #-} !ForAllTyBinder
Type -- ^ A Î type.
- -- Note [When we quantify over a coercion variable]
+ -- See Note [Why ForAllTy can quantify over a coercion variable]
-- INVARIANT: If the binder is a coercion variable, it must
- -- be mentioned in the Type. See
- -- Note [Unused coercion variable in ForAllTy]
+ -- be mentioned in the Type.
+ -- See Note [Unused coercion variable in ForAllTy]
| FunTy -- ^ FUN m t1 t2 Very common, so an important special case
-- See Note [Function types]
@@ -452,7 +454,7 @@ to differ, leading to a contradiction. Thus, co is reflexive.
Accordingly, by eliminating reflexive casts, splitTyConApp need not worry
about outermost casts to uphold (EQ). Eliminating reflexive casts is done
-in mkCastTy. This is (EQ1) below.
+in mkCastTy. This is (EQ2) below.
Unfortunately, that's not the end of the story. Consider comparing
(T a b c) =? (T a b |> (co -> <Type>)) (c |> co)
@@ -475,7 +477,7 @@ our (EQ) property.
In order to detect reflexive casts reliably, we must make sure not
to have nested casts: we update (t |> co1 |> co2) to (t |> (co1 `TransCo` co2)).
-This is (EQ2) below.
+This is (EQ3) below.
One other troublesome case is ForAllTy. See Note [Weird typing rule for ForAllTy].
The kind of the body is the same as the kind of the ForAllTy. Accordingly,
@@ -488,9 +490,9 @@ This is done in mkCastTy.
In sum, in order to uphold (EQ), we need the following invariants:
- (EQ1) No decomposable CastTy to the left of an AppTy, where a decomposable
- cast is one that relates either a FunTy to a FunTy or a
- ForAllTy to a ForAllTy.
+ (EQ1) No decomposable CastTy to the left of an AppTy,
+ where a "decomposable cast" is one that relates
+ either a FunTy to a FunTy, or a ForAllTy to a ForAllTy.
(EQ2) No reflexive casts in CastTy.
(EQ3) No nested CastTys.
(EQ4) No CastTy over (ForAllTy (Bndr tyvar vis) body).
@@ -517,8 +519,22 @@ In order to compare FunTys while respecting how they could
expand into TyConApps, we must check
the kinds of the arg and the res.
-Note [When we quantify over a coercion variable]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [ForAllTy]
+~~~~~~~~~~~~~~~
+A (ForAllTy (Bndr tcv vis) ty) can quantify over a TyVar or, less commonly, a CoVar.
+See Note [Why ForAllTy can quantify over a coercion variable] for why we need the latter.
+
+(FT1) Invariant: See Note [Weird typing rule for ForAllTy]
+
+(FT2) Invariant: in (ForAllTy (Bndr tcv vis) ty),
+ if tcv is a CoVar, then vis = coreTyLamForAllTyFlag.
+ Visibility is not important for coercion abstractions,
+ because they are not user-visible.
+
+(FT3) Invariant: see Note [Unused coercion variable in ForAllTy]
+
+Note [Why ForAllTy can quantify over a coercion variable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The ForAllTyBinder in a ForAllTy can be (most often) a TyVar or (rarely)
a CoVar. We support quantifying over a CoVar here in order to support
a homogeneous (~#) relation (someday -- not yet implemented). Here is
@@ -541,10 +557,8 @@ Note that we must cast `a` by a cv bound in the same type in order to
make this work out.
See also https://gitlab.haskell.org/ghc/ghc/-/wikis/dependent-haskell/phase2
-which gives a general road map that covers this space.
-
-Having this feature in Core does *not* mean we have it in source Haskell.
-See #15710 about that.
+which gives a general road map that covers this space. Having this feature in
+Core does *not* mean we have it in source Haskell. See #15710 about that.
Note [Unused coercion variable in ForAllTy]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -775,7 +789,17 @@ tcMkScaledFunTys tys ty = foldr mk ty tys
-- | Like 'mkTyCoForAllTy', but does not check the occurrence of the binder
-- See Note [Unused coercion variable in ForAllTy]
mkForAllTy :: ForAllTyBinder -> Type -> Type
-mkForAllTy = ForAllTy
+mkForAllTy bndr body
+ = assertPpr (good_bndr bndr) (ppr bndr <+> ppr body) $
+ ForAllTy bndr body
+ where
+ -- Check ForAllTy invariants
+ good_bndr (Bndr cv vis)
+ | isCoVar cv = vis == coreTyLamForAllTyFlag
+ -- See (FT2) in Note [ForAllTy]
+ && (cv `elemVarSet` tyCoVarsOfType body)
+ -- See (FT3) in Note [ForAllTy]
+ | otherwise = True
-- | Wraps foralls over the type using the provided 'TyCoVar's from left to right
mkForAllTys :: [ForAllTyBinder] -> Type -> Type
@@ -849,8 +873,14 @@ data Coercion
| AppCo Coercion CoercionN -- lift AppTy
-- AppCo :: e -> N -> e
- -- See Note [Forall coercions]
- | ForAllCo TyCoVar KindCoercion Coercion
+ -- See Note [ForAllCo]
+ | ForAllCo
+ { fco_tcv :: TyCoVar
+ , fco_visL :: !ForAllTyFlag -- Visibility of coercionLKind
+ , fco_visR :: !ForAllTyFlag -- Visibility of coercionRKind
+ -- See (FC7) of Note [ForAllCo]
+ , fco_kind :: KindCoercion
+ , fco_body :: Coercion }
-- ForAllCo :: _ -> N -> e -> e
| FunCo -- FunCo :: "e" -> N/P -> e -> e -> e
@@ -1159,43 +1189,105 @@ among branches, but that doesn't quite concern us here.)
The Int in the AxiomInstCo constructor is the 0-indexed number
of the chosen branch.
-Note [Forall coercions]
-~~~~~~~~~~~~~~~~~~~~~~~
+Note [ForAllCo]
+~~~~~~~~~~~~~~~
+See also Note [ForAllTy and type equality] in GHC.Core.TyCo.Compare.
+
Constructing coercions between forall-types can be a bit tricky,
because the kinds of the bound tyvars can be different.
The typing rule is:
-
- kind_co : k1 ~ k2
- tv1:k1 |- co : t1 ~ t2
- -------------------------------------------------------------------
- ForAllCo tv1 kind_co co : all tv1:k1. t1 ~
- all tv1:k2. (t2[tv1 |-> tv1 |> sym kind_co])
-
-First, the TyCoVar stored in a ForAllCo is really an optimisation: this field
-should be a Name, as its kind is redundant. Thinking of the field as a Name
-is helpful in understanding what a ForAllCo means.
-The kind of TyCoVar always matches the left-hand kind of the coercion.
-
-The idea is that kind_co gives the two kinds of the tyvar. See how, in the
-conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
-
-Of course, a type variable can't have different kinds at the same time. So,
-we arbitrarily prefer the first kind when using tv1 in the inner coercion
-co, which shows that t1 equals t2.
-
-The last wrinkle is that we need to fix the kinds in the conclusion. In
-t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
-the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
-(tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
-mentions the same name with different kinds, but it *is* well-kinded, noting
-that `(tv1:k2) |> sym kind_co` has kind k1.
-
-This all really would work storing just a Name in the ForAllCo. But we can't
-add Names to, e.g., VarSets, and there generally is just an impedance mismatch
-in a bunch of places. So we use tv1. When we need tv2, we can use
-setTyVarKind.
+ kind_co : k1 ~N k2
+ tv1:k1 |- co : t1 ~r t2
+ if r=N, then vis1=vis2
+ ------------------------------------
+ ForAllCo (tv1:k1) vis1 vis2 kind_co co
+ : forall (tv1:k1) <vis1>. t1
+ ~r
+ forall (tv1:k2) <vis2>. (t2[tv1 |-> (tv1:k2) |> sym kind_co])
+
+Several things to note here
+
+(FC1) First, the TyCoVar stored in a ForAllCo is really just a convenience: this
+ field should be a Name, as its kind is redundant. Thinking of the field as a
+ Name is helpful in understanding what a ForAllCo means. The kind of TyCoVar
+ always matches the left-hand kind of the coercion.
+
+ * The idea is that kind_co gives the two kinds of the tyvar. See how, in the
+ conclusion, tv1 is assigned kind k1 on the left but kind k2 on the right.
+
+ * Of course, a type variable can't have different kinds at the same time.
+ So, in `co` itself we use (tv1 : k1); hence the premise
+ tv1:k1 |- co : t1 ~r t2
+
+ * The last wrinkle is that we need to fix the kinds in the conclusion. In
+ t2, tv1 is assumed to have kind k1, but it has kind k2 in the conclusion of
+ the rule. So we do a kind-fixing substitution, replacing (tv1:k1) with
+ (tv1:k2) |> sym kind_co. This substitution is slightly bizarre, because it
+ mentions the same name with different kinds, but it *is* well-kinded, noting
+ that `(tv1:k2) |> sym kind_co` has kind k1.
+
+ We could instead store just a Name in the ForAllCo, and it might even be
+ more efficient to do so. But we can't add Names to, e.g., VarSets, and
+ there generally is just an impedance mismatch in a bunch of places. So we
+ use tv1. When we need tv2, we can use setTyVarKind.
+
+(FC2) Note that the kind coercion must be Nominal; and that the role `r` of
+ the final coercion is the same as that of the body coercion.
+
+(FC3) A ForAllCo allows casting between visibilities. For example:
+ ForAllCo a Required Specified (SubCo (Refl ty))
+ : (forall a -> ty) ~R (forall a. ty)
+ But you can only cast between visiblities at Representational role;
+ Hence the premise
+ if r=N, then vis1=vis2
+ in the typing rule. See also Note [ForAllTy and type equality] in
+ GHC.Core.TyCo.Compare.
+
+(FC4) A lambda term (Lam a e) has type (forall a. ty), with visibility
+ flag `GHC.Type.Var.coreTyLamForAllTyFlag`, not (forall a -> ty).
+ See `GHC.Type.Var.coreTyLamForAllTyFlag` and `GHC.Core.Utils.mkLamType`.
+ The only way to get a term of type (forall a -> ty) is to cast a lambda.
+
+(FC5) In a /type/, in (ForAllTy cv ty) where cv is a CoVar, we insist that
+ `cv` must appear free in `ty`; see Note [Unused coercion variable in ForAllTy]
+ in GHC.Core.TyCo.Rep for the motivation. If it does not appear free,
+ use FunTy.
+
+ However we do /not/ impose the same restriction on ForAllCo in /coercions/.
+ Instead, in coercionLKind and coercionRKind, we use mkTyCoForAllTy to perform
+ the check and construct a FunTy when necessary. Why?
+ * For a coercion, all that matters is its kind, So ForAllCo vs FunCo does not
+ make a difference.
+ * Even if cv occurs in body_co, it is possible that cv does not occur in the kind
+ of body_co. Therefore the check in coercionKind is inevitable.
+
+(FC6) Invariant: in a ForAllCo where fco_tcv is a coercion variable, `cv`,
+ we insist that `cv` appears only in positions that are erased. In fact we use
+ a conservative approximation of this: we require that
+ (almostDevoidCoVarOfCo cv fco_body)
+ holds. This function checks that `cv` appers only within the type in a Refl
+ node and under a GRefl node (including in the Coercion stored in a GRefl).
+ It's possible other places are OK, too, but this is a safe approximation.
+
+ Why all this fuss? See Section 5.8.5.2 of Richard's thesis. The idea is that
+ we cannot prove that the type system is consistent with unrestricted use of this
+ cv; the consistency proof uses an untyped rewrite relation that works over types
+ with all coercions and casts removed. So, we can allow the cv to appear only in
+ positions that are erased.
+
+ Sadly, with heterogeneous equality, this restriction might be able to be
+ violated; Richard's thesis is unable to prove that it isn't. Specifically, the
+ liftCoSubst function might create an invalid coercion. Because a violation of
+ the restriction might lead to a program that "goes wrong", it is checked all
+ the time, even in a production compiler and without -dcore-lint. We *have*
+ proved that the problem does not occur with homogeneous equality, so this
+ check can be dropped once ~# is made to be homogeneous.
+
+(FC7) Invariant: in a ForAllCo, if fco_tcv is a CoVar, then
+ fco_visL = fco_visR = coreTyLamForAllTyFlag
+ c.f. (FT2) in Note [ForAllTy]
Note [Predicate coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1760,7 +1852,7 @@ foldTyCo (TyCoFolder { tcf_view = view
go_co env (FunCo { fco_mult = cw, fco_arg = c1, fco_res = c2 })
= go_co env cw `mappend` go_co env c1 `mappend` go_co env c2
- go_co env (ForAllCo tv kind_co co)
+ go_co env (ForAllCo tv _vis1 _vis2 kind_co co)
= go_co env kind_co `mappend` go_ty env (varType tv)
`mappend` go_co env' co
where
@@ -1815,7 +1907,8 @@ coercionSize (GRefl _ ty MRefl) = typeSize ty
coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co
coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (AppCo co arg) = coercionSize co + coercionSize arg
-coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h
+coercionSize (ForAllCo { fco_kind = h, fco_body = co })
+ = 1 + coercionSize co + coercionSize h
coercionSize (FunCo _ _ _ w c1 c2) = 1 + coercionSize c1 + coercionSize c2
+ coercionSize w
coercionSize (CoVarCo _) = 1
diff --git a/compiler/GHC/Core/TyCo/Subst.hs b/compiler/GHC/Core/TyCo/Subst.hs
index 4224bd127bc39aed9c7afd4b5af23ff401b3dac3..c867ed2e76f8b1104f2b2547b0ec910a765259b0 100644
--- a/compiler/GHC/Core/TyCo/Subst.hs
+++ b/compiler/GHC/Core/TyCo/Subst.hs
@@ -535,7 +535,8 @@ Note [Sym and ForAllCo]
In OptCoercion, we try to push "sym" out to the leaves of a coercion. But,
how do we push sym into a ForAllCo? It's a little ugly.
-Here is the typing rule:
+Ignoring visibility, here is the typing rule
+(see Note [ForAllCo] in GHC.Core.TyCo.Rep).
h : k1 ~# k2
(tv : k1) |- g : ty1 ~# ty2
@@ -889,10 +890,10 @@ subst_co subst co
go (TyConAppCo r tc args)= let args' = map go args
in args' `seqList` mkTyConAppCo r tc args'
go (AppCo co arg) = (mkAppCo $! go co) $! go arg
- go (ForAllCo tv kind_co co)
+ go (ForAllCo tv visL visR kind_co co)
= case substForAllCoBndrUnchecked subst tv kind_co of
(subst', tv', kind_co') ->
- ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co
+ ((mkForAllCo $! tv') visL visR $! kind_co') $! subst_co subst' co
go (FunCo r afl afr w co1 co2) = ((mkFunCo2 r afl afr $! go w) $! go co1) $! go co2
go (CoVarCo cv) = substCoVar subst cv
go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
diff --git a/compiler/GHC/Core/TyCo/Tidy.hs b/compiler/GHC/Core/TyCo/Tidy.hs
index bfd7e4c7ccb0e3b72957fabd8a5c690113e1056c..e5e091a30af9a0297196ec2361260996acaee748 100644
--- a/compiler/GHC/Core/TyCo/Tidy.hs
+++ b/compiler/GHC/Core/TyCo/Tidy.hs
@@ -228,7 +228,8 @@ tidyCo env@(_, subst) co
go (GRefl r ty mco) = (GRefl r $! tidyType env ty) $! go_mco mco
go (TyConAppCo r tc cos) = TyConAppCo r tc $! strictMap go cos
go (AppCo co1 co2) = (AppCo $! go co1) $! go co2
- go (ForAllCo tv h co) = ((ForAllCo $! tvp) $! (go h)) $! (tidyCo envp co)
+ go (ForAllCo tv visL visR h co)
+ = ((((ForAllCo $! tvp) $! visL) $! visR) $! (go h)) $! (tidyCo envp co)
where (envp, tvp) = tidyVarBndr env tv
-- the case above duplicates a bit of work in tidying h and the kind
-- of tv. But the alternative is to use coercionKind, which seems worse.
diff --git a/compiler/GHC/Core/Type.hs b/compiler/GHC/Core/Type.hs
index 447b77eaae5863f39fff1a21ae982267027235e5..0adf4cc74e72173f8ebf189555957899bb589b2a 100644
--- a/compiler/GHC/Core/Type.hs
+++ b/compiler/GHC/Core/Type.hs
@@ -48,11 +48,11 @@ module GHC.Core.Type (
mkForAllTy, mkForAllTys, mkInvisForAllTys, mkTyCoInvForAllTys,
mkSpecForAllTy, mkSpecForAllTys,
- mkVisForAllTys, mkTyCoInvForAllTy,
+ mkVisForAllTys, mkTyCoForAllTy, mkTyCoForAllTys, mkTyCoInvForAllTy,
mkInfForAllTy, mkInfForAllTys,
splitForAllTyCoVars, splitForAllTyVars,
splitForAllReqTyBinders, splitForAllInvisTyBinders,
- splitForAllForAllTyBinders,
+ splitForAllForAllTyBinders, splitForAllForAllTyBinder_maybe,
splitForAllTyCoVar_maybe, splitForAllTyCoVar,
splitForAllTyVar_maybe, splitForAllCoVar_maybe,
splitPiTy_maybe, splitPiTy, splitPiTys,
@@ -549,9 +549,10 @@ expandTypeSynonyms ty
= mkTyConAppCo r tc (map (go_co subst) args)
go_co subst (AppCo co arg)
= mkAppCo (go_co subst co) (go_co subst arg)
- go_co subst (ForAllCo tv kind_co co)
+ go_co subst (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co })
= let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
- mkForAllCo tv' kind_co' (go_co subst' co)
+ mkForAllCo tv' visL visR kind_co' (go_co subst' co)
go_co subst (FunCo r afl afr w co1 co2)
= mkFunCo2 r afl afr (go_co subst w) (go_co subst co1) (go_co subst co2)
go_co subst (CoVarCo cv)
@@ -850,7 +851,7 @@ on all variables and binding sites. Primarily used for zonking.
Note [Efficiency for ForAllCo case of mapTyCoX]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-As noted in Note [Forall coercions] in GHC.Core.TyCo.Rep, a ForAllCo is a bit redundant.
+As noted in Note [ForAllCo] in GHC.Core.TyCo.Rep, a ForAllCo is a bit redundant.
It stores a TyCoVar and a Coercion, where the kind of the TyCoVar always matches
the left-hand kind of the coercion. This is convenient lots of the time, but
not when mapping a function over a coercion.
@@ -991,11 +992,12 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
| otherwise
= mkTyConAppCo r tc <$> go_cos env cos
- go_co !env (ForAllCo tv kind_co co)
+ go_co !env (ForAllCo { fco_tcv = tv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co })
= do { kind_co' <- go_co env kind_co
- ; tycobinder env tv Inferred $ \env' tv' -> do
+ ; tycobinder env tv visL $ \env' tv' -> do
; co' <- go_co env' co
- ; return $ mkForAllCo tv' kind_co' co' }
+ ; return $ mkForAllCo tv' visL visR kind_co' co' }
-- See Note [Efficiency for ForAllCo case of mapTyCoX]
go_prov !env (PhantomProv co) = PhantomProv <$> go_co env co
@@ -1063,14 +1065,13 @@ The type (Proxy (Eq Int => Int)) is only accepted with -XImpredicativeTypes,
but suppose we want that. But then in the call to 'i', we end
up decomposing (Eq Int => Int), and we definitely don't want that.
-This really only applies to the type checker; in Core, '=>' and '->'
-are the same, as are 'Constraint' and '*'. But for now I've put
-the test in splitAppTyNoView_maybe, which applies throughout, because
-the other calls to splitAppTy are in GHC.Core.Unify, which is also used by
-the type checker (e.g. when matching type-function equations).
-
We are willing to split (t1 -=> t2) because the argument is still of
kind Type, not Constraint. So the criterion is isVisibleFunArg.
+
+In Core there is no real reason to avoid such decomposition. But for now I've
+put the test in splitAppTyNoView_maybe, which applies throughout, because the
+other calls to splitAppTy are in GHC.Core.Unify, which is also used by the
+type checker (e.g. when matching type-function equations).
-}
-- | Applies a type to another, as in e.g. @k a@
@@ -1763,14 +1764,25 @@ tyConBindersPiTyBinders = map to_tyb
to_tyb (Bndr tv (NamedTCB vis)) = Named (Bndr tv vis)
to_tyb (Bndr tv AnonTCB) = Anon (tymult (varType tv)) FTF_T_T
--- | Make a dependent forall over an 'Inferred' variable
-mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
-mkTyCoInvForAllTy tv ty
+-- | Make a dependent forall over a TyCoVar
+mkTyCoForAllTy :: TyCoVar -> ForAllTyFlag -> Type -> Type
+mkTyCoForAllTy tv vis ty
| isCoVar tv
, not (tv `elemVarSet` tyCoVarsOfType ty)
+ -- Maintain ForAllTy's invariants
+ -- See Note [Unused coercion variable in ForAllTy] in GHC.Core.TyCo.Rep
= mkVisFunTyMany (varType tv) ty
| otherwise
- = ForAllTy (Bndr tv Inferred) ty
+ = ForAllTy (mkForAllTyBinder vis tv) ty
+
+-- | Make a dependent forall over a TyCoVar
+mkTyCoForAllTys :: [ForAllTyBinder] -> Type -> Type
+mkTyCoForAllTys bndrs ty
+ = foldr (\(Bndr var vis) -> mkTyCoForAllTy var vis) ty bndrs
+
+-- | Make a dependent forall over an 'Inferred' variable
+mkTyCoInvForAllTy :: TyCoVar -> Type -> Type
+mkTyCoInvForAllTy tv ty = mkTyCoForAllTy tv Inferred ty
-- | Like 'mkTyCoInvForAllTy', but tv should be a tyvar
mkInfForAllTy :: TyVar -> Type -> Type
@@ -1937,14 +1949,20 @@ dropForAlls ty = go ty
go ty | Just ty' <- coreView ty = go ty'
go res = res
--- | Attempts to take a forall type apart, but only if it's a proper forall,
--- with a named binder
+-- | Attempts to take a ForAllTy apart, returning the full ForAllTyBinder
+splitForAllForAllTyBinder_maybe :: Type -> Maybe (ForAllTyBinder, Type)
+splitForAllForAllTyBinder_maybe ty
+ | ForAllTy bndr inner_ty <- coreFullView ty = Just (bndr, inner_ty)
+ | otherwise = Nothing
+
+
+-- | Attempts to take a ForAllTy apart, returning the Var
splitForAllTyCoVar_maybe :: Type -> Maybe (TyCoVar, Type)
splitForAllTyCoVar_maybe ty
| ForAllTy (Bndr tv _) inner_ty <- coreFullView ty = Just (tv, inner_ty)
| otherwise = Nothing
--- | Like 'splitForAllTyCoVar_maybe', but only returns Just if it is a tyvar binder.
+-- | Attempts to take a ForAllTy apart, but only if the binder is a TyVar
splitForAllTyVar_maybe :: Type -> Maybe (TyVar, Type)
splitForAllTyVar_maybe ty
| ForAllTy (Bndr tv _) inner_ty <- coreFullView ty
diff --git a/compiler/GHC/Core/Unify.hs b/compiler/GHC/Core/Unify.hs
index eefb9e35ac174ebf83e7aa9dfdb8b39cce7aa96f..e268bee26aed5a3babfcfe9cea2eb665e3c9b8c6 100644
--- a/compiler/GHC/Core/Unify.hs
+++ b/compiler/GHC/Core/Unify.hs
@@ -1675,10 +1675,14 @@ ty_co_match menv subst (FunTy { ft_mult = w, ft_arg = ty1, ft_res = ty2 })
-- NB: we include the RuntimeRep arguments in the matching;
-- not doing so caused #21205.
-ty_co_match menv subst (ForAllTy (Bndr tv1 _) ty1)
- (ForAllCo tv2 kind_co2 co2)
+ty_co_match menv subst (ForAllTy (Bndr tv1 vis1t) ty1)
+ (ForAllCo tv2 vis1c vis2c kind_co2 co2)
lkco rkco
| isTyVar tv1 && isTyVar tv2
+ , vis1t == vis1c && vis1c == vis2c -- Is this necessary?
+ -- Is this visibility check necessary? @rae says: yes, I think the
+ -- check is necessary, if we're caring about visibility (and we are).
+ -- But ty_co_match is a dark and not important corner.
= do { subst1 <- ty_co_match menv subst (tyVarKind tv1) kind_co2
ki_ki_co ki_ki_co
; let rn_env0 = me_env menv
@@ -1778,9 +1782,10 @@ pushRefl co =
-> Just (FunCo r af af (mkReflCo r w) (mkReflCo r ty1) (mkReflCo r ty2))
Just (TyConApp tc tys, r)
-> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRoleListX r tc) tys))
- Just (ForAllTy (Bndr tv _) ty, r)
- -> Just (ForAllCo tv (mkNomReflCo (varType tv)) (mkReflCo r ty))
- -- NB: NoRefl variant. Otherwise, we get a loop!
+ Just (ForAllTy (Bndr tv vis) ty, r)
+ -> Just (ForAllCo { fco_tcv = tv, fco_visL = vis, fco_visR = vis
+ , fco_kind = mkNomReflCo (varType tv)
+ , fco_body = mkReflCo r ty })
_ -> Nothing
{-
diff --git a/compiler/GHC/Core/Utils.hs b/compiler/GHC/Core/Utils.hs
index efd74a3a67159d55ee176ca05fa80e38c6b11d55..89439af515139da9d5a26a12782d80e03a21eb18 100644
--- a/compiler/GHC/Core/Utils.hs
+++ b/compiler/GHC/Core/Utils.hs
@@ -21,7 +21,8 @@ module GHC.Core.Utils (
scaleAltsBy,
-- * Properties of expressions
- exprType, coreAltType, coreAltsType, mkLamType, mkLamTypes,
+ exprType, coreAltType, coreAltsType,
+ mkLamType, mkLamTypes,
mkFunctionType,
exprIsDupable, exprIsTrivial, getIdFromTrivialExpr,
getIdFromTrivialExpr_maybe,
@@ -161,17 +162,20 @@ mkLamType :: HasDebugCallStack => Var -> Type -> Type
-- ^ Makes a @(->)@ type or an implicit forall type, depending
-- on whether it is given a type variable or a term variable.
-- This is used, for example, when producing the type of a lambda.
--- Always uses Inferred binders.
+--
mkLamTypes :: [Var] -> Type -> Type
-- ^ 'mkLamType' for multiple type or value arguments
mkLamType v body_ty
| isTyVar v
- = mkForAllTy (Bndr v Inferred) body_ty
+ = mkForAllTy (Bndr v coreTyLamForAllTyFlag) body_ty
+ -- coreTyLamForAllTyFlag: see (FC4) in Note [ForAllCo]
+ -- in GHC.Core.TyCo.Rep
| isCoVar v
, v `elemVarSet` tyCoVarsOfType body_ty
- = mkForAllTy (Bndr v Required) body_ty
+ -- See Note [Unused coercion variable in ForAllTy] in GHC.Core.TyCo.Rep
+ = mkForAllTy (Bndr v coreTyLamForAllTyFlag) body_ty
| otherwise
= mkFunctionType (varMult v) (varType v) body_ty
diff --git a/compiler/GHC/CoreToIface.hs b/compiler/GHC/CoreToIface.hs
index c0b66e204913b64c20bc658e09e539bf01df9c77..16707c92a0c6c22d1bae0ed8213a121fdff667d5 100644
--- a/compiler/GHC/CoreToIface.hs
+++ b/compiler/GHC/CoreToIface.hs
@@ -309,9 +309,12 @@ toIfaceCoercionX fr co
go (FunCo { fco_role = r, fco_mult = w, fco_arg = co1, fco_res = co2 })
= IfaceFunCo r (go w) (go co1) (go co2)
- go (ForAllCo tv k co) = IfaceForAllCo (toIfaceBndr tv)
- (toIfaceCoercionX fr' k)
- (toIfaceCoercionX fr' co)
+ go (ForAllCo tv visL visR k co)
+ = IfaceForAllCo (toIfaceBndr tv)
+ visL
+ visR
+ (toIfaceCoercionX fr' k)
+ (toIfaceCoercionX fr' co)
where
fr' = fr `delVarSet` tv
diff --git a/compiler/GHC/Iface/Rename.hs b/compiler/GHC/Iface/Rename.hs
index b372e7a1d91ad0313c87d74edcad74088b7b1d5a..fe08cad0599cd8dd3b7433caa2c91ac769b2d7b8 100644
--- a/compiler/GHC/Iface/Rename.hs
+++ b/compiler/GHC/Iface/Rename.hs
@@ -668,8 +668,9 @@ rnIfaceCo (IfaceTyConAppCo role tc cos)
= IfaceTyConAppCo role <$> rnIfaceTyCon tc <*> mapM rnIfaceCo cos
rnIfaceCo (IfaceAppCo co1 co2)
= IfaceAppCo <$> rnIfaceCo co1 <*> rnIfaceCo co2
-rnIfaceCo (IfaceForAllCo bndr co1 co2)
- = IfaceForAllCo <$> rnIfaceBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2
+rnIfaceCo (IfaceForAllCo bndr visL visR co1 co2)
+ = (\bndr' co1' co2' -> IfaceForAllCo bndr' visL visR co1' co2')
+ <$> rnIfaceBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceFreeCoVar c) = pure (IfaceFreeCoVar c)
rnIfaceCo (IfaceCoVarCo lcl) = IfaceCoVarCo <$> pure lcl
rnIfaceCo (IfaceHoleCo lcl) = IfaceHoleCo <$> pure lcl
diff --git a/compiler/GHC/Iface/Syntax.hs b/compiler/GHC/Iface/Syntax.hs
index 289997f3aaf9b8b64beeabaad0a7ea9552bbc5ea..3a7795a92d3b6fa478ba5de5bb642a0e4fcf04f2 100644
--- a/compiler/GHC/Iface/Syntax.hs
+++ b/compiler/GHC/Iface/Syntax.hs
@@ -1766,7 +1766,7 @@ freeNamesIfCoercion (IfaceTyConAppCo _ tc cos)
= freeNamesIfTc tc &&& fnList freeNamesIfCoercion cos
freeNamesIfCoercion (IfaceAppCo c1 c2)
= freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
-freeNamesIfCoercion (IfaceForAllCo _ kind_co co)
+freeNamesIfCoercion (IfaceForAllCo _tcv _visL _visR kind_co co)
= freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co
freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet
freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet
diff --git a/compiler/GHC/Iface/Type.hs b/compiler/GHC/Iface/Type.hs
index 6243e40470264218f4c6f924fde4470c5e01128f..1ea0307fc5346ec90db2218412e65e2766ea90ed 100644
--- a/compiler/GHC/Iface/Type.hs
+++ b/compiler/GHC/Iface/Type.hs
@@ -381,7 +381,7 @@ data IfaceCoercion
| IfaceFunCo Role IfaceCoercion IfaceCoercion IfaceCoercion
| IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion]
| IfaceAppCo IfaceCoercion IfaceCoercion
- | IfaceForAllCo IfaceBndr IfaceCoercion IfaceCoercion
+ | IfaceForAllCo IfaceBndr !ForAllTyFlag !ForAllTyFlag IfaceCoercion IfaceCoercion
| IfaceCoVarCo IfLclName
| IfaceAxiomInstCo IfExtName BranchIndex [IfaceCoercion]
| IfaceAxiomRuleCo IfLclName [IfaceCoercion]
@@ -1282,7 +1282,8 @@ pprIfaceForAllPartMust :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
pprIfaceForAllPartMust tvs ctxt sdoc
= ppr_iface_forall_part ShowForAllMust tvs ctxt sdoc
-pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion)] -> SDoc -> SDoc
+pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)]
+ -> SDoc -> SDoc
pprIfaceForAllCoPart tvs sdoc
= sep [ pprIfaceForAllCo tvs, sdoc ]
@@ -1321,11 +1322,11 @@ ppr_itv_bndrs all_bndrs@(bndr@(Bndr _ vis) : bndrs) vis1
| otherwise = (all_bndrs, [])
ppr_itv_bndrs [] _ = ([], [])
-pprIfaceForAllCo :: [(IfLclName, IfaceCoercion)] -> SDoc
+pprIfaceForAllCo :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc
pprIfaceForAllCo [] = empty
pprIfaceForAllCo tvs = text "forall" <+> pprIfaceForAllCoBndrs tvs <> dot
-pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion)] -> SDoc
+pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc
pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
@@ -1340,9 +1341,15 @@ pprIfaceForAllBndr bndr =
-- See Note [Suppressing binder signatures]
suppress_sig = SuppressBndrSig False
-pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion) -> SDoc
-pprIfaceForAllCoBndr (tv, kind_co)
- = parens (ppr tv <+> dcolon <+> pprIfaceCoercion kind_co)
+pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag) -> SDoc
+pprIfaceForAllCoBndr (tv, kind_co, visL, visR)
+ = parens (ppr tv <> pp_vis <+> dcolon <+> pprIfaceCoercion kind_co)
+ where
+ pp_vis | visL == coreTyLamForAllTyFlag
+ , visR == coreTyLamForAllTyFlag
+ = empty
+ | otherwise
+ = ppr visL <> char '~' <> ppr visR -- "[spec]~[reqd]"
-- | Show forall flag
--
@@ -1850,14 +1857,15 @@ ppr_co ctxt_prec (IfaceAppCo co1 co2)
ppr_co funPrec co1 <+> pprParendIfaceCoercion co2
ppr_co ctxt_prec co@(IfaceForAllCo {})
= maybeParen ctxt_prec funPrec $
+ -- FIXME: collect and pretty-print visibility info?
pprIfaceForAllCoPart tvs (pprIfaceCoercion inner_co)
where
(tvs, inner_co) = split_co co
- split_co (IfaceForAllCo (IfaceTvBndr (name, _)) kind_co co')
- = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
- split_co (IfaceForAllCo (IfaceIdBndr (_, name, _)) kind_co co')
- = let (tvs, co'') = split_co co' in ((name,kind_co):tvs,co'')
+ split_co (IfaceForAllCo (IfaceTvBndr (name, _)) visL visR kind_co co')
+ = let (tvs, co'') = split_co co' in ((name,kind_co,visL,visR):tvs,co'')
+ split_co (IfaceForAllCo (IfaceIdBndr (_, name, _)) visL visR kind_co co')
+ = let (tvs, co'') = split_co co' in ((name,kind_co,visL,visR):tvs,co'')
split_co co' = ([], co')
-- Why these three? See Note [Free tyvars in IfaceType]
@@ -2163,9 +2171,11 @@ instance Binary IfaceCoercion where
putByte bh 5
put_ bh a
put_ bh b
- put_ bh (IfaceForAllCo a b c) = do
+ put_ bh (IfaceForAllCo a visL visR b c) = do
putByte bh 6
put_ bh a
+ put_ bh visL
+ put_ bh visR
put_ bh b
put_ bh c
put_ bh (IfaceCoVarCo a) = do
@@ -2239,9 +2249,11 @@ instance Binary IfaceCoercion where
b <- get bh
return $ IfaceAppCo a b
6 -> do a <- get bh
+ visL <- get bh
+ visR <- get bh
b <- get bh
c <- get bh
- return $ IfaceForAllCo a b c
+ return $ IfaceForAllCo a visL visR b c
7 -> do a <- get bh
return $ IfaceCoVarCo a
8 -> do a <- get bh
@@ -2339,7 +2351,7 @@ instance NFData IfaceCoercion where
IfaceFunCo f1 f2 f3 f4 -> f1 `seq` rnf f2 `seq` rnf f3 `seq` rnf f4
IfaceTyConAppCo f1 f2 f3 -> f1 `seq` rnf f2 `seq` rnf f3
IfaceAppCo f1 f2 -> rnf f1 `seq` rnf f2
- IfaceForAllCo f1 f2 f3 -> rnf f1 `seq` rnf f2 `seq` rnf f3
+ IfaceForAllCo f1 f2 f3 f4 f5 -> rnf f1 `seq` rnf f2 `seq` rnf f3 `seq` rnf f4 `seq` rnf f5
IfaceCoVarCo f1 -> rnf f1
IfaceAxiomInstCo f1 f2 f3 -> rnf f1 `seq` rnf f2 `seq` rnf f3
IfaceAxiomRuleCo f1 f2 -> rnf f1 `seq` rnf f2
diff --git a/compiler/GHC/IfaceToCore.hs b/compiler/GHC/IfaceToCore.hs
index 814fce49badc5cb73502c29781710cf119f11b3a..1d6c49b6b2a18ee13228ba211bfb9736718fc39a 100644
--- a/compiler/GHC/IfaceToCore.hs
+++ b/compiler/GHC/IfaceToCore.hs
@@ -1463,9 +1463,9 @@ tcIfaceCo = go
go (IfaceFunCo r w c1 c2) = mkFunCoNoFTF r <$> go w <*> go c1 <*> go c2
go (IfaceTyConAppCo r tc cs) = TyConAppCo r <$> tcIfaceTyCon tc <*> mapM go cs
go (IfaceAppCo c1 c2) = AppCo <$> go c1 <*> go c2
- go (IfaceForAllCo tv k c) = do { k' <- go k
+ go (IfaceForAllCo tv visL visR k c) = do { k' <- go k
; bindIfaceBndr tv $ \ tv' ->
- ForAllCo tv' k' <$> go c }
+ ForAllCo tv' visL visR k' <$> go c }
go (IfaceCoVarCo n) = CoVarCo <$> go_var n
go (IfaceAxiomInstCo n i cs) = AxiomInstCo <$> tcIfaceCoAxiom n <*> pure i <*> mapM go cs
go (IfaceUnivCo p r t1 t2) = UnivCo <$> tcIfaceUnivCoProv p <*> pure r
diff --git a/compiler/GHC/Tc/Solver/Equality.hs b/compiler/GHC/Tc/Solver/Equality.hs
index 0dc574723279862183cb237343f853b1d437df16..c8bb3a5eeb85bbbabfc1e5623f27403a7fa32bd2 100644
--- a/compiler/GHC/Tc/Solver/Equality.hs
+++ b/compiler/GHC/Tc/Solver/Equality.hs
@@ -21,6 +21,7 @@ import GHC.Tc.Utils.Unify
import GHC.Tc.Utils.TcType
import GHC.Tc.Instance.Family ( tcTopNormaliseNewTypeTF_maybe )
import GHC.Tc.Instance.FunDeps( FunDepEqn(..) )
+import qualified GHC.Tc.Utils.Monad as TcM
import GHC.Core.Type
import GHC.Core.Predicate
@@ -467,29 +468,24 @@ Missing this point is what caused #15431
can_eq_nc_forall :: CtEvidence -> EqRel
-> Type -> Type -- LHS and RHS
-> TcS (StopOrContinue (Either IrredCt EqCt))
--- (forall as. phi1) ~ (forall bs. phi2)
--- Check for length match of as, bs
--- Then build an implication constraint: forall as. phi1 ~ phi2[as/bs]
--- But remember also to unify the kinds of as and bs
--- (this is the 'go' loop), and actually substitute phi2[as |> cos / bs]
--- Remember also that we might have forall z (a:z). blah
--- so we must proceed one binder at a time (#13879)
+-- See Note [Solving forall equalities]
can_eq_nc_forall ev eq_rel s1 s2
- | CtWanted { ctev_loc = loc, ctev_dest = orig_dest, ctev_rewriters = rewriters } <- ev
- = do { let free_tvs = tyCoVarsOfTypes [s1,s2]
- (bndrs1, phi1) = tcSplitForAllTyVarBinders s1
- (bndrs2, phi2) = tcSplitForAllTyVarBinders s2
+ | CtWanted { ctev_dest = orig_dest } <- ev
+ = do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2
flags1 = binderFlags bndrs1
flags2 = binderFlags bndrs2
- ; if not (all2 eqForAllVis flags1 flags2) -- Note [ForAllTy and type equality]
- then do { traceTcS "Forall failure" $
+
+ ; if eq_rel == NomEq && not (all2 eqForAllVis flags1 flags2) -- Note [ForAllTy and type equality]
+ then do { traceTcS "Forall failure: visibility-mismatch" $
vcat [ ppr s1, ppr s2, ppr bndrs1, ppr bndrs2
, ppr flags1, ppr flags2 ]
; canEqHardFailure ev s1 s2 }
- else
- do { traceTcS "Creating implication for polytype equality" $ ppr ev
- ; let empty_subst1 = mkEmptySubst $ mkInScopeSet free_tvs
+
+ else do {
+ traceTcS "Creating implication for polytype equality" (ppr ev)
+ ; let free_tvs = tyCoVarsOfTypes [s1,s2]
+ empty_subst1 = mkEmptySubst $ mkInScopeSet free_tvs
; skol_info <- mkSkolemInfo (UnifyForAllSkol phi1)
; (subst1, skol_tvs) <- tcInstSkolTyVarsX skol_info empty_subst1 $
binderVars bndrs1
@@ -497,31 +493,44 @@ can_eq_nc_forall ev eq_rel s1 s2
; let phi1' = substTy subst1 phi1
-- Unify the kinds, extend the substitution
- go :: [TcTyVar] -> Subst -> [TyVarBinder]
- -> TcS (TcCoercion, Cts)
- go (skol_tv:skol_tvs) subst (bndr2:bndrs2)
- = do { let tv2 = binderVar bndr2
- ; (kind_co, wanteds1) <- unify loc rewriters Nominal (tyVarKind skol_tv)
- (substTy subst (tyVarKind tv2))
- ; let subst' = extendTvSubstAndInScope subst tv2
+ go :: UnifyEnv -> [TcTyVar] -> Subst
+ -> [TyVarBinder] -> [TyVarBinder] -> TcM.TcM TcCoercion
+ go uenv (skol_tv:skol_tvs) subst2 (bndr1:bndrs1) (bndr2:bndrs2)
+ = do { let tv2 = binderVar bndr2
+ vis1 = binderFlag bndr1
+ vis2 = binderFlag bndr2
+
+ -- Unify the kinds, at Nominal role
+ -- See (SF1) in Note [Solving forall equalities]
+ ; kind_co <- uType (uenv `setUEnvRole` Nominal)
+ (tyVarKind skol_tv)
+ (substTy subst2 (tyVarKind tv2))
+
+ ; let subst2' = extendTvSubstAndInScope subst2 tv2
(mkCastTy (mkTyVarTy skol_tv) kind_co)
-- skol_tv is already in the in-scope set, but the
-- free vars of kind_co are not; hence "...AndInScope"
- ; (co, wanteds2) <- go skol_tvs subst' bndrs2
- ; return ( mkForAllCo skol_tv kind_co co
- , wanteds1 `unionBags` wanteds2 ) }
+ ; co <- go uenv skol_tvs subst2' bndrs1 bndrs2
+
+ ; return (mkNakedForAllCo skol_tv vis1 vis2 kind_co co)}
+ -- mkNaked.. because these types are not zonked, and the
+ -- assertions in mkForAllCo may fail without that zonking
-- Done: unify phi1 ~ phi2
- go [] subst bndrs2
- = assert (null bndrs2) $
- unify loc rewriters (eqRelRole eq_rel) phi1' (substTyUnchecked subst phi2)
+ go uenv [] subst2 bndrs1 bndrs2
+ = assert (null bndrs1 && null bndrs2) $
+ uType uenv phi1' (substTyUnchecked subst2 phi2)
- go _ _ _ = panic "cna_eq_nc_forall" -- case (s:ss) []
+ go _ _ _ _ _ = panic "can_eq_nc_forall" -- case (s:ss) []
- empty_subst2 = mkEmptySubst (getSubstInScope subst1)
+ init_subst2 = mkEmptySubst (getSubstInScope subst1)
+
+ -- Generate the constraints that live in the body of the implication
+ -- See (SF5) in Note [Solving forall equalities]
+ ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
+ unifyForAllBody ev (eqRelRole eq_rel) $ \uenv ->
+ go uenv skol_tvs init_subst2 bndrs1 bndrs2
- ; (lvl, (all_co, wanteds)) <- pushLevelNoWorkList (ppr skol_info) $
- go skol_tvs empty_subst2 bndrs2
; emitTvImplicationTcS lvl (getSkolemInfo skol_info) skol_tvs wanteds
; setWantedEq orig_dest all_co
@@ -533,16 +542,69 @@ can_eq_nc_forall ev eq_rel s1 s2
; stopWith ev "Discard given polytype equality" }
where
- unify :: CtLoc -> RewriterSet -> Role -> TcType -> TcType -> TcS (TcCoercion, Cts)
- -- This version returns the wanted constraint rather
- -- than putting it in the work list
- unify loc rewriters role ty1 ty2
- | ty1 `tcEqType` ty2
- = return (mkReflCo role ty1, emptyBag)
- | otherwise
- = do { (wanted, co) <- newWantedEq loc rewriters role ty1 ty2
- ; return (co, unitBag (mkNonCanonical wanted)) }
-
+ split_foralls :: TcType -> TcType
+ -> ( [ForAllTyBinder], TcType
+ , [ForAllTyBinder], TcType)
+ -- Split matching foralls; stop when the foralls don't match
+ -- See #22537. See (SF3) in Note [Solving forall equalities]
+ -- Postcondition: the two lists of binders returned have the same length
+ split_foralls s1 s2
+ | Just (bndr1, s1') <- splitForAllForAllTyBinder_maybe s1
+ , Just (bndr2, s2') <- splitForAllForAllTyBinder_maybe s2
+ = let !(bndrs1, phi1, bndrs2, phi2) = split_foralls s1' s2'
+ in (bndr1:bndrs1, phi1, bndr2:bndrs2, phi2)
+ split_foralls s1 s2 = ([], s1, [], s2)
+
+{- Note [Solving forall equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+To solve an equality between foralls
+ [W] (forall a. t1) ~ (forall b. t2)
+the basic plan is simple: just create the implication constraint
+ [W] forall a. { t1 ~ (t2[a/b]) }
+
+The evidence we produce is a ForAllCo; see the typing rule for
+ForAllCo in Note [ForAllCo] in GHC.Tc.TyCo.Rep.
+
+There are lots of wrinkles of course:
+
+(SF1) We must check the kinds match (at Nominal role). So from
+ [W] (forall (a:ka). t1) ~ (forall (b:kb). t2)
+ we actually generate the implication
+ [W] forall (a:ka). { ka ~N kb, t1 ~ t2[a/b] }
+ These kind equalities are generated by the `go` loop in `can_eq_nc_forall`.
+ Why Nominal role? See the typing rule for ForAllCo.
+
+(SF2) At Nominal role we must check that the visiblities match.
+ For example
+ [W] (forall a. a -> a) ~N (forall b -> b -> b)
+ should fail. At /Representational/ role we allow this; see the
+ typing rule for ForAllCo, mentioned above.
+
+(SF3) Consider this (#22537)
+ newtype P a = MkP (forall c. (a,c))
+ [W] (forall a. P a) ~R (forall a b. (a,b))
+ The number of foralls does not line up. But if we just unwrap the outer
+ forall a, we'll get
+ [W] P a ~R forall b. (a,b)
+ Now unwrap the newtype
+ [W] (forall c. (a,c)) ~R (forall b. (a,b))
+ and all is good.
+
+ Conclusion: Don't fail if the number of foralls does not line up. Instead,
+ handle as many binders as are visibly apparent on both sides, and then keep
+ going with unification. See `split_foralls` in `can_eq_nc_forall`. In the
+ above example, at Representational role, the unifier will proceed to unwrap
+ the newtype on the RHS and we'll end up back in can_eq_nc_forall.
+
+(SF4) Remember also that we might have forall z (a:z). blah
+ so in that `go` loop, we must proceed one binder at a time (#13879)
+
+(SF5) Rather than manually gather the constraints needed in the body of the
+ implication, we use `uType`. That way we can solve some of them on the fly,
+ especially Refl ones. We use the `unifyForAllBody` wrapper for `uType`,
+ because we want to /gather/ the equality constraint (to put in the implication)
+ rather than /emit/ them into the monad, as `wrapUnifierTcS` does.
+-}
{- Note [Unwrap newtypes first]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -3188,4 +3250,4 @@ To avoid this situation we do not cache as solved any workitems (or inert)
which did not really made a 'step' towards proving some goal. Solved's are
just an optimization so we don't lose anything in terms of completeness of
solving.
--}
\ No newline at end of file
+-}
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index da38736dbfc7982c7307c63acb09ebdf7c91bd4b..9943ae543597fc90b9e54f7c819b605410c36aca 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -97,7 +97,7 @@ module GHC.Tc.Solver.Monad (
instDFunType,
-- Unification
- wrapUnifierTcS, unifyFunDeps, uPairsTcM,
+ wrapUnifierTcS, unifyFunDeps, uPairsTcM, unifyForAllBody,
-- MetaTyVars
newFlexiTcSTy, instFlexiX,
@@ -1998,6 +1998,22 @@ unifyFunDeps ev role do_unifications
where
fvs = tyCoVarsOfType (ctEvPred ev)
+unifyForAllBody :: CtEvidence -> Role -> (UnifyEnv -> TcM a)
+ -> TcS (a, Cts)
+-- We /return/ the equality constraints we generate,
+-- rather than emitting them into the monad.
+-- See See (SF5) in Note [Solving forall equalities] in GHC.Tc.Solver.Equality
+unifyForAllBody ev role unify_body
+ = do { (res, cts, unified, _rewriters) <- wrapUnifierX ev role unify_body
+ -- Ignore the rewriters. They are used in wrapUnifierTcS only
+ -- as an optimistion to prioritise the work list; but they are
+ -- /also/ stored in each individual constraint we return.
+
+ -- Kick out any inert constraint that we have unified
+ ; _ <- kickOutAfterUnification unified
+
+ ; return (res, cts) }
+
wrapUnifierTcS :: CtEvidence -> Role
-> (UnifyEnv -> TcM a) -- Some calls to uType
-> TcS (a, Bag Ct, [TcTyVar])
@@ -2011,31 +2027,41 @@ wrapUnifierTcS :: CtEvidence -> Role
-- unified the process; the (Bag Ct) are the deferred constraints.
wrapUnifierTcS ev role do_unifications
- = do { (cos, unified, rewriters, cts) <- wrapTcS $
- do { defer_ref <- TcM.newTcRef emptyBag
- ; unified_ref <- TcM.newTcRef []
- ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev)
- ; let env = UE { u_role = role
- , u_rewriters = rewriters
- , u_loc = ctEvLoc ev
- , u_defer = defer_ref
- , u_unified = Just unified_ref}
-
- ; cos <- do_unifications env
-
- ; cts <- TcM.readTcRef defer_ref
- ; unified <- TcM.readTcRef unified_ref
- ; return (cos, unified, rewriters, cts) }
+ = do { (res, cts, unified, rewriters) <- wrapUnifierX ev role do_unifications
-- Emit the deferred constraints
-- See Note [Work-list ordering] in GHC.Tc.Solved.Equality
+ --
+ -- All the constraints in `cts` share the same rewriter set so,
+ -- rather than looking at it one by one, we pass it to
+ -- extendWorkListEqs; just a small optimisation.
; unless (isEmptyBag cts) $
updWorkListTcS (extendWorkListEqs rewriters cts)
-- And kick out any inert constraint that we have unified
; _ <- kickOutAfterUnification unified
- ; return (cos, cts, unified) }
+ ; return (res, cts, unified) }
+
+wrapUnifierX :: CtEvidence -> Role
+ -> (UnifyEnv -> TcM a) -- Some calls to uType
+ -> TcS (a, Bag Ct, [TcTyVar], RewriterSet)
+wrapUnifierX ev role do_unifications
+ = wrapTcS $
+ do { defer_ref <- TcM.newTcRef emptyBag
+ ; unified_ref <- TcM.newTcRef []
+ ; rewriters <- TcM.zonkRewriterSet (ctEvRewriters ev)
+ ; let env = UE { u_role = role
+ , u_rewriters = rewriters
+ , u_loc = ctEvLoc ev
+ , u_defer = defer_ref
+ , u_unified = Just unified_ref}
+
+ ; res <- do_unifications env
+
+ ; cts <- TcM.readTcRef defer_ref
+ ; unified <- TcM.readTcRef unified_ref
+ ; return (res, cts, unified, rewriters) }
{-
diff --git a/compiler/GHC/Tc/TyCl/Utils.hs b/compiler/GHC/Tc/TyCl/Utils.hs
index dab5f3f77a03d76468f2f986815cd8d2405db605..9c9d356a22d2e059b0bd116c87ace777cd738824 100644
--- a/compiler/GHC/Tc/TyCl/Utils.hs
+++ b/compiler/GHC/Tc/TyCl/Utils.hs
@@ -139,7 +139,8 @@ synonymTyConsOfType ty
go_co (GRefl _ ty mco) = go ty `plusNameEnv` go_mco mco
go_co (TyConAppCo _ tc cs) = go_tc tc `plusNameEnv` go_co_s cs
go_co (AppCo co co') = go_co co `plusNameEnv` go_co co'
- go_co (ForAllCo _ co co') = go_co co `plusNameEnv` go_co co'
+ go_co (ForAllCo { fco_kind = kind_co, fco_body = body_co })
+ = go_co kind_co `plusNameEnv` go_co body_co
go_co (FunCo { fco_mult = m, fco_arg = a, fco_res = r })
= go_co m `plusNameEnv` go_co a `plusNameEnv` go_co r
go_co (CoVarCo _) = emptyNameEnv
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 748b18ab234e1ab494c532571060c6ce8849cf70..1e111fa83e567790c884d39d939fd28b6cca73d5 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -1447,7 +1447,7 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
go_co dv (CoVarCo cv) = go_cv dv cv
- go_co dv (ForAllCo tcv kind_co co)
+ go_co dv (ForAllCo { fco_tcv = tcv, fco_kind = kind_co, fco_body = co })
= do { dv1 <- go_co dv kind_co
; collect_cand_qtvs_co orig_ty cur_lvl (bound `extendVarSet` tcv) dv1 co }
diff --git a/compiler/GHC/Types/Var.hs b/compiler/GHC/Types/Var.hs
index 0471688aa6771a5f51aad4c7e9b1dc71adc83391..bbc5454c9fc009396d8643bfb26acac080ee804f 100644
--- a/compiler/GHC/Types/Var.hs
+++ b/compiler/GHC/Types/Var.hs
@@ -69,6 +69,7 @@ module GHC.Types.Var (
ForAllTyFlag(Invisible,Required,Specified,Inferred),
Specificity(..),
isVisibleForAllTyFlag, isInvisibleForAllTyFlag, isInferredForAllTyFlag,
+ coreTyLamForAllTyFlag,
-- * FunTyFlag
FunTyFlag(..), isVisibleFunArg, isInvisibleFunArg, isFUNArg,
@@ -126,6 +127,7 @@ import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import Data.Data
+import Control.DeepSeq
{-
************************************************************************
@@ -453,7 +455,7 @@ updateVarTypeM upd var
-- permitted by request ('Specified') (visible type application), or
-- prohibited entirely from appearing in source Haskell ('Inferred')?
-- See Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility] in "GHC.Core.TyCo.Rep"
-data ForAllTyFlag = Invisible Specificity
+data ForAllTyFlag = Invisible !Specificity
| Required
deriving (Eq, Ord, Data)
-- (<) on ForAllTyFlag means "is less visible than"
@@ -487,6 +489,12 @@ isInferredForAllTyFlag :: ForAllTyFlag -> Bool
isInferredForAllTyFlag (Invisible InferredSpec) = True
isInferredForAllTyFlag _ = False
+coreTyLamForAllTyFlag :: ForAllTyFlag
+-- ^ The ForAllTyFlag on a (Lam a e) term, where `a` is a type variable.
+-- If you want other ForAllTyFlag, use a cast.
+-- See Note [ForAllCo] in GHC.Core.TyCo.Rep
+coreTyLamForAllTyFlag = Specified
+
instance Outputable ForAllTyFlag where
ppr Required = text "[req]"
ppr Specified = text "[spec]"
@@ -514,6 +522,13 @@ instance Binary ForAllTyFlag where
1 -> return Specified
_ -> return Inferred
+instance NFData Specificity where
+ rnf SpecifiedSpec = ()
+ rnf InferredSpec = ()
+instance NFData ForAllTyFlag where
+ rnf (Invisible spec) = rnf spec
+ rnf Required = ()
+
{- *********************************************************************
* *
* FunTyFlag
@@ -882,7 +897,7 @@ Wrinkles
Note [VarBndrs, ForAllTyBinders, TyConBinders, and visibility]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* A ForAllTy (used for both types and kinds) contains a ForAllTyBinder.
Each ForAllTyBinder
Bndr a tvis
diff --git a/docs/core-spec/core-spec.mng b/docs/core-spec/core-spec.mng
index 1e77f3b4de95d470478b257414ca1bc4e2160fb2..95f79fbf7623cc5d5c0d792f6aa212e2a17f0b77 100644
--- a/docs/core-spec/core-spec.mng
+++ b/docs/core-spec/core-spec.mng
@@ -223,8 +223,8 @@ be a type function.
the payload in a \texttt{Refl} must not be built with \texttt{CoercionTy}.
\item If $[[forall z: h .g]]$ is a polymorphic coercion over a coercion variable
(i.e. $[[z]]$ is a coercion variable), then $[[z]]$ can only appear in
- \texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{Note [Unused coercion
- variable in ForAllCo] in \ghcfile{GHC.Core.Coercion}}.
+ \texttt{Refl} and \texttt{GRefl} in $[[g]]$. See \texttt{(FC6) in Note [ForAllCo]
+ in \ghcfile{GHC.Core.TyCon.Rep}}.
\item Prefer $[[g1 ->_R g2]]$ over $[[(->)_R g1 g2]]$; that is, we use \ctor{FunCo},
never \ctor{TyConAppCo}, for coercions over saturated uses of $[[->]]$.
\end{itemize}
diff --git a/testsuite/tests/cpranal/should_compile/T18174.stderr b/testsuite/tests/cpranal/should_compile/T18174.stderr
index b251d9914a48d657379b54bf2a8137ca72fcb024..b47152a95c68cdc723a207c045de2f676072996b 100644
--- a/testsuite/tests/cpranal/should_compile/T18174.stderr
+++ b/testsuite/tests/cpranal/should_compile/T18174.stderr
@@ -1,23 +1,18 @@
==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 464, types: 475, coercions: 6, joins: 0/3}
+Result size of Tidy Core = {terms: 467, types: 458, coercions: 6, joins: 0/3}
-- RHS size: {terms: 8, types: 7, coercions: 0, joins: 0/0}
T18174.$WMkT :: Int %1 -> (Int, Int) %1 -> T
-T18174.$WMkT = \ (conrep_aU0 :: Int) (conrep_aU1 :: (Int, Int)) -> case conrep_aU1 of conrep_X0 { __DEFAULT -> T18174.MkT conrep_aU0 conrep_X0 }
+T18174.$WMkT = \ (conrep_aXh :: Int) (conrep1_aXi :: (Int, Int)) -> case conrep1_aXi of conrep2_aXi { __DEFAULT -> T18174.MkT conrep_aXh conrep2_aXi }
--- RHS size: {terms: 5, types: 10, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 8, types: 15, coercions: 0, joins: 0/0}
T18174.$wstrictField :: Int -> (Int, Int) -> (# Int, (Int, Int) #)
-T18174.$wstrictField
- = \ (ww_s18W :: Int)
- (ww1_s18X
- :: (Int, Int)
- Unf=OtherCon []) ->
- (# ww_s18W, ww1_s18X #)
+T18174.$wstrictField = \ (ww_s1cs :: Int) (ww1_s1ct :: (Int, Int)) -> case ww1_s1ct of ww2_X1 { (ipv_s1ex, ipv1_s1ey) -> (# ww_s1cs, ww2_X1 #) }
-- RHS size: {terms: 12, types: 21, coercions: 0, joins: 0/0}
strictField :: T -> (Int, (Int, Int))
-strictField = \ (ds_s18U :: T) -> case ds_s18U of { MkT ww_s18W ww1_s18X -> case T18174.$wstrictField ww_s18W ww1_s18X of { (# ww2_s1aJ, ww3_s1aK #) -> (ww2_s1aJ, ww3_s1aK) } }
+strictField = \ (ds_s1cq :: T) -> case ds_s1cq of { MkT ww_s1cs ww1_s1ct -> case T18174.$wstrictField ww_s1cs ww1_s1ct of { (# ww2_s1ef, ww3_s1eg #) -> (ww2_s1ef, ww3_s1eg) } }
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18174.$trModule4 :: GHC.Prim.Addr#
@@ -40,20 +35,20 @@ T18174.$trModule :: GHC.Types.Module
T18174.$trModule = GHC.Types.Module T18174.$trModule3 T18174.$trModule1
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
-$krep_r1c2 :: GHC.Types.KindRep
-$krep_r1c2 = GHC.Types.KindRepTyConApp GHC.Types.$tcInt (GHC.Types.[] @GHC.Types.KindRep)
+$krep_r1fR :: GHC.Types.KindRep
+$krep_r1fR = GHC.Types.KindRepTyConApp GHC.Types.$tcInt (GHC.Types.[] @GHC.Types.KindRep)
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
-$krep1_r1c3 :: [GHC.Types.KindRep]
-$krep1_r1c3 = GHC.Types.: @GHC.Types.KindRep $krep_r1c2 (GHC.Types.[] @GHC.Types.KindRep)
+$krep1_r1fS :: [GHC.Types.KindRep]
+$krep1_r1fS = GHC.Types.: @GHC.Types.KindRep $krep_r1fR (GHC.Types.[] @GHC.Types.KindRep)
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
-$krep2_r1c4 :: [GHC.Types.KindRep]
-$krep2_r1c4 = GHC.Types.: @GHC.Types.KindRep $krep_r1c2 $krep1_r1c3
+$krep2_r1fT :: [GHC.Types.KindRep]
+$krep2_r1fT = GHC.Types.: @GHC.Types.KindRep $krep_r1fR $krep1_r1fS
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep3_r1c5 :: GHC.Types.KindRep
-$krep3_r1c5 = GHC.Types.KindRepTyConApp GHC.Tuple.$tc(,) $krep2_r1c4
+$krep3_r1fU :: GHC.Types.KindRep
+$krep3_r1fU = GHC.Types.KindRepTyConApp GHC.Tuple.Prim.$tcTuple2 $krep2_r1fT
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18174.$tcT2 :: GHC.Prim.Addr#
@@ -65,19 +60,19 @@ T18174.$tcT1 = GHC.Types.TrNameS T18174.$tcT2
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18174.$tcT :: GHC.Types.TyCon
-T18174.$tcT = GHC.Types.TyCon 10767449832801551323## 11558512111670031614## T18174.$trModule T18174.$tcT1 0# GHC.Types.krep$*
+T18174.$tcT = GHC.Types.TyCon 10767449832801551323#Word64 11558512111670031614#Word64 T18174.$trModule T18174.$tcT1 0# GHC.Types.krep$*
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
-$krep4_r1c6 :: GHC.Types.KindRep
-$krep4_r1c6 = GHC.Types.KindRepTyConApp T18174.$tcT (GHC.Types.[] @GHC.Types.KindRep)
+$krep4_r1fV :: GHC.Types.KindRep
+$krep4_r1fV = GHC.Types.KindRepTyConApp T18174.$tcT (GHC.Types.[] @GHC.Types.KindRep)
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep5_r1c7 :: GHC.Types.KindRep
-$krep5_r1c7 = GHC.Types.KindRepFun $krep3_r1c5 $krep4_r1c6
+$krep5_r1fW :: GHC.Types.KindRep
+$krep5_r1fW = GHC.Types.KindRepFun $krep3_r1fU $krep4_r1fV
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
T18174.$tc'MkT1 :: GHC.Types.KindRep
-T18174.$tc'MkT1 = GHC.Types.KindRepFun $krep_r1c2 $krep5_r1c7
+T18174.$tc'MkT1 = GHC.Types.KindRepFun $krep_r1fR $krep5_r1fW
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18174.$tc'MkT3 :: GHC.Prim.Addr#
@@ -89,60 +84,60 @@ T18174.$tc'MkT2 = GHC.Types.TrNameS T18174.$tc'MkT3
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
T18174.$tc'MkT :: GHC.Types.TyCon
-T18174.$tc'MkT = GHC.Types.TyCon 15126196523434762667## 13148007393547580468## T18174.$trModule T18174.$tc'MkT2 0# T18174.$tc'MkT1
+T18174.$tc'MkT = GHC.Types.TyCon 15126196523434762667#Word64 13148007393547580468#Word64 T18174.$trModule T18174.$tc'MkT2 0# T18174.$tc'MkT1
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-lvl_r1c8 :: Int
-lvl_r1c8 = GHC.Types.I# 1#
+lvl_r1fX :: Int
+lvl_r1fX = GHC.Types.I# 1#
Rec {
--- RHS size: {terms: 38, types: 38, coercions: 0, joins: 0/1}
-T18174.$wfac3 :: forall {a}. GHC.Prim.Int# -> a -> (# a, Int #)
+-- RHS size: {terms: 38, types: 37, coercions: 0, joins: 0/1}
+T18174.$wfac3 :: forall a. GHC.Prim.Int# -> a -> (# a, Int #)
T18174.$wfac3
- = \ (@a_s196) (ww_s199 :: GHC.Prim.Int#) (s_s19b :: a_s196) ->
- case GHC.Prim.<# ww_s199 2# of {
+ = \ (@a_s1cC) (ww_s1cF :: GHC.Prim.Int#) (s_s1cH :: a_s1cC) ->
+ case GHC.Prim.<# ww_s1cF 2# of {
__DEFAULT ->
let {
- ds_s18k :: (a_s196, Int)
- ds_s18k = case T18174.$wfac3 @a_s196 (GHC.Prim.-# ww_s199 1#) s_s19b of { (# ww1_s1aM, ww2_s1aN #) -> (ww1_s1aM, ww2_s1aN) } } in
- (# case ds_s18k of { (s'_aYW, n'_aYX) -> s'_aYW }, case ds_s18k of { (s'_aYW, n'_aYX) -> case n'_aYX of { GHC.Types.I# ww1_s193 -> GHC.Types.I# (GHC.Prim.*# ww1_s193 ww1_s193) } } #);
- 1# -> (# s_s19b, lvl_r1c8 #)
+ ds_s1bj :: (a_s1cC, Int)
+ ds_s1bj = case T18174.$wfac3 @a_s1cC (GHC.Prim.-# ww_s1cF 1#) s_s1cH of { (# ww1_s1ei, ww2_s1ej #) -> (ww1_s1ei, ww2_s1ej) } } in
+ (# case ds_s1bj of { (s'_a12d, n'_a12e) -> s'_a12d }, case ds_s1bj of { (s'_a12d, n'_a12e) -> case n'_a12e of { GHC.Types.I# ww1_s1cz -> GHC.Types.I# (GHC.Prim.*# ww1_s1cz ww1_s1cz) } } #);
+ 1# -> (# s_s1cH, lvl_r1fX #)
}
end Rec }
--- RHS size: {terms: 14, types: 16, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 14, types: 15, coercions: 0, joins: 0/0}
fac3 :: forall a. Int -> a -> (a, Int)
-fac3 = \ (@a_s196) (n_s197 :: Int) (s_s19b :: a_s196) -> case n_s197 of { GHC.Types.I# ww_s199 -> case T18174.$wfac3 @a_s196 ww_s199 s_s19b of { (# ww1_s1aM, ww2_s1aN #) -> (ww1_s1aM, ww2_s1aN) } }
+fac3 = \ (@a_s1cC) (n_s1cD :: Int) (s_s1cH :: a_s1cC) -> case n_s1cD of { GHC.Types.I# ww_s1cF -> case T18174.$wfac3 @a_s1cC ww_s1cF s_s1cH of { (# ww1_s1ei, ww2_s1ej #) -> (ww1_s1ei, ww2_s1ej) } }
Rec {
--- RHS size: {terms: 24, types: 21, coercions: 0, joins: 0/0}
-T18174.$wfac2 :: forall {a}. GHC.Prim.Int# -> a -> (# a, Int #)
+-- RHS size: {terms: 24, types: 20, coercions: 0, joins: 0/0}
+T18174.$wfac2 :: forall a. GHC.Prim.Int# -> a -> (# a, Int #)
T18174.$wfac2
- = \ (@a_s19g) (ww_s19j :: GHC.Prim.Int#) (s_s19l :: a_s19g) ->
- case GHC.Prim.<# ww_s19j 2# of {
- __DEFAULT -> case T18174.$wfac2 @a_s19g (GHC.Prim.-# ww_s19j 1#) s_s19l of { (# ww1_s1aP, ww2_s1aQ #) -> (# ww1_s1aP, GHC.Num.$fNumInt_$c* ww2_s1aQ ww2_s1aQ #) };
- 1# -> (# s_s19l, lvl_r1c8 #)
+ = \ (@a_s1cM) (ww_s1cP :: GHC.Prim.Int#) (s_s1cR :: a_s1cM) ->
+ case GHC.Prim.<# ww_s1cP 2# of {
+ __DEFAULT -> case T18174.$wfac2 @a_s1cM (GHC.Prim.-# ww_s1cP 1#) s_s1cR of { (# ww1_s1el, ww2_s1em #) -> (# ww1_s1el, GHC.Num.$fNumInt_$c* ww2_s1em ww2_s1em #) };
+ 1# -> (# s_s1cR, lvl_r1fX #)
}
end Rec }
--- RHS size: {terms: 14, types: 16, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 14, types: 15, coercions: 0, joins: 0/0}
fac2 :: forall a. Int -> a -> (a, Int)
-fac2 = \ (@a_s19g) (n_s19h :: Int) (s_s19l :: a_s19g) -> case n_s19h of { GHC.Types.I# ww_s19j -> case T18174.$wfac2 @a_s19g ww_s19j s_s19l of { (# ww1_s1aP, ww2_s1aQ #) -> (ww1_s1aP, ww2_s1aQ) } }
+fac2 = \ (@a_s1cM) (n_s1cN :: Int) (s_s1cR :: a_s1cM) -> case n_s1cN of { GHC.Types.I# ww_s1cP -> case T18174.$wfac2 @a_s1cM ww_s1cP s_s1cR of { (# ww1_s1el, ww2_s1em #) -> (ww1_s1el, ww2_s1em) } }
Rec {
--- RHS size: {terms: 24, types: 21, coercions: 0, joins: 0/0}
-T18174.$wfac1 :: forall {a}. GHC.Prim.Int# -> a -> (# a, GHC.Prim.Int# #)
+-- RHS size: {terms: 24, types: 20, coercions: 0, joins: 0/0}
+T18174.$wfac1 :: forall a. GHC.Prim.Int# -> a -> (# a, GHC.Prim.Int# #)
T18174.$wfac1
- = \ (@a_s19q) (ww_s19t :: GHC.Prim.Int#) (s_s19v :: a_s19q) ->
- case GHC.Prim.<# ww_s19t 2# of {
- __DEFAULT -> case T18174.$wfac1 @a_s19q (GHC.Prim.-# ww_s19t 1#) s_s19v of { (# ww1_s19y, ww2_s1aS #) -> (# ww1_s19y, GHC.Prim.*# ww_s19t ww2_s1aS #) };
- 1# -> (# s_s19v, 1# #)
+ = \ (@a_s1cW) (ww_s1cZ :: GHC.Prim.Int#) (s_s1d1 :: a_s1cW) ->
+ case GHC.Prim.<# ww_s1cZ 2# of {
+ __DEFAULT -> case T18174.$wfac1 @a_s1cW (GHC.Prim.-# ww_s1cZ 1#) s_s1d1 of { (# ww1_s1d4, ww2_s1eo #) -> (# ww1_s1d4, GHC.Prim.*# ww_s1cZ ww2_s1eo #) };
+ 1# -> (# s_s1d1, 1# #)
}
end Rec }
--- RHS size: {terms: 15, types: 16, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 15, types: 15, coercions: 0, joins: 0/0}
fac1 :: forall a. Int -> a -> (a, Int)
-fac1 = \ (@a_s19q) (n_s19r :: Int) (s_s19v :: a_s19q) -> case n_s19r of { GHC.Types.I# ww_s19t -> case T18174.$wfac1 @a_s19q ww_s19t s_s19v of { (# ww1_s19y, ww2_s1aS #) -> (ww1_s19y, GHC.Types.I# ww2_s1aS) } }
+fac1 = \ (@a_s1cW) (n_s1cX :: Int) (s_s1d1 :: a_s1cW) -> case n_s1cX of { GHC.Types.I# ww_s1cZ -> case T18174.$wfac1 @a_s1cW ww_s1cZ s_s1d1 of { (# ww1_s1d4, ww2_s1eo #) -> (ww1_s1d4, GHC.Types.I# ww2_s1eo) } }
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
T18174.h5 :: Int
@@ -151,51 +146,51 @@ T18174.h5 = GHC.Types.I# 0#
-- RHS size: {terms: 37, types: 15, coercions: 0, joins: 0/1}
T18174.$wg2 :: GHC.Prim.Int# -> GHC.Prim.Int# -> (# GHC.Prim.Int#, Int #)
T18174.$wg2
- = \ (ww_s19G :: GHC.Prim.Int#) (ww1_s19K :: GHC.Prim.Int#) ->
- case ww1_s19K of ds_X2 {
+ = \ (ww_s1dc :: GHC.Prim.Int#) (ww1_s1dg :: GHC.Prim.Int#) ->
+ case ww1_s1dg of ds_X2 {
__DEFAULT ->
- (# GHC.Prim.*# 2# ww_s19G,
+ (# GHC.Prim.*# 2# ww_s1dc,
case ds_X2 of wild_X3 {
__DEFAULT ->
let {
- c1#_a17n :: GHC.Prim.Int#
- c1#_a17n = GHC.Prim.andI# 1# (GHC.Prim.<# wild_X3 0#) } in
- case GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#_a17n) wild_X3 of wild1_a17o { __DEFAULT -> GHC.Types.I# (GHC.Prim.-# wild1_a17o c1#_a17n) };
+ c1#_a1co :: GHC.Prim.Int#
+ c1#_a1co = GHC.Prim.andI# 1# (GHC.Prim.<# wild_X3 0#) } in
+ case GHC.Prim.-# (GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#_a1co) wild_X3) c1#_a1co of ds2_a1aa { __DEFAULT -> GHC.Types.I# ds2_a1aa };
0# -> GHC.Real.divZeroError @Int
} #);
- 1# -> (# GHC.Prim.+# 2# ww_s19G, T18174.h5 #)
+ 1# -> (# GHC.Prim.+# 2# ww_s1dc, T18174.h5 #)
}
-- RHS size: {terms: 30, types: 19, coercions: 0, joins: 0/0}
T18174.$wh2 :: GHC.Prim.Int# -> Int
T18174.$wh2
- = \ (ww_s19W :: GHC.Prim.Int#) ->
- case ww_s19W of ds_X2 {
+ = \ (ww_s1ds :: GHC.Prim.Int#) ->
+ case ww_s1ds of ds_X2 {
__DEFAULT ->
case GHC.Prim.remInt# ds_X2 2# of {
- __DEFAULT -> case T18174.$wg2 ds_X2 2# of { (# ww1_s1aU, ww2_s19Q #) -> ww2_s19Q };
- 0# -> case T18174.$wg2 2# ds_X2 of { (# ww1_s1aU, ww2_s19Q #) -> case ww2_s19Q of { GHC.Types.I# y_a17v -> GHC.Types.I# (GHC.Prim.+# ww1_s1aU y_a17v) } }
+ __DEFAULT -> case T18174.$wg2 ds_X2 2# of { (# ww1_s1eq, ww2_s1dl #) -> ww2_s1dl };
+ 0# -> case T18174.$wg2 2# ds_X2 of { (# ww1_s1eq, ww2_s1dl #) -> case ww2_s1dl of { GHC.Types.I# y_a1ah -> GHC.Types.I# (GHC.Prim.+# ww1_s1eq y_a1ah) } }
};
1# -> T18174.h5
}
-- RHS size: {terms: 6, types: 3, coercions: 0, joins: 0/0}
h2 :: Int -> Int
-h2 = \ (ds_s19U :: Int) -> case ds_s19U of { GHC.Types.I# ww_s19W -> T18174.$wh2 ww_s19W }
+h2 = \ (ds_s1dq :: Int) -> case ds_s1dq of { GHC.Types.I# ww_s1ds -> T18174.$wh2 ww_s1ds }
-- RHS size: {terms: 34, types: 14, coercions: 0, joins: 0/1}
T18174.$wg1 :: GHC.Prim.Int# -> (# GHC.Prim.Int#, Int #)
T18174.$wg1
- = \ (ww_s1a3 :: GHC.Prim.Int#) ->
- case ww_s1a3 of ds_X2 {
+ = \ (ww_s1dz :: GHC.Prim.Int#) ->
+ case ww_s1dz of ds_X2 {
__DEFAULT ->
(# GHC.Prim.*# 2# ds_X2,
case ds_X2 of wild_X3 {
__DEFAULT ->
let {
- c1#_a17n :: GHC.Prim.Int#
- c1#_a17n = GHC.Prim.andI# 1# (GHC.Prim.<# wild_X3 0#) } in
- case GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#_a17n) wild_X3 of wild1_a17o { __DEFAULT -> GHC.Types.I# (GHC.Prim.-# wild1_a17o c1#_a17n) };
+ c1#_a1co :: GHC.Prim.Int#
+ c1#_a1co = GHC.Prim.andI# 1# (GHC.Prim.<# wild_X3 0#) } in
+ case GHC.Prim.-# (GHC.Prim.quotInt# (GHC.Prim.-# 2# c1#_a1co) wild_X3) c1#_a1co of ds2_a1aa { __DEFAULT -> GHC.Types.I# ds2_a1aa };
0# -> GHC.Real.divZeroError @Int
} #);
1# -> (# 15#, T18174.h5 #)
@@ -203,52 +198,52 @@ T18174.$wg1
-- RHS size: {terms: 8, types: 9, coercions: 0, joins: 0/0}
T18174.h4 :: (Int, Int)
-T18174.h4 = case T18174.$wg1 2# of { (# ww_s1aW, ww1_s1a9 #) -> (GHC.Types.I# ww_s1aW, ww1_s1a9) }
+T18174.h4 = case T18174.$wg1 2# of { (# ww_s1es, ww1_s1dE #) -> (GHC.Types.I# ww_s1es, ww1_s1dE) }
-- RHS size: {terms: 22, types: 16, coercions: 0, joins: 0/0}
T18174.$wh1 :: GHC.Prim.Int# -> Int
T18174.$wh1
- = \ (ww_s1af :: GHC.Prim.Int#) ->
- case ww_s1af of ds_X2 {
- __DEFAULT -> case T18174.$wg1 ds_X2 of { (# ww1_s1aW, ww2_s1a9 #) -> case ww2_s1a9 of { GHC.Types.I# y_a17v -> GHC.Types.I# (GHC.Prim.+# ww1_s1aW y_a17v) } };
+ = \ (ww_s1dL :: GHC.Prim.Int#) ->
+ case ww_s1dL of ds_X2 {
+ __DEFAULT -> case T18174.$wg1 ds_X2 of { (# ww1_s1es, ww2_s1dE #) -> case ww2_s1dE of { GHC.Types.I# y_a1ah -> GHC.Types.I# (GHC.Prim.+# ww1_s1es y_a1ah) } };
1# -> T18174.h5;
- 2# -> case T18174.h4 of { (ds1_a155, y_a156) -> y_a156 }
+ 2# -> case T18174.h4 of { (ds1_a1aS, y_a1aT) -> y_a1aT }
}
-- RHS size: {terms: 6, types: 3, coercions: 0, joins: 0/0}
h1 :: Int -> Int
-h1 = \ (ds_s1ad :: Int) -> case ds_s1ad of { GHC.Types.I# ww_s1af -> T18174.$wh1 ww_s1af }
+h1 = \ (ds_s1dJ :: Int) -> case ds_s1dJ of { GHC.Types.I# ww_s1dL -> T18174.$wh1 ww_s1dL }
-- RHS size: {terms: 12, types: 5, coercions: 0, joins: 0/0}
thunkDiverges :: Int -> (Int, Bool)
-thunkDiverges = \ (x_aIy :: Int) -> (case x_aIy of { GHC.Types.I# x1_a17s -> GHC.Types.I# (GHC.Prim.+# 2# (GHC.Prim.*# 2# x1_a17s)) }, GHC.Types.False)
+thunkDiverges = \ (x_aLg :: Int) -> (case x_aLg of { GHC.Types.I# x1_a1ae -> GHC.Types.I# (GHC.Prim.+# 2# (GHC.Prim.*# 2# x1_a1ae)) }, GHC.Types.False)
-- RHS size: {terms: 13, types: 10, coercions: 0, joins: 0/0}
T18174.$wdataConWrapper :: (Int, Int) -> Int -> (# T, Int #)
-T18174.$wdataConWrapper = \ (p_s1av :: (Int, Int)) (x_s1aw :: Int) -> (# T18174.$WMkT x_s1aw p_s1av, case x_s1aw of { GHC.Types.I# x1_a17s -> GHC.Types.I# (GHC.Prim.+# x1_a17s 1#) } #)
+T18174.$wdataConWrapper = \ (p_s1e1 :: (Int, Int)) (x_s1e2 :: Int) -> (# T18174.$WMkT x_s1e2 p_s1e1, case x_s1e2 of { GHC.Types.I# x1_a1ae -> GHC.Types.I# (GHC.Prim.+# x1_a1ae 1#) } #)
-- RHS size: {terms: 10, types: 13, coercions: 0, joins: 0/0}
dataConWrapper :: (Int, Int) -> Int -> (T, Int)
-dataConWrapper = \ (p_s1av :: (Int, Int)) (x_s1aw :: Int) -> case T18174.$wdataConWrapper p_s1av x_s1aw of { (# ww_s1aY, ww1_s1aZ #) -> (ww_s1aY, ww1_s1aZ) }
+dataConWrapper = \ (p_s1e1 :: (Int, Int)) (x_s1e2 :: Int) -> case T18174.$wdataConWrapper p_s1e1 x_s1e2 of { (# ww_s1eu, ww1_s1ev #) -> (ww_s1eu, ww1_s1ev) }
Rec {
--- RHS size: {terms: 27, types: 31, coercions: 0, joins: 0/0}
+-- RHS size: {terms: 27, types: 25, coercions: 0, joins: 0/0}
T18174.$wfacIO :: GHC.Prim.Int# -> GHC.Prim.State# GHC.Prim.RealWorld -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)
T18174.$wfacIO
- = \ (ww_s1aD :: GHC.Prim.Int#) (eta_s1aF :: GHC.Prim.State# GHC.Prim.RealWorld) ->
- case GHC.Prim.<# ww_s1aD 2# of {
- __DEFAULT -> case T18174.$wfacIO (GHC.Prim.-# ww_s1aD 1#) eta_s1aF of { (# ipv_a180, ipv1_a181 #) -> (# ipv_a180, case ipv1_a181 of { GHC.Types.I# y_a16I -> GHC.Types.I# (GHC.Prim.*# ww_s1aD y_a16I) } #) };
- 1# -> (# eta_s1aF, lvl_r1c8 #)
+ = \ (ww_s1e9 :: GHC.Prim.Int#) (eta_s1eb :: GHC.Prim.State# GHC.Prim.RealWorld) ->
+ case GHC.Prim.<# ww_s1e9 2# of {
+ __DEFAULT -> case T18174.$wfacIO (GHC.Prim.-# ww_s1e9 1#) eta_s1eb of { (# ipv_a1bb, ipv1_a1bc #) -> (# ipv_a1bb, case ipv1_a1bc of { GHC.Types.I# y_a19M -> GHC.Types.I# (GHC.Prim.*# ww_s1e9 y_a19M) } #) };
+ 1# -> (# eta_s1eb, lvl_r1fX #)
}
end Rec }
-- RHS size: {terms: 8, types: 5, coercions: 0, joins: 0/0}
T18174.facIO1 :: Int -> GHC.Prim.State# GHC.Prim.RealWorld -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)
-T18174.facIO1 = \ (n_s1aB :: Int) (eta_s1aF :: GHC.Prim.State# GHC.Prim.RealWorld) -> case n_s1aB of { GHC.Types.I# ww_s1aD -> T18174.$wfacIO ww_s1aD eta_s1aF }
+T18174.facIO1 = \ (n_s1e7 :: Int) (eta_s1eb :: GHC.Prim.State# GHC.Prim.RealWorld) -> case n_s1e7 of { GHC.Types.I# ww_s1e9 -> T18174.$wfacIO ww_s1e9 eta_s1eb }
-- RHS size: {terms: 1, types: 0, coercions: 6, joins: 0/0}
facIO :: Int -> IO Int
-facIO = T18174.facIO1 `cast` (<Int>_R %<'Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R) :: (Int -> GHC.Prim.State# GHC.Prim.RealWorld -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)) ~R# (Int -> IO Int))
+facIO = T18174.facIO1 `cast` (<Int>_R %<Many>_N ->_R Sym (GHC.Types.N:IO[0] <Int>_R) :: (Int -> GHC.Prim.State# GHC.Prim.RealWorld -> (# GHC.Prim.State# GHC.Prim.RealWorld, Int #)) ~R# (Int -> IO Int))
diff --git a/testsuite/tests/cpranal/should_compile/T18401.stderr b/testsuite/tests/cpranal/should_compile/T18401.stderr
index 75913b39798157be7e0d4d38030083585cf58cc4..5993a2b07c313a7125a9ae2d866f270cd262d2c1 100644
--- a/testsuite/tests/cpranal/should_compile/T18401.stderr
+++ b/testsuite/tests/cpranal/should_compile/T18401.stderr
@@ -4,31 +4,31 @@ Result size of Tidy Core = {terms: 52, types: 86, coercions: 0, joins: 0/0}
Rec {
-- RHS size: {terms: 18, types: 24, coercions: 0, joins: 0/0}
-T18401.$w$spoly_$wgo1 :: forall {a}. a -> [a] -> (# [a] #)
+T18401.$w$spoly_$wgo1 :: forall a. a -> [a] -> (# [a] #)
T18401.$w$spoly_$wgo1
- = \ (@a_s18C) (w_s18D :: a_s18C) (w1_s18E :: [a_s18C]) ->
- case w1_s18E of {
- [] -> (# GHC.Types.[] @a_s18C #);
- : y_a15b ys_a15c -> (# GHC.Types.: @a_s18C w_s18D (case T18401.$w$spoly_$wgo1 @a_s18C y_a15b ys_a15c of { (# ww_s18J #) -> ww_s18J }) #)
+ = \ (@a_s1cL) (sc_s1cM :: a_s1cL) (sc1_s1cN :: [a_s1cL]) ->
+ case sc1_s1cN of {
+ [] -> (# GHC.Types.[] @a_s1cL #);
+ : y_a1bH ys_a1bI -> (# GHC.Types.: @a_s1cL sc_s1cM (case T18401.$w$spoly_$wgo1 @a_s1cL y_a1bH ys_a1bI of { (# ww_s1cR #) -> ww_s1cR }) #)
}
end Rec }
-- RHS size: {terms: 17, types: 22, coercions: 0, joins: 0/0}
si :: forall a. [a] -> (Bool, [a])
si
- = \ (@a_s17T) (w_s17U :: [a_s17T]) ->
- case w_s17U of {
- [] -> (GHC.Types.False, GHC.Types.[] @a_s17T);
- : y_a15b ys_a15c -> (GHC.Types.True, case T18401.$w$spoly_$wgo1 @a_s17T y_a15b ys_a15c of { (# ww_s18J #) -> ww_s18J })
+ = \ (@a_s1bR) (xs0_s1bS :: [a_s1bR]) ->
+ case xs0_s1bS of {
+ [] -> (GHC.Types.False, GHC.Types.[] @a_s1bR);
+ : y_a1bH ys_a1bI -> (GHC.Types.True, case T18401.$w$spoly_$wgo1 @a_s1bR y_a1bH ys_a1bI of { (# ww_s1cR #) -> ww_s1cR })
}
-- RHS size: {terms: 14, types: 19, coercions: 0, joins: 0/0}
safeInit :: forall a. [a] -> Maybe [a]
safeInit
- = \ (@a_aPB) (xs_aut :: [a_aPB]) ->
- case xs_aut of {
- [] -> GHC.Maybe.Nothing @[a_aPB];
- : y_a15b ys_a15c -> GHC.Maybe.Just @[a_aPB] (case T18401.$w$spoly_$wgo1 @a_aPB y_a15b ys_a15c of { (# ww_s18J #) -> ww_s18J })
+ = \ (@a_aQu) (xs_awN :: [a_aQu]) ->
+ case xs_awN of {
+ [] -> GHC.Maybe.Nothing @[a_aQu];
+ : y_a1bH ys_a1bI -> GHC.Maybe.Just @[a_aQu] (case T18401.$w$spoly_$wgo1 @a_aQu y_a1bH ys_a1bI of { (# ww_s1cR #) -> ww_s1cR })
}
diff --git a/testsuite/tests/pmcheck/should_compile/T11195.hs b/testsuite/tests/pmcheck/should_compile/T11195.hs
index 7a7a4b05c5b47740e1e1eeba7d400609fbea6460..8b1c79c21911f93f2ac9f5a776451328abcfed67 100644
--- a/testsuite/tests/pmcheck/should_compile/T11195.hs
+++ b/testsuite/tests/pmcheck/should_compile/T11195.hs
@@ -111,11 +111,11 @@ opt_trans_rule is co1 co2@(AppCo co2a co2b)
-- Push transitivity inside forall
opt_trans_rule is co1 co2
- | ForAllCo tv1 eta1 r1 <- co1
- , Just (tv2,eta2,r2) <- etaForAllCo_maybe co2 = undefined
+ | ForAllCo tv1 vl1 vr1 eta1 r1 <- co1
+ , Just (tv2,vl2,vr2,eta2,r2) <- etaForAllCo_maybe co2 = undefined
- | ForAllCo tv2 eta2 r2 <- co2
- , Just (tv1,eta1,r1) <- etaForAllCo_maybe co1 = undefined
+ | ForAllCo tv2 vl2 vr1 eta2 r2 <- co2
+ , Just (tv1,vl1,vr2,eta1,r1) <- etaForAllCo_maybe co1 = undefined
where
push_trans tv1 eta1 r1 tv2 eta2 r2 = undefined
diff --git a/testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr b/testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr
index 7c495e48fe0ee85c86e5a1068157814fb35c6aa5..8776aed758292331cf78fccd2d7a3327dc9daa5b 100644
--- a/testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr
+++ b/testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr
@@ -4,7 +4,7 @@ Result size of Tidy Core
= {terms: 82, types: 52, coercions: 29, joins: 0/0}
-- RHS size: {terms: 3, types: 3, coercions: 0, joins: 0/0}
-unsafeToInteger1 :: forall {n :: Nat}. Signed n -> Signed n
+unsafeToInteger1 :: forall (n :: Nat). Signed n -> Signed n
[GblId, Arity=1, Unf=OtherCon []]
unsafeToInteger1 = \ (@(n :: Nat)) (ds :: Signed n) -> ds
@@ -15,8 +15,8 @@ unsafeToInteger
= unsafeToInteger1
`cast` (forall (n :: <Nat>_N).
<Signed n>_R %<Many>_N ->_R OpaqueNoCastWW.N:Signed[0] <n>_P
- :: (forall {n :: Nat}. Signed n -> Signed n)
- ~R# (forall {n :: Nat}. Signed n -> Integer))
+ :: (forall (n :: Nat). Signed n -> Signed n)
+ ~R# (forall (n :: Nat). Signed n -> Integer))
-- RHS size: {terms: 8, types: 7, coercions: 21, joins: 0/0}
times [InlPrag=OPAQUE]
@@ -38,8 +38,8 @@ times
<Signed m>_R
%<Many>_N ->_R <Signed n>_R
%<Many>_N ->_R Sym (OpaqueNoCastWW.N:Signed[0] <m + n>_P)
- :: (forall {m :: Nat} {n :: Nat}. Signed m -> Signed n -> Integer)
- ~R# (forall {m :: Nat} {n :: Nat}.
+ :: (forall (m :: Nat) (n :: Nat). Signed m -> Signed n -> Integer)
+ ~R# (forall (m :: Nat) (n :: Nat).
Signed m -> Signed n -> Signed (m + n)))
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
diff --git a/testsuite/tests/stranal/should_compile/T15627.stderr b/testsuite/tests/stranal/should_compile/T15627.stderr
index 38c054da179d0d19762ea8a187e3bd8477e721bf..02520ebd719bf3fee6cea4085ce11af99b660e65 100644
--- a/testsuite/tests/stranal/should_compile/T15627.stderr
+++ b/testsuite/tests/stranal/should_compile/T15627.stderr
@@ -1,337 +1,320 @@
-[1 of 1] Compiling Unlifted ( T15627.hs, T15627.o )
==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 254, types: 130, coercions: 0, joins: 3/3}
+Result size of Tidy Core = {terms: 266, types: 128, coercions: 0, joins: 3/3}
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
Unlifted.$trModule4 :: Addr#
-[GblId,
- Caf=NoCafRefs,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}]
Unlifted.$trModule4 = "main"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
Unlifted.$trModule3 :: GHC.Types.TrName
-[GblId,
- Caf=NoCafRefs,
- Str=m1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$trModule3 = GHC.Types.TrNameS Unlifted.$trModule4
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
Unlifted.$trModule2 :: Addr#
-[GblId,
- Caf=NoCafRefs,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
Unlifted.$trModule2 = "Unlifted"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
Unlifted.$trModule1 :: GHC.Types.TrName
-[GblId,
- Caf=NoCafRefs,
- Str=m1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$trModule1 = GHC.Types.TrNameS Unlifted.$trModule2
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-Unlifted.$trModule :: GHC.Unit.Module
-[GblId,
- Caf=NoCafRefs,
- Str=m,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}]
-Unlifted.$trModule = GHC.Unit.Module Unlifted.$trModule3 Unlifted.$trModule1
+Unlifted.$trModule :: GHC.Types.Module
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+Unlifted.$trModule = GHC.Types.Module Unlifted.$trModule3 Unlifted.$trModule1
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep_r1d0 :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep_r1d0 = GHC.Types.KindRepTyConApp GHC.Types.$tc'Lifted (GHC.Types.[] @GHC.Types.KindRep)
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
-$krep_r2Xd :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m1, Unf=OtherCon []]
-$krep_r2Xd = GHC.Types.KindRepTyConApp GHC.Types.$tcInt (GHC.Types.[] @ GHC.Types.KindRep)
+$krep1_r1d1 :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep1_r1d1 = GHC.Types.KindRepTyConApp GHC.Types.$tcInt (GHC.Types.[] @GHC.Types.KindRep)
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-$krep1_r2Xe :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m2, Unf=OtherCon []]
-$krep1_r2Xe = GHC.Types.KindRepVar 1#
+$krep2_r1d2 :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep2_r1d2 = GHC.Types.KindRepVar 1#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-$krep2_r2Xf :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m2, Unf=OtherCon []]
-$krep2_r2Xf = GHC.Types.KindRepVar 0#
+$krep3_r1d3 :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep3_r1d3 = GHC.Types.KindRepVar 0#
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
-$krep3_r2Xg :: [GHC.Types.KindRep]
-[GblId, Caf=NoCafRefs, Str=m2, Unf=OtherCon []]
-$krep3_r2Xg = GHC.Types.: @ GHC.Types.KindRep $krep2_r2Xf (GHC.Types.[] @ GHC.Types.KindRep)
+$krep4_r1d4 :: [GHC.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep4_r1d4 = GHC.Types.: @GHC.Types.KindRep $krep3_r1d3 (GHC.Types.[] @GHC.Types.KindRep)
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep5_r1d5 :: [GHC.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep5_r1d5 = GHC.Types.: @GHC.Types.KindRep $krep_r1d0 $krep4_r1d4
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep4_r2Xh :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m1, Unf=OtherCon []]
-$krep4_r2Xh = GHC.Types.KindRepTyConApp GHC.Types.$tcArray# $krep3_r2Xg
+$krep6_r1d6 :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep6_r1d6 = GHC.Types.KindRepTyConApp GHC.Types.$tcArray# $krep5_r1d5
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
-$krep5_r2Xi :: [GHC.Types.KindRep]
-[GblId, Caf=NoCafRefs, Str=m2, Unf=OtherCon []]
-$krep5_r2Xi = GHC.Types.: @ GHC.Types.KindRep $krep1_r2Xe (GHC.Types.[] @ GHC.Types.KindRep)
+$krep7_r1d7 :: [GHC.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep7_r1d7 = GHC.Types.: @GHC.Types.KindRep $krep2_r1d2 (GHC.Types.[] @GHC.Types.KindRep)
-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
-$krep6_r2Xj :: [GHC.Types.KindRep]
-[GblId, Caf=NoCafRefs, Str=m2, Unf=OtherCon []]
-$krep6_r2Xj = GHC.Types.: @ GHC.Types.KindRep $krep2_r2Xf $krep5_r2Xi
+$krep8_r1d8 :: [GHC.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep8_r1d8 = GHC.Types.: @GHC.Types.KindRep $krep3_r1d3 $krep7_r1d7
+
+-- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
+$krep9_r1d9 :: [GHC.Types.KindRep]
+[GblId, Unf=OtherCon []]
+$krep9_r1d9 = GHC.Types.: @GHC.Types.KindRep $krep_r1d0 $krep8_r1d8
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep7_r2Xk :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m1, Unf=OtherCon []]
-$krep7_r2Xk = GHC.Types.KindRepTyConApp GHC.Types.$tcMutVar# $krep6_r2Xj
+$krep10_r1da :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep10_r1da = GHC.Types.KindRepTyConApp GHC.Types.$tcMutVar# $krep9_r1d9
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tcMMutVar2 :: Addr#
-[GblId,
- Caf=NoCafRefs,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
Unlifted.$tcMMutVar2 = "MMutVar"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tcMMutVar1 :: GHC.Types.TrName
-[GblId,
- Caf=NoCafRefs,
- Str=m1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$tcMMutVar1 = GHC.Types.TrNameS Unlifted.$tcMMutVar2
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tcMMutVar :: GHC.Types.TyCon
-[GblId,
- Caf=NoCafRefs,
- Str=m,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 70}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$tcMMutVar
- = GHC.Types.TyCon 976071122164149049## 18076036821450447502## Unlifted.$trModule Unlifted.$tcMMutVar1 0# GHC.Types.krep$*->*->*
+ = GHC.Types.TyCon
+ 976071122164149049#Word64 18076036821450447502#Word64 Unlifted.$trModule Unlifted.$tcMMutVar1 0# GHC.Types.krep$*->*->*
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep8_r2Xl :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m1, Unf=OtherCon []]
-$krep8_r2Xl = GHC.Types.KindRepTyConApp Unlifted.$tcMMutVar $krep6_r2Xj
+$krep11_r1db :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep11_r1db = GHC.Types.KindRepTyConApp Unlifted.$tcMMutVar $krep8_r1d8
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep9_r2Xm :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m4, Unf=OtherCon []]
-$krep9_r2Xm = GHC.Types.KindRepFun $krep_r2Xd $krep8_r2Xl
+$krep12_r1dc :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep12_r1dc = GHC.Types.KindRepFun $krep1_r1d1 $krep11_r1db
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-Unlifted.$tc'MMutVar1 [InlPrag=NOUSERINLINE[~]] :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m4, Unf=OtherCon []]
-Unlifted.$tc'MMutVar1 = GHC.Types.KindRepFun $krep7_r2Xk $krep9_r2Xm
+Unlifted.$tc'MMutVar1 [InlPrag=[~]] :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+Unlifted.$tc'MMutVar1 = GHC.Types.KindRepFun $krep10_r1da $krep12_r1dc
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tc'MMutVar3 :: Addr#
-[GblId,
- Caf=NoCafRefs,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
Unlifted.$tc'MMutVar3 = "'MMutVar"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tc'MMutVar2 :: GHC.Types.TrName
-[GblId,
- Caf=NoCafRefs,
- Str=m1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$tc'MMutVar2 = GHC.Types.TrNameS Unlifted.$tc'MMutVar3
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tc'MMutVar :: GHC.Types.TyCon
-[GblId,
- Caf=NoCafRefs,
- Str=m,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 70}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$tc'MMutVar
- = GHC.Types.TyCon 1807347364283186211## 6245494011022471830## Unlifted.$trModule Unlifted.$tc'MMutVar2 2# Unlifted.$tc'MMutVar1
+ = GHC.Types.TyCon
+ 1807347364283186211#Word64 6245494011022471830#Word64 Unlifted.$trModule Unlifted.$tc'MMutVar2 2# Unlifted.$tc'MMutVar1
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tcAArray2 :: Addr#
-[GblId,
- Caf=NoCafRefs,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
Unlifted.$tcAArray2 = "AArray"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tcAArray1 :: GHC.Types.TrName
-[GblId,
- Caf=NoCafRefs,
- Str=m1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$tcAArray1 = GHC.Types.TrNameS Unlifted.$tcAArray2
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tcAArray :: GHC.Types.TyCon
-[GblId,
- Caf=NoCafRefs,
- Str=m,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 70}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$tcAArray
- = GHC.Types.TyCon 15463012197909582608## 8369862272173810511## Unlifted.$trModule Unlifted.$tcAArray1 0# GHC.Types.krep$*Arr*
+ = GHC.Types.TyCon
+ 15463012197909582608#Word64 8369862272173810511#Word64 Unlifted.$trModule Unlifted.$tcAArray1 0# GHC.Types.krep$*Arr*
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep10_r2Xn :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m1, Unf=OtherCon []]
-$krep10_r2Xn = GHC.Types.KindRepTyConApp Unlifted.$tcAArray $krep3_r2Xg
+$krep13_r1dd :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep13_r1dd = GHC.Types.KindRepTyConApp Unlifted.$tcAArray $krep4_r1d4
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep11_r2Xo :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m4, Unf=OtherCon []]
-$krep11_r2Xo = GHC.Types.KindRepFun $krep_r2Xd $krep10_r2Xn
+$krep14_r1de :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+$krep14_r1de = GHC.Types.KindRepFun $krep1_r1d1 $krep13_r1dd
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-Unlifted.$tc'AArray1 [InlPrag=NOUSERINLINE[~]] :: GHC.Types.KindRep
-[GblId, Caf=NoCafRefs, Str=m4, Unf=OtherCon []]
-Unlifted.$tc'AArray1 = GHC.Types.KindRepFun $krep4_r2Xh $krep11_r2Xo
+Unlifted.$tc'AArray1 [InlPrag=[~]] :: GHC.Types.KindRep
+[GblId, Unf=OtherCon []]
+Unlifted.$tc'AArray1 = GHC.Types.KindRepFun $krep6_r1d6 $krep14_r1de
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tc'AArray3 :: Addr#
-[GblId,
- Caf=NoCafRefs,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 30 0}]
Unlifted.$tc'AArray3 = "'AArray"#
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tc'AArray2 :: GHC.Types.TrName
-[GblId,
- Caf=NoCafRefs,
- Str=m1,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$tc'AArray2 = GHC.Types.TrNameS Unlifted.$tc'AArray3
-- RHS size: {terms: 7, types: 0, coercions: 0, joins: 0/0}
Unlifted.$tc'AArray :: GHC.Types.TyCon
-[GblId,
- Caf=NoCafRefs,
- Str=m,
- Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 70}]
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
Unlifted.$tc'AArray
- = GHC.Types.TyCon 5117353292610538775## 18288923674485681885## Unlifted.$trModule Unlifted.$tc'AArray2 1# Unlifted.$tc'AArray1
+ = GHC.Types.TyCon
+ 5117353292610538775#Word64 18288923674485681885#Word64 Unlifted.$trModule Unlifted.$tc'AArray2 1# Unlifted.$tc'AArray1
-- RHS size: {terms: 2, types: 0, coercions: 0, joins: 0/0}
-lvl_r2Xp :: Int
-[GblId, Caf=NoCafRefs, Str=m, Unf=OtherCon []]
-lvl_r2Xp = GHC.Types.I# 1#
+Unlifted.fac1 :: Int
+[GblId, Unf=Unf{Src=<vanilla>, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 10}]
+Unlifted.fac1 = GHC.Types.I# 1#
-- RHS size: {terms: 34, types: 10, coercions: 0, joins: 1/1}
-fac [InlPrag=NOUSERINLINE[2]] :: Int -> Int
+fac :: Int -> Int
[GblId,
Arity=1,
- Caf=NoCafRefs,
- Str=<S(S),1*U(U)>m,
- Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True,
+ Str=<1!P(L)>,
+ Cpr=1,
+ Unf=Unf{Src=StableSystem, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
- Tmpl= \ (w_s2UI [Occ=Once!] :: Int) ->
- case w_s2UI of { I# ww1_s2UL ->
- case ># 1# ww1_s2UL of {
+ Tmpl= \ (n_ayj [Occ=Once1!] :: Int) ->
+ case n_ayj of { I# y_a1bo ->
+ case ># 1# y_a1bo of {
__DEFAULT ->
joinrec {
- $wgo_s2UH [InlPrag=NOUSERINLINE[2], Occ=LoopBreakerT[2]] :: Int# -> Int# -> Int
- [LclId[JoinId(2)], Arity=2, Str=<S,U><S,U>m, Unf=OtherCon []]
- $wgo_s2UH (w1_s2UB :: Int#) (ww2_s2UF [Occ=Once*] :: Int#)
- = case ==# w1_s2UB ww1_s2UL of {
- __DEFAULT -> jump $wgo_s2UH (+# w1_s2UB 1#) (*# ww2_s2UF w1_s2UB);
- 1# -> GHC.Types.I# (*# ww2_s2UF w1_s2UB)
+ go3_a1bC [InlPrag=[2], Occ=T[2]] :: Int# -> Int -> Int
+ [LclId[JoinId(2)(Just [~, !])],
+ Arity=2,
+ Str=<L><S!P(L)>,
+ Unf=Unf{Src=StableSystem, TopLvl=False, Value=True, ConLike=True, WorkFree=True, Expandable=True,
+ Guidance=ALWAYS_IF(arity=2,unsat_ok=True,boring_ok=False)
+ Tmpl= \ (x_s1bI [Occ=Once1] :: Int#) (v_s1bJ [Occ=Once1!, OS=OneShot] :: Int) ->
+ case v_s1bJ of { I# ww_s1bL [Occ=Once1] -> jump $wgo3_s1bO x_s1bI ww_s1bL }}]
+ go3_a1bC (x_s1bI [Occ=Once1] :: Int#) (v_s1bJ [Occ=Once1!, OS=OneShot] :: Int)
+ = case v_s1bJ of { I# ww_s1bL [Occ=Once1] -> jump $wgo3_s1bO x_s1bI ww_s1bL };
+ $wgo3_s1bO [InlPrag=[2], Occ=LoopBreakerT[2]] :: Int# -> Int# -> Int
+ [LclId[JoinId(2)(Nothing)], Arity=2, Str=<L><L>, Unf=OtherCon []]
+ $wgo3_s1bO (x_s1bI :: Int#) (ww_s1bL [Occ=Once2] :: Int#)
+ = case ==# x_s1bI y_a1bo of {
+ __DEFAULT -> jump go3_a1bC (+# x_s1bI 1#) (GHC.Types.I# (*# ww_s1bL x_s1bI));
+ 1# -> GHC.Types.I# (*# ww_s1bL x_s1bI)
}; } in
- jump $wgo_s2UH 1# 1#;
- 1# -> GHC.Types.I# 1#
+ jump go3_a1bC 1# Unlifted.fac1;
+ 1# -> Unlifted.fac1
}
}}]
fac
- = \ (w_s2UI :: Int) ->
- case w_s2UI of { I# ww1_s2UL ->
- case ># 1# ww1_s2UL of {
+ = \ (n_ayj :: Int) ->
+ case n_ayj of { I# y_a1bo ->
+ case ># 1# y_a1bo of {
__DEFAULT ->
joinrec {
- $wgo_s2UH [InlPrag=NOUSERINLINE[2], Occ=LoopBreaker] :: Int# -> Int# -> Int
- [LclId[JoinId(2)], Arity=2, Str=<S,U><S,U>m, Unf=OtherCon []]
- $wgo_s2UH (w1_s2UB :: Int#) (ww2_s2UF :: Int#)
- = case ==# w1_s2UB ww1_s2UL of {
- __DEFAULT -> jump $wgo_s2UH (+# w1_s2UB 1#) (*# ww2_s2UF w1_s2UB);
- 1# -> GHC.Types.I# (*# ww2_s2UF w1_s2UB)
+ $wgo3_s1bO [InlPrag=[2], Occ=LoopBreaker, Dmd=SC(S,C(1,!P(L)))] :: Int# -> Int# -> Int
+ [LclId[JoinId(2)(Nothing)], Arity=2, Str=<L><L>, Unf=OtherCon []]
+ $wgo3_s1bO (x_s1bI :: Int#) (ww_s1bL :: Int#)
+ = case ==# x_s1bI y_a1bo of {
+ __DEFAULT -> jump $wgo3_s1bO (+# x_s1bI 1#) (*# ww_s1bL x_s1bI);
+ 1# -> GHC.Types.I# (*# ww_s1bL x_s1bI)
}; } in
- jump $wgo_s2UH 1# 1#;
- 1# -> lvl_r2Xp
+ jump $wgo3_s1bO 1# 1#;
+ 1# -> Unlifted.fac1
}
}
--- RHS size: {terms: 32, types: 12, coercions: 0, joins: 1/1}
-Unlifted.$wmutVar [InlPrag=NOINLINE] :: forall {s} {a}. Int# -> Int#
-[GblId, Arity=1, Caf=NoCafRefs, Str=<S,U>, Unf=OtherCon []]
+-- RHS size: {terms: 32, types: 10, coercions: 0, joins: 1/1}
+Unlifted.$wmutVar [InlPrag=NOINLINE] :: forall s a. Int# -> Int#
+[GblId, Arity=1, Str=<L>, Unf=OtherCon []]
Unlifted.$wmutVar
- = \ (@ s_s2UR) (@ a_s2US) (ww_s2V0 :: Int#) ->
- case ># 1# ww_s2V0 of {
+ = \ (@s_s1bX) (@a_s1bY) (ww_s1c4 :: Int#) ->
+ case ># 1# ww_s1c4 of {
__DEFAULT ->
joinrec {
- $wgo_s2UH [InlPrag=NOUSERINLINE[2], Occ=LoopBreaker] :: Int# -> Int# -> Int#
- [LclId[JoinId(2)], Arity=2, Str=<S,U><S,U>, Unf=OtherCon []]
- $wgo_s2UH (w_s2UB :: Int#) (ww1_s2UF :: Int#)
- = case ==# w_s2UB ww_s2V0 of {
- __DEFAULT -> jump $wgo_s2UH (+# w_s2UB 1#) (*# ww1_s2UF w_s2UB);
- 1# -> *# ww1_s2UF w_s2UB
+ $wgo3_s1bO [InlPrag=[2], Occ=LoopBreaker, Dmd=SC(S,C(1,L))] :: Int# -> Int# -> Int#
+ [LclId[JoinId(2)(Nothing)], Arity=2, Str=<L><L>, Unf=OtherCon []]
+ $wgo3_s1bO (x_s1bI :: Int#) (ww1_s1bL :: Int#)
+ = case ==# x_s1bI ww_s1c4 of {
+ __DEFAULT -> jump $wgo3_s1bO (+# x_s1bI 1#) (*# ww1_s1bL x_s1bI);
+ 1# -> *# ww1_s1bL x_s1bI
}; } in
- jump $wgo_s2UH 1# 1#;
+ jump $wgo3_s1bO 1# 1#;
1# -> 1#
}
--- RHS size: {terms: 15, types: 19, coercions: 0, joins: 0/0}
-mutVar [InlPrag=NOUSERINLINE[0]] :: forall s a. MMutVar s a -> Int
+-- RHS size: {terms: 15, types: 18, coercions: 0, joins: 0/0}
+mutVar [InlPrag=NOINLINE[final]] :: forall s a. MMutVar s a -> Int
[GblId,
Arity=1,
- Caf=NoCafRefs,
- Str=<S(LS(S)),1*U(A,1*U(U))>m,
- Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True,
+ Str=<1!P(A,1!P(L))>,
+ Cpr=1,
+ Unf=Unf{Src=StableSystem, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
- Tmpl= \ (@ s_s2UR) (@ a_s2US) (w_s2UT [Occ=Once!] :: MMutVar s_s2UR a_s2US) ->
- case w_s2UT of { MMutVar _ [Occ=Dead] ww2_s2UX [Occ=Once!] ->
- case ww2_s2UX of { I# ww4_s2V0 [Occ=Once] ->
- case Unlifted.$wmutVar @ s_s2UR @ a_s2US ww4_s2V0 of ww5_s2V5 [Occ=Once] { __DEFAULT -> GHC.Types.I# ww5_s2V5 }
+ Tmpl= \ (@s_s1bX) (@a_s1bY) (ds_s1bZ [Occ=Once1!] :: MMutVar s_s1bX a_s1bY) ->
+ case ds_s1bZ of { MMutVar _ [Occ=Dead] ww1_s1c2 [Occ=Once1!] ->
+ case ww1_s1c2 of { I# ww2_s1c4 [Occ=Once1] ->
+ case Unlifted.$wmutVar @s_s1bX @a_s1bY ww2_s1c4 of ww3_s1cn [Occ=Once1] { __DEFAULT -> GHC.Types.I# ww3_s1cn }
}
}}]
mutVar
- = \ (@ s_s2UR) (@ a_s2US) (w_s2UT :: MMutVar s_s2UR a_s2US) ->
- case w_s2UT of { MMutVar ww1_s2UW ww2_s2UX ->
- case ww2_s2UX of { I# ww4_s2V0 ->
- case Unlifted.$wmutVar @ s_s2UR @ a_s2US ww4_s2V0 of ww5_s2V5 { __DEFAULT -> GHC.Types.I# ww5_s2V5 }
+ = \ (@s_s1bX) (@a_s1bY) (ds_s1bZ :: MMutVar s_s1bX a_s1bY) ->
+ case ds_s1bZ of { MMutVar ww_s1c1 ww1_s1c2 ->
+ case ww1_s1c2 of { I# ww2_s1c4 ->
+ case Unlifted.$wmutVar @s_s1bX @a_s1bY ww2_s1c4 of ww3_s1cn { __DEFAULT -> GHC.Types.I# ww3_s1cn }
}
}
--- RHS size: {terms: 31, types: 10, coercions: 0, joins: 1/1}
-Unlifted.$warray [InlPrag=NOINLINE] :: forall {a}. Int# -> Int#
-[GblId, Arity=1, Caf=NoCafRefs, Str=<S,U>, Unf=OtherCon []]
+-- RHS size: {terms: 31, types: 9, coercions: 0, joins: 1/1}
+Unlifted.$warray [InlPrag=NOINLINE] :: forall a. Int# -> Int#
+[GblId, Arity=1, Str=<L>, Unf=OtherCon []]
Unlifted.$warray
- = \ (@ a_s2V7) (ww_s2Vf :: Int#) ->
- case ># 1# ww_s2Vf of {
+ = \ (@a_s1cb) (ww_s1ch :: Int#) ->
+ case ># 1# ww_s1ch of {
__DEFAULT ->
joinrec {
- $wgo_s2UH [InlPrag=NOUSERINLINE[2], Occ=LoopBreaker] :: Int# -> Int# -> Int#
- [LclId[JoinId(2)], Arity=2, Str=<S,U><S,U>, Unf=OtherCon []]
- $wgo_s2UH (w_s2UB :: Int#) (ww1_s2UF :: Int#)
- = case ==# w_s2UB ww_s2Vf of {
- __DEFAULT -> jump $wgo_s2UH (+# w_s2UB 1#) (*# ww1_s2UF w_s2UB);
- 1# -> *# ww1_s2UF w_s2UB
+ $wgo3_s1bO [InlPrag=[2], Occ=LoopBreaker, Dmd=SC(S,C(1,L))] :: Int# -> Int# -> Int#
+ [LclId[JoinId(2)(Nothing)], Arity=2, Str=<L><L>, Unf=OtherCon []]
+ $wgo3_s1bO (x_s1bI :: Int#) (ww1_s1bL :: Int#)
+ = case ==# x_s1bI ww_s1ch of {
+ __DEFAULT -> jump $wgo3_s1bO (+# x_s1bI 1#) (*# ww1_s1bL x_s1bI);
+ 1# -> *# ww1_s1bL x_s1bI
}; } in
- jump $wgo_s2UH 1# 1#;
+ jump $wgo3_s1bO 1# 1#;
1# -> 1#
}
-- RHS size: {terms: 14, types: 13, coercions: 0, joins: 0/0}
-array [InlPrag=NOUSERINLINE[0]] :: forall a. AArray a -> Int
+array [InlPrag=NOINLINE[final]] :: forall a. AArray a -> Int
[GblId,
Arity=1,
- Caf=NoCafRefs,
- Str=<S(LS(S)),1*U(A,1*U(U))>m,
- Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True,
+ Str=<1!P(A,1!P(L))>,
+ Cpr=1,
+ Unf=Unf{Src=StableSystem, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=False)
- Tmpl= \ (@ a_s2V7) (w_s2V8 [Occ=Once!] :: AArray a_s2V7) ->
- case w_s2V8 of { AArray _ [Occ=Dead] ww2_s2Vc [Occ=Once!] ->
- case ww2_s2Vc of { I# ww4_s2Vf [Occ=Once] ->
- case Unlifted.$warray @ a_s2V7 ww4_s2Vf of ww5_s2Vk [Occ=Once] { __DEFAULT -> GHC.Types.I# ww5_s2Vk }
+ Tmpl= \ (@a_s1cb) (ds_s1cc [Occ=Once1!] :: AArray a_s1cb) ->
+ case ds_s1cc of { AArray _ [Occ=Dead] ww1_s1cf [Occ=Once1!] ->
+ case ww1_s1cf of { I# ww2_s1ch [Occ=Once1] ->
+ case Unlifted.$warray @a_s1cb ww2_s1ch of ww3_s1cp [Occ=Once1] { __DEFAULT -> GHC.Types.I# ww3_s1cp }
}
}}]
array
- = \ (@ a_s2V7) (w_s2V8 :: AArray a_s2V7) ->
- case w_s2V8 of { AArray ww1_s2Vb ww2_s2Vc ->
- case ww2_s2Vc of { I# ww4_s2Vf -> case Unlifted.$warray @ a_s2V7 ww4_s2Vf of ww5_s2Vk { __DEFAULT -> GHC.Types.I# ww5_s2Vk } }
+ = \ (@a_s1cb) (ds_s1cc :: AArray a_s1cb) ->
+ case ds_s1cc of { AArray ww_s1ce ww1_s1cf ->
+ case ww1_s1cf of { I# ww2_s1ch -> case Unlifted.$warray @a_s1cb ww2_s1ch of ww3_s1cp { __DEFAULT -> GHC.Types.I# ww3_s1cp } }
}
diff --git a/testsuite/tests/stranal/should_compile/T18982.stderr b/testsuite/tests/stranal/should_compile/T18982.stderr
index 4d1606cba97e90f02c02db201d11e7d292e024a7..6e1be6b724eea8c9007b46aef0bab328481b2408 100644
--- a/testsuite/tests/stranal/should_compile/T18982.stderr
+++ b/testsuite/tests/stranal/should_compile/T18982.stderr
@@ -1,10 +1,10 @@
==================== Tidy Core ====================
-Result size of Tidy Core = {terms: 311, types: 214, coercions: 4, joins: 0/0}
+Result size of Tidy Core = {terms: 295, types: 206, coercions: 4, joins: 0/0}
-- RHS size: {terms: 8, types: 9, coercions: 1, joins: 0/0}
T18982.$WExGADT :: forall e. (e ~ Int) => e %1 -> Int %1 -> ExGADT Int
-T18982.$WExGADT = \ (@e) (conrep :: e ~ Int) (conrep :: e) (conrep :: Int) -> T18982.ExGADT @Int @e @~(<Int>_N :: Int GHC.Prim.~# Int) conrep conrep conrep
+T18982.$WExGADT = \ (@e) (conrep :: e ~ Int) (conrep1 :: e) (conrep2 :: Int) -> T18982.ExGADT @Int @e @~(<Int>_N :: Int GHC.Prim.~# Int) conrep conrep1 conrep2
-- RHS size: {terms: 3, types: 2, coercions: 1, joins: 0/0}
T18982.$WGADT :: Int %1 -> GADT Int
@@ -12,7 +12,7 @@ T18982.$WGADT = \ (conrep :: Int) -> T18982.GADT @Int @~(<Int>_N :: Int GHC.Prim
-- RHS size: {terms: 7, types: 6, coercions: 0, joins: 0/0}
T18982.$WEx :: forall e a. e %1 -> a %1 -> Ex a
-T18982.$WEx = \ (@e) (@a) (conrep :: e) (conrep :: a) -> T18982.Ex @a @e conrep conrep
+T18982.$WEx = \ (@e) (@a) (conrep :: e) (conrep1 :: a) -> T18982.Ex @a @e conrep conrep1
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$trModule4 :: GHC.Prim.Addr#
@@ -46,22 +46,6 @@ $krep1 = GHC.Types.KindRepVar 1#
$krep2 :: GHC.Types.KindRep
$krep2 = GHC.Types.KindRepVar 0#
--- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
-$krep3 :: [GHC.Types.KindRep]
-$krep3 = GHC.Types.: @GHC.Types.KindRep $krep (GHC.Types.[] @GHC.Types.KindRep)
-
--- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
-$krep4 :: [GHC.Types.KindRep]
-$krep4 = GHC.Types.: @GHC.Types.KindRep $krep2 $krep3
-
--- RHS size: {terms: 3, types: 1, coercions: 0, joins: 0/0}
-$krep5 :: [GHC.Types.KindRep]
-$krep5 = GHC.Types.: @GHC.Types.KindRep GHC.Types.krep$* $krep4
-
--- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep6 :: GHC.Types.KindRep
-$krep6 = GHC.Types.KindRepTyConApp GHC.Types.$tc~ $krep5
-
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$tcBox2 :: GHC.Prim.Addr#
T18982.$tcBox2 = "Box"#
@@ -75,16 +59,16 @@ T18982.$tcBox :: GHC.Types.TyCon
T18982.$tcBox = GHC.Types.TyCon 16948648223906549518#Word64 2491460178135962649#Word64 T18982.$trModule T18982.$tcBox1 0# GHC.Types.krep$*Arr*
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
-$krep7 :: [GHC.Types.KindRep]
-$krep7 = GHC.Types.: @GHC.Types.KindRep $krep2 (GHC.Types.[] @GHC.Types.KindRep)
+$krep3 :: [GHC.Types.KindRep]
+$krep3 = GHC.Types.: @GHC.Types.KindRep $krep2 (GHC.Types.[] @GHC.Types.KindRep)
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep8 :: GHC.Types.KindRep
-$krep8 = GHC.Types.KindRepTyConApp T18982.$tcBox $krep7
+$krep4 :: GHC.Types.KindRep
+$krep4 = GHC.Types.KindRepTyConApp T18982.$tcBox $krep3
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'Box1 :: GHC.Types.KindRep
-T18982.$tc'Box1 = GHC.Types.KindRepFun $krep2 $krep8
+T18982.$tc'Box1 = GHC.Types.KindRepFun $krep2 $krep4
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'Box3 :: GHC.Prim.Addr#
@@ -111,20 +95,20 @@ T18982.$tcEx :: GHC.Types.TyCon
T18982.$tcEx = GHC.Types.TyCon 4376661818164435927#Word64 18005417598910668817#Word64 T18982.$trModule T18982.$tcEx1 0# GHC.Types.krep$*Arr*
-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
-$krep9 :: [GHC.Types.KindRep]
-$krep9 = GHC.Types.: @GHC.Types.KindRep $krep1 (GHC.Types.[] @GHC.Types.KindRep)
+$krep5 :: [GHC.Types.KindRep]
+$krep5 = GHC.Types.: @GHC.Types.KindRep $krep1 (GHC.Types.[] @GHC.Types.KindRep)
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep10 :: GHC.Types.KindRep
-$krep10 = GHC.Types.KindRepTyConApp T18982.$tcEx $krep9
+$krep6 :: GHC.Types.KindRep
+$krep6 = GHC.Types.KindRepTyConApp T18982.$tcEx $krep5
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep11 :: GHC.Types.KindRep
-$krep11 = GHC.Types.KindRepFun $krep1 $krep10
+$krep7 :: GHC.Types.KindRep
+$krep7 = GHC.Types.KindRepFun $krep1 $krep6
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'Ex1 :: GHC.Types.KindRep
-T18982.$tc'Ex1 = GHC.Types.KindRepFun $krep2 $krep11
+T18982.$tc'Ex1 = GHC.Types.KindRepFun $krep2 $krep7
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'Ex3 :: GHC.Prim.Addr#
@@ -150,13 +134,17 @@ T18982.$tcGADT1 = GHC.Types.TrNameS T18982.$tcGADT2
T18982.$tcGADT :: GHC.Types.TyCon
T18982.$tcGADT = GHC.Types.TyCon 9243924476135839950#Word64 5096619276488416461#Word64 T18982.$trModule T18982.$tcGADT1 0# GHC.Types.krep$*Arr*
+-- RHS size: {terms: 3, types: 2, coercions: 0, joins: 0/0}
+$krep8 :: [GHC.Types.KindRep]
+$krep8 = GHC.Types.: @GHC.Types.KindRep $krep (GHC.Types.[] @GHC.Types.KindRep)
+
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep12 :: GHC.Types.KindRep
-$krep12 = GHC.Types.KindRepTyConApp T18982.$tcGADT $krep3
+$krep9 :: GHC.Types.KindRep
+$krep9 = GHC.Types.KindRepTyConApp T18982.$tcGADT $krep8
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'GADT1 :: GHC.Types.KindRep
-T18982.$tc'GADT1 = GHC.Types.KindRepFun $krep $krep12
+T18982.$tc'GADT1 = GHC.Types.KindRepFun $krep $krep9
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'GADT3 :: GHC.Prim.Addr#
@@ -183,20 +171,16 @@ T18982.$tcExGADT :: GHC.Types.TyCon
T18982.$tcExGADT = GHC.Types.TyCon 6470898418160489500#Word64 10361108917441214060#Word64 T18982.$trModule T18982.$tcExGADT1 0# GHC.Types.krep$*Arr*
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep13 :: GHC.Types.KindRep
-$krep13 = GHC.Types.KindRepTyConApp T18982.$tcExGADT $krep3
-
--- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep14 :: GHC.Types.KindRep
-$krep14 = GHC.Types.KindRepFun $krep $krep13
+$krep10 :: GHC.Types.KindRep
+$krep10 = GHC.Types.KindRepTyConApp T18982.$tcExGADT $krep8
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
-$krep15 :: GHC.Types.KindRep
-$krep15 = GHC.Types.KindRepFun $krep2 $krep14
+$krep11 :: GHC.Types.KindRep
+$krep11 = GHC.Types.KindRepFun $krep $krep10
-- RHS size: {terms: 3, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'ExGADT1 :: GHC.Types.KindRep
-T18982.$tc'ExGADT1 = GHC.Types.KindRepFun $krep6 $krep15
+T18982.$tc'ExGADT1 = GHC.Types.KindRepFun $krep2 $krep11
-- RHS size: {terms: 1, types: 0, coercions: 0, joins: 0/0}
T18982.$tc'ExGADT3 :: GHC.Prim.Addr#
@@ -211,7 +195,7 @@ T18982.$tc'ExGADT :: GHC.Types.TyCon
T18982.$tc'ExGADT = GHC.Types.TyCon 8468257409157161049#Word64 5503123603717080600#Word64 T18982.$trModule T18982.$tc'ExGADT2 1# T18982.$tc'ExGADT1
-- RHS size: {terms: 11, types: 10, coercions: 0, joins: 0/0}
-T18982.$wi :: forall {a} {e}. (a GHC.Prim.~# Int) => e -> GHC.Prim.Int# -> GHC.Prim.Int#
+T18982.$wi :: forall a e. (a GHC.Prim.~# Int) => e -> GHC.Prim.Int# -> GHC.Prim.Int#
T18982.$wi = \ (@a) (@e) (ww :: a GHC.Prim.~# Int) (ww1 :: e) (ww2 :: GHC.Prim.Int#) -> case ww1 of { __DEFAULT -> GHC.Prim.+# ww2 1# }
-- RHS size: {terms: 15, types: 22, coercions: 1, joins: 0/0}
@@ -219,7 +203,7 @@ i :: forall a. ExGADT a -> Int
i = \ (@a) (ds :: ExGADT a) -> case ds of { ExGADT @e ww ww1 ww2 ww3 -> case ww3 of { GHC.Types.I# ww4 -> case T18982.$wi @a @e @~(ww :: a GHC.Prim.~# Int) ww2 ww4 of ww5 { __DEFAULT -> GHC.Types.I# ww5 } } }
-- RHS size: {terms: 6, types: 7, coercions: 0, joins: 0/0}
-T18982.$wh :: forall {a}. (a GHC.Prim.~# Int) => GHC.Prim.Int# -> GHC.Prim.Int#
+T18982.$wh :: forall a. (a GHC.Prim.~# Int) => GHC.Prim.Int# -> GHC.Prim.Int#
T18982.$wh = \ (@a) (ww :: a GHC.Prim.~# Int) (ww1 :: GHC.Prim.Int#) -> GHC.Prim.+# ww1 1#
-- RHS size: {terms: 14, types: 15, coercions: 1, joins: 0/0}
@@ -227,7 +211,7 @@ h :: forall a. GADT a -> Int
h = \ (@a) (ds :: GADT a) -> case ds of { GADT ww ww1 -> case ww1 of { GHC.Types.I# ww2 -> case T18982.$wh @a @~(ww :: a GHC.Prim.~# Int) ww2 of ww3 { __DEFAULT -> GHC.Types.I# ww3 } } }
-- RHS size: {terms: 9, types: 4, coercions: 0, joins: 0/0}
-T18982.$wg :: forall {e}. e -> GHC.Prim.Int# -> GHC.Prim.Int#
+T18982.$wg :: forall e. e -> GHC.Prim.Int# -> GHC.Prim.Int#
T18982.$wg = \ (@e) (ww :: e) (ww1 :: GHC.Prim.Int#) -> case ww of { __DEFAULT -> GHC.Prim.+# ww1 1# }
-- RHS size: {terms: 14, types: 11, coercions: 0, joins: 0/0}
diff --git a/testsuite/tests/stranal/should_compile/T23398.stderr b/testsuite/tests/stranal/should_compile/T23398.stderr
index 84177a1424f2a650923a5a89150477e5021eda14..03a7dbb9fd0c62b26f6217c59af7f57b05ad6e28 100644
--- a/testsuite/tests/stranal/should_compile/T23398.stderr
+++ b/testsuite/tests/stranal/should_compile/T23398.stderr
@@ -5,7 +5,7 @@ Result size of Tidy Core
-- RHS size: {terms: 18, types: 11, coercions: 0, joins: 0/0}
T23398.$wfoo [InlPrag=[2]]
- :: forall {a}. (Eq a, Show a) => a -> a -> String
+ :: forall a. (Eq a, Show a) => a -> a -> String
[GblId[StrictWorker([!, !])],
Arity=4,
Str=<SP(1C(1,C(1,L)),A)><SP(A,1C(1,L),A)><L><L>,
@@ -41,7 +41,7 @@ foo
Rec {
-- RHS size: {terms: 21, types: 19, coercions: 3, joins: 0/0}
T23398.$wbar [InlPrag=[2], Occ=LoopBreaker]
- :: forall {a} {b}.
+ :: forall a b.
(a GHC.Prim.~# b, Show a) =>
GHC.Prim.Int# -> a -> (# b, String #)
[GblId[StrictWorker([~, !])],
diff --git a/testsuite/tests/typecheck/should_compile/CoerceToVDQ.hs b/testsuite/tests/typecheck/should_compile/CoerceToVDQ.hs
new file mode 100644
index 0000000000000000000000000000000000000000..0305683a596a9f7cc460e0e4988c7f3f0d5ff8c2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/CoerceToVDQ.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE ImpredicativeTypes, TypeFamilies, UndecidableInstances #-}
+module CoerceToVDQ where
+
+import Data.Kind
+import GHC.Exts (UnliftedType)
+
+import Data.Coerce
+
+type S0 = forall (k :: Type) -> k -> k
+
+type family S where
+ -- S just smuggles S0 past the validity checks
+ -- that normally prevent VDQ in types of terms
+ S = ArgKind (S0Consumer S0Inhabitant)
+
+type ArgKind :: Type -> Type
+type family ArgKind a where
+ ArgKind (_ (arg :: k)) = k
+
+type S0Inhabitant :: S0
+data family S0Inhabitant a b
+
+type S0Consumer :: S0 -> Type
+newtype S0Consumer f = Con (f Type Bool)
+
+test :: S
+test = coerce @(forall t. t -> t) id
diff --git a/testsuite/tests/typecheck/should_compile/T22537.hs b/testsuite/tests/typecheck/should_compile/T22537.hs
new file mode 100644
index 0000000000000000000000000000000000000000..8bb892c4558f7412ac4d47c8ad3f5037a33c859d
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22537.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE ExplicitForAll #-}
+
+module T22537 where
+
+import Data.Coerce
+
+newtype M = MkM (forall a b. a -> b -> b)
+newtype N a = MkN (forall b. a -> b -> b)
+newtype P = MkP (forall a. N a)
+
+g1 :: M -> P
+g1 x = coerce x
+
+g2 :: P -> M
+g2 x = coerce x
diff --git a/testsuite/tests/typecheck/should_compile/T22762.hs b/testsuite/tests/typecheck/should_compile/T22762.hs
new file mode 100644
index 0000000000000000000000000000000000000000..2c343fde4b128e749aad24b25cfa4099ac44e9c0
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T22762.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE GHC2021 #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Bug where
+
+import Data.Kind
+
+type Const :: a -> b -> a
+type family Const x y where
+ Const x _ = x
+
+type F :: (forall (b :: Bool) -> Const Type b) -> Type
+data F f
+
+type G :: forall (b :: Bool) -> Type
+data G b
+
+type H :: Type
+type family H where
+ H = F G
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 13bb8cbd501c445e0de3263b4416e0749e9c3e75..edcc812181e52932717c819eb682f6c1a654657b 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -871,6 +871,8 @@ test('T22194', normal, compile, [''])
test('QualifiedRecordUpdate',
[ extra_files(['QualifiedRecordUpdate_aux.hs']) ]
, multimod_compile, ['QualifiedRecordUpdate', '-v0'])
+test('CoerceToVDQ', normal, compile, ['-dlint'])
+test('T22762', normal, compile, ['-dlint'])
test('T23171', normal, compile, [''])
test('T23192', normal, compile, [''])
test('T23199', normal, compile, [''])
@@ -883,3 +885,5 @@ test('T22560d', extra_files(['T22560d.hs']), ghci_script, ['T22560d.script'])
test('T22560e', normal, compile, [''])
test('T23514b', normal, compile, [''])
test('T23514c', normal, compile, [''])
+test('T22537', normal, compile, [''])
+