Simon Peyton Jones pushed to branch wip/T26369 at Glasgow Haskell Compiler / GHC
Commits:
2897da11 by Simon Peyton Jones at 2025-09-04T12:58:10+01:00
Refactor ForAllCo
This is a pure refactor, addressing #26389.
It arranges that the kind coercion in a ForAllCo is a MCoercion, rather
than a plain Coercion, thus removing redundancy in the common case.
See (FC8) in Note [ForAllCo]
It's a nice cleanup.
- - - - -
22 changed files:
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Reduction.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Subst.hs
- compiler/GHC/Core/TyCo/Tidy.hs
- compiler/GHC/Core/Type.hs
- compiler/GHC/Core/Unify.hs
- compiler/GHC/CoreToIface.hs
- compiler/GHC/Iface/Rename.hs
- compiler/GHC/Iface/Syntax.hs
- compiler/GHC/Iface/Type.hs
- compiler/GHC/IfaceToCore.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Tc/Utils/TcType.hs
- compiler/GHC/Types/Id/Make.hs
- testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr
Changes:
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -47,7 +47,7 @@ module GHC.Core.Coercion (
mkProofIrrelCo,
downgradeRole,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
- mkKindCo,
+ mkKindCo, forAllCoKindCo,
castCoercionKind, castCoercionKind1, castCoercionKind2,
-- ** Decomposition
@@ -66,11 +66,14 @@ module GHC.Core.Coercion (
tyConRoleListX, tyConRoleListRepresentational, funRole,
pickLR,
- isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
- isReflCoVar_maybe, isGReflMCo, mkGReflLeftMCo, mkGReflRightMCo,
+ isReflKindCo,isReflKindMCo,
+ isReflCo, isReflCo_maybe,
+ isReflexiveMCo, isReflexiveCo, isReflexiveCo_maybe,
+ isReflCoVar_maybe, mkGReflLeftMCo, mkGReflRightMCo,
mkCoherenceRightMCo,
- coToMCo, mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo,
+ coToMCo, kindCoToMKindCo,
+ mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo,
mkFunResMCo, mkPiMCos,
isReflMCo, checkReflexiveMCo,
@@ -85,7 +88,7 @@ module GHC.Core.Coercion (
-- ** Substitution
CvSubstEnv, emptyCvSubstEnv,
lookupCoVar,
- substCo, substCos, substCoVar, substCoVars, substCoWith,
+ substCo, substCos, substCoVar, substCoVars, substCoWithInScope,
substCoVarBndr,
extendTvSubstAndInScope, getCvSubstEnv,
@@ -317,23 +320,23 @@ coToMCo :: Coercion -> MCoercion
coToMCo co | isReflCo co = MRefl
| otherwise = MCo co
+kindCoToMKindCo :: KindCoercion -> KindMCoercion
+-- Convert a KindCoercion to a KindMCoercion,
+-- coToMCo doesn't eliminate GRefl, but kindCoToMCo can
+-- See Note [KindCoercion]
+kindCoToMKindCo co | isReflKindCo co = MRefl
+ | otherwise = MCo co
+
checkReflexiveMCo :: MCoercion -> MCoercion
checkReflexiveMCo MRefl = MRefl
checkReflexiveMCo (MCo co) | isReflexiveCo co = MRefl
| otherwise = MCo co
--- | Tests if this MCoercion is obviously generalized reflexive
--- Guaranteed to work very quickly.
-isGReflMCo :: MCoercion -> Bool
-isGReflMCo MRefl = True
-isGReflMCo (MCo co) | isGReflCo co = True
-isGReflMCo _ = False
-
-- | Make a generalized reflexive coercion
mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflCo r ty mco
- | isGReflMCo mco = if r == Nominal then Refl ty
- else GRefl r ty MRefl
+ | isReflKindMCo mco = if r == Nominal then Refl ty
+ else GRefl r ty MRefl
| otherwise
= -- I'd like to have this assert, but sadly it's not true during type
-- inference because the types are not fully zonked
@@ -565,10 +568,13 @@ 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, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
+splitForAllCo_maybe :: Coercion
+ -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion)
+-- You might think that this function should return KindMCoercion (rather
+-- than a KindCoercion), but in fact most of the clients want a KindCoercion.
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)
+ , fco_kind = k_mco, fco_body = co })
+ = Just (tv, vL, vR, forAllCoKindCo tv k_mco, co)
splitForAllCo_maybe co
| Just (ty, r) <- isReflCo_maybe co
, Just (Bndr tcv vis, body_ty) <- splitForAllForAllTyBinder_maybe ty
@@ -576,7 +582,8 @@ splitForAllCo_maybe co
splitForAllCo_maybe _ = Nothing
-- | Like 'splitForAllCo_maybe', but only returns Just for tyvar binder
-splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
+splitForAllCo_ty_maybe :: Coercion
+ -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion)
splitForAllCo_ty_maybe co
| Just stuff@(tv, _, _, _, _) <- splitForAllCo_maybe co
, isTyVar tv
@@ -584,7 +591,8 @@ splitForAllCo_ty_maybe co
splitForAllCo_ty_maybe _ = Nothing
-- | Like 'splitForAllCo_maybe', but only returns Just for covar binder
-splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
+splitForAllCo_co_maybe :: Coercion
+ -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion)
splitForAllCo_co_maybe co
| Just stuff@(cv, _, _, _, _) <- splitForAllCo_maybe co
, isCoVar cv
@@ -676,34 +684,50 @@ isReflCoVar_maybe cv
| otherwise
= Nothing
--- | Tests if this coercion is obviously a generalized reflexive coercion.
+-- | Tests whether this is a "kind coercion":
+-- that is, Nominal and between two types of kind @Type@.
+-- See Note [KindCoercion] in GHC.Core.TyCo.Rep
+isKindCo :: Coercion -> Bool
+isKindCo co
+ = role == Nominal && isLiftedTypeKind kk1 && isLiftedTypeKind kk2
+ where
+ (Pair kk1 kk2, role) = coercionKindRole co
+
+-- | Tests if this /kind/ coercion is Refl
+-- Guaranteed to work very quickly.
+-- PRECONDITION: the argument is a KindCoercion
+-- So if it sees (GRefl k (MCo kk)) :: k ~ (k |> kk)
+-- then we know that kk must be reflexive.
+-- And hence if co = GRefl {} then it is equivalent to Refl,
+-- because GRefl N ty MRefl = Refl ty
+-- so we return True
+-- See Note [KindCoercion] in GHC.Core.TyCo.Rep
+isReflKindCo :: HasDebugCallStack => KindCoercion -> Bool
+isReflKindCo co@(GRefl {}) = assertPpr (isKindCo co) (ppr co) $
+ True
+isReflKindCo (Refl{}) = True -- Refl ty == GRefl N ty MRefl
+isReflKindCo _ = False
+
+-- | Tests if this /kind/ MCoercion is obviously generalized reflexive
-- Guaranteed to work very quickly.
-isGReflCo :: Coercion -> Bool
-isGReflCo (GRefl{}) = True
-isGReflCo (Refl{}) = True -- Refl ty == GRefl N ty MRefl
-isGReflCo _ = False
+isReflKindMCo :: KindMCoercion -> Bool
+isReflKindMCo MRefl = True
+isReflKindMCo (MCo co) = isReflKindCo co
-- | Tests if this coercion is obviously reflexive. Guaranteed to work
-- very quickly. Sometimes a coercion can be reflexive, but not obviously
-- so. c.f. 'isReflexiveCo'
isReflCo :: Coercion -> Bool
isReflCo (Refl{}) = True
-isReflCo (GRefl _ _ mco) | isGReflMCo mco = True
+isReflCo (GRefl _ _ mco) | isReflKindMCo mco = True
isReflCo _ = False
--- | Returns the type coerced if this coercion is a generalized reflexive
--- coercion. Guaranteed to work very quickly.
-isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
-isGReflCo_maybe (GRefl r ty _) = Just (ty, r)
-isGReflCo_maybe (Refl ty) = Just (ty, Nominal)
-isGReflCo_maybe _ = Nothing
-
-- | Returns the type coerced if this coercion is reflexive. Guaranteed
-- to work very quickly. Sometimes a coercion can be reflexive, but not
-- obviously so. c.f. 'isReflexiveCo_maybe'
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe (Refl ty) = Just (ty, Nominal)
-isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
+isReflCo_maybe (GRefl r ty mco) | isReflKindMCo mco = Just (ty, r)
isReflCo_maybe _ = Nothing
-- | Slowly checks if the coercion is reflexive. Don't call this in a loop,
@@ -711,11 +735,15 @@ isReflCo_maybe _ = Nothing
isReflexiveCo :: Coercion -> Bool
isReflexiveCo = isJust . isReflexiveCo_maybe
+isReflexiveMCo :: MCoercion -> Bool
+isReflexiveMCo MRefl = True
+isReflexiveMCo (MCo co) = isReflexiveCo co
+
-- | Extracts the coerced type from a reflexive coercion. This potentially
-- walks over the entire coercion, so avoid doing this in a loop.
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)
-isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
+isReflexiveCo_maybe (GRefl r ty mco) | isReflKindMCo mco = Just (ty, r)
isReflexiveCo_maybe co
| ty1 `eqType` ty2
= Just (ty1, r)
@@ -723,6 +751,10 @@ isReflexiveCo_maybe co
= Nothing
where (Pair ty1 ty2, r) = coercionKindRole co
+forAllCoKindCo :: TyCoVar -> KindMCoercion -> KindCoercion
+-- Get the kind coercion from a ForAllCo
+forAllCoKindCo _ (MCo co) = co
+forAllCoKindCo tcv MRefl = mkNomReflCo (varType tcv)
{-
%************************************************************************
@@ -939,10 +971,11 @@ mkAppCos co1 cos = foldl' mkAppCo co1 cos
-- | Make a Coercion from a tycovar, a kind coercion, and a body coercion.
-mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
+mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag
+ -> KindMCoercion -> Coercion -> Coercion
mkForAllCo v visL visR kind_co co
| Just (ty, r) <- isReflCo_maybe co
- , isReflCo kind_co
+ , isReflMCo kind_co
, visL `eqForAllVis` visR
= mkReflCo r (mkTyCoForAllTy v visL ty)
@@ -955,8 +988,7 @@ mkForAllCo v visL visR kind_co co
mkForAllVisCos :: HasDebugCallStack => [ForAllTyBinder] -> Coercion -> Coercion
mkForAllVisCos bndrs orig_co = foldr go orig_co bndrs
where
- go (Bndr tv vis)
- = mkForAllCo tv coreTyLamForAllTyFlag vis (mkNomReflCo (varType tv))
+ go (Bndr tv vis) = mkForAllCo tv coreTyLamForAllTyFlag vis MRefl
-- | Make a Coercion quantified over a type/coercion variable;
-- the variable has the same kind and visibility in both sides of the coercion
@@ -967,29 +999,30 @@ mkHomoForAllCos vs orig_co
| otherwise
= foldr go orig_co vs
where
- go (Bndr var vis) co
- = mkForAllCo_NoRefl var vis vis (mkNomReflCo (varType var)) co
+ go :: ForAllTyBinder -> Coercion -> Coercion
+ go (Bndr var vis) = mkForAllCo_NoRefl var vis vis MRefl
-- | 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 :: TyCoVar -> ForAllTyFlag -> ForAllTyFlag
+ -> KindMCoercion -> 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) $
+ assertPpr (not (isReflCo co && isReflMCo 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
+ => TyCoVar -> ForAllTyFlag -> ForAllTyFlag
+ -> KindMCoercion -> 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
+ = assertPpr tcv_kind_co_agree doc
| otherwise
- = assertPpr (tcv_type `eqType` kind_co_lkind) doc
+ = assertPpr tcv_kind_co_agree 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
@@ -998,13 +1031,17 @@ assertGoodForAllCo tcv visL visR kind_co co
-- See (FC7) in Note [ForAllCo] in GHC.Core.TyCo.Rep
where
tcv_type = varType tcv
- kind_co_lkind = coercionLKind kind_co
+ tcv_kind_co_agree = case kind_co of
+ MRefl -> True
+ MCo co -> tcv_type `eqType` coercionLKind 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 "kind_co:" <+> pp_kind_co
, text "body_co" <+> ppr co ]
+ pp_kind_co = case kind_co of
+ MRefl -> text "MRefl"
+ MCo co -> ppr co <+> dcolon <+> ppr (coercionKind co)
mkNakedForAllCo :: TyVar -- Never a CoVar
@@ -1024,7 +1061,7 @@ mkNakedForAllCo tv visL visR kind_co co
= 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 }
+ , fco_kind = MCo kind_co, fco_body = co }
mkCoVarCo :: CoVar -> Coercion
@@ -1149,7 +1186,7 @@ mkSymCo co | isReflCo co = co
mkSymCo (SymCo co) = co
mkSymCo (SubCo (SymCo co)) = SubCo co
mkSymCo co@(ForAllCo { fco_kind = kco, fco_body = body_co })
- | isReflCo kco = co { fco_body = mkSymCo body_co }
+ | isReflMCo kco = co { fco_body = mkSymCo body_co }
mkSymCo co = SymCo co
-- | mkTransCo creates a new 'Coercion' by composing the two
@@ -1193,8 +1230,8 @@ mkSelCo_maybe cs co
go cs co
where
- go SelForAll (ForAllCo { fco_kind = kind_co })
- = Just kind_co
+ go SelForAll (ForAllCo { fco_tcv = tcv, fco_kind = kind_co })
+ = Just (forAllCoKindCo tcv kind_co)
-- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
-- then (nth SelForAll co :: k1 ~N k2)
-- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
@@ -1312,46 +1349,45 @@ mkInstCo :: Coercion -> CoercionN -> Coercion
mkInstCo co_fun co_arg
| Just (tcv, _, _, kind_co, body_co) <- splitForAllCo_maybe co_fun
, Just (arg, _) <- isReflCo_maybe co_arg
+ , let in_scope = mkInScopeSet $
+ tyCoVarsOfType arg `unionVarSet` tyCoVarsOfCo body_co
+ subst = extendTCvSubst (mkEmptySubst in_scope) tcv arg
= assertPpr (isReflexiveCo kind_co) (ppr co_fun $$ ppr co_arg) $
-- If the arg is Refl, then kind_co must be reflexive too
- substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
+ substCo subst body_co
mkInstCo co arg = InstCo co arg
-- | Given @ty :: k1@, @co :: k1 ~ k2@,
-- produces @co' :: ty ~r (ty |> co)@
-mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
+mkGReflRightCo :: Role -> Type -> KindCoercion -> Coercion
mkGReflRightCo r ty co
- | isGReflCo co = mkReflCo r ty
- -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
- -- instead of @isReflCo@
- | otherwise = mkGReflMCo r ty co
+ | isReflKindCo co = mkReflCo r ty -- Homo (tested) AND nominal (I promise) => Refl
+ | otherwise = mkGReflMCo r ty co
-- | Given @r@, @ty :: k1@, and @co :: k1 ~N k2@,
-- produces @co' :: (ty |> co) ~r ty@
-mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
+mkGReflLeftCo :: Role -> Type -> KindCoercion -> Coercion
mkGReflLeftCo r ty co
- | isGReflCo co = mkReflCo r ty
- -- the kinds of @k1@ and @k2@ are the same, thus @isGReflCo@
- -- instead of @isReflCo@
- | otherwise = mkSymCo $ mkGReflMCo r ty co
+ | isReflKindCo co = mkReflCo r ty
+ | otherwise = mkSymCo $ mkGReflMCo r ty co
-- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty ~r ty'@,
-- produces @co' :: (ty |> co) ~r ty'
-- It is not only a utility function, but it saves allocation when co
-- is a GRefl coercion.
-mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
+mkCoherenceLeftCo :: Role -> Type -> KindCoercion -> Coercion -> Coercion
mkCoherenceLeftCo r ty co co2
- | isGReflCo co = co2
- | otherwise = (mkSymCo $ mkGReflMCo r ty co) `mkTransCo` co2
+ | isReflKindCo co = co2
+ | otherwise = (mkSymCo $ mkGReflMCo r ty co) `mkTransCo` co2
-- | Given @ty :: k1@, @co :: k1 ~ k2@, @co2:: ty' ~r ty@,
-- produces @co' :: ty' ~r (ty |> co)
-- It is not only a utility function, but it saves allocation when co
-- is a GRefl coercion.
-mkCoherenceRightCo :: HasDebugCallStack => Role -> Type -> CoercionN -> Coercion -> Coercion
+mkCoherenceRightCo :: HasDebugCallStack => Role -> Type -> KindCoercion -> Coercion -> Coercion
mkCoherenceRightCo r ty co co2
- | isGReflCo co = co2
- | otherwise = co2 `mkTransCo` mkGReflMCo r ty co
+ | isReflKindCo co = co2
+ | otherwise = co2 `mkTransCo` mkGReflMCo r ty co
-- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
mkKindCo :: Coercion -> Coercion
@@ -1411,18 +1447,19 @@ downgradeRole r1 r2 co
Nothing -> pprPanic "downgradeRole" (ppr co)
-- | Make a "coercion between coercions".
-mkProofIrrelCo :: Role -- ^ role of the created coercion, "r"
- -> CoercionN -- ^ :: phi1 ~N phi2
- -> Coercion -- ^ g1 :: phi1
- -> Coercion -- ^ g2 :: phi2
- -> Coercion -- ^ :: g1 ~r g2
+mkProofIrrelCo :: Role -- ^ role of the created coercion, "r"
+ -> KindCoercion -- ^ :: phi1 ~N phi2
+ -> Coercion -- ^ g1 :: phi1
+ -> Coercion -- ^ g2 :: phi2
+ -> Coercion -- ^ :: g1 ~r g2
-- if the two coercion prove the same fact, I just don't care what
-- the individual coercions are.
-mkProofIrrelCo r co g _ | isGReflCo co = mkReflCo r (mkCoercionTy g)
- -- kco is a kind coercion, thus @isGReflCo@ rather than @isReflCo@
-mkProofIrrelCo r kco g1 g2 = mkUnivCo ProofIrrelProv [kco] r
- (mkCoercionTy g1) (mkCoercionTy g2)
+mkProofIrrelCo r kco g1 g2
+ | isReflKindCo kco = mkReflCo r (mkCoercionTy g1)
+ -- kco is a kind coercion, thus @isReflKindCo@ rather than @isReflCo@
+ | otherwise = mkUnivCo ProofIrrelProv [kco] r
+ (mkCoercionTy g1) (mkCoercionTy g2)
{-
%************************************************************************
@@ -2165,16 +2202,17 @@ ty_co_subst !lc role ty
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 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
+ = let (lc', v', k_co) = liftCoSubstVarBndr lc v
+ body_co = ty_co_subst lc' r ty
+ k_mco = kindCoToMKindCo k_co
+ 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
-- (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
+ then mkForAllCo v' vis vis k_mco body_co
else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
go r ty@(LitTy {}) = assert (r == Nominal) $
mkNomReflCo ty
@@ -2262,6 +2300,7 @@ liftCoSubstVarBndr :: LiftingContext -> TyCoVar
liftCoSubstVarBndr lc tv
= liftCoSubstVarBndrUsing id callback lc tv
where
+ callback :: LiftingContext -> Type -> Coercion
callback lc' ty' = ty_co_subst lc' Nominal ty'
-- the callback must produce a nominal coercion
@@ -2424,7 +2463,7 @@ seqCo (SubCo co) = seqCo co
seqCo (AxiomCo _ cs) = seqCos cs
seqCo (ForAllCo tv visL visR k co)
= seqType (varType tv) `seq` rnf visL `seq` rnf visR `seq`
- seqCo k `seq` seqCo co
+ seqMCo 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 (UnivCo { uco_prov = p, uco_role = r
@@ -2522,7 +2561,7 @@ coercion_lr_kind which orig_co
, fco_kind = k_co, fco_body = co1 })
= case which of
CLeft -> mkTyCoForAllTy tv1 visL (go co1)
- CRight | isGReflCo k_co -- kind_co always has kind `Type`, thus `isGReflCo`
+ CRight | isReflKindMCo k_co
-> mkTyCoForAllTy tv1 visR (go co1)
| otherwise
-> go_forall_right empty_subst co
@@ -2577,43 +2616,47 @@ coercion_lr_kind which orig_co
-------------
go_forall_right subst (ForAllCo { fco_tcv = tv1, fco_visR = visR
- , fco_kind = k_co, fco_body = co })
+ , fco_kind = k_mco, fco_body = co })
-- See Note [Nested ForAllCos]
| isTyVar tv1
- = mkForAllTy (Bndr tv2 visR) (go_forall_right subst' co)
- where
- k2 = coercionRKind k_co
- tv2 = setTyVarKind tv1 (substTy subst k2)
- subst' | isGReflCo k_co = extendSubstInScope subst tv1
- -- kind_co always has kind @Type@, thus @isGReflCo@
- | otherwise = extendTvSubst (extendSubstInScope subst tv2) tv1 $
- TyVarTy tv2 `mkCastTy` mkSymCo k_co
+ = case k_mco of
+ MRefl -> mkForAllTy (Bndr tv1 visR) (go_forall_right subst' co)
+ where
+ subst' = extendSubstInScope subst tv1
+ MCo k_co -> mkForAllTy (Bndr tv2 visR) (go_forall_right subst' co)
+ where
+ k2 = coercionRKind k_co
+ tv2 = setTyVarKind tv1 (substTy subst k2)
+ subst' = extendTvSubst (extendSubstInScope subst tv2) tv1 $
+ TyVarTy tv2 `mkCastTy` mkSymCo k_co
go_forall_right subst (ForAllCo { fco_tcv = cv1, fco_visR = visR
- , fco_kind = k_co, fco_body = co })
+ , fco_kind = k_mco, fco_body = co })
| isCoVar cv1
- = mkTyCoForAllTy cv2 visR (go_forall_right subst' co)
- where
- k2 = coercionRKind k_co
- r = coVarRole cv1
- k_co' = downgradeRole r Nominal k_co
- eta1 = mkSelCo (SelTyCon 2 r) k_co'
- eta2 = mkSelCo (SelTyCon 3 r) k_co'
-
- -- k_co :: (t1 ~r t2) ~N (s1 ~r s2)
- -- k1 = t1 ~r t2
- -- k2 = s1 ~r s2
- -- cv1 :: t1 ~r t2
- -- cv2 :: s1 ~r s2
- -- eta1 :: t1 ~r s1
- -- eta2 :: t2 ~r s2
- -- n_subst = (eta1 ; cv2 ; sym eta2) :: t1 ~r t2
-
- cv2 = setVarType cv1 (substTy subst k2)
- n_subst = eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2)
- subst' | isReflCo k_co = extendSubstInScope subst cv1
- | otherwise = extendCvSubst (extendSubstInScope subst cv2)
- cv1 n_subst
+ = case k_mco of
+ MRefl -> mkTyCoForAllTy cv1 visR (go_forall_right subst' co)
+ where
+ subst' = extendSubstInScope subst cv1
+ MCo k_co -> mkTyCoForAllTy cv2 visR (go_forall_right subst' co)
+ where
+ k2 = coercionRKind k_co
+ r = coVarRole cv1
+ k_co' = downgradeRole r Nominal k_co
+ eta1 = mkSelCo (SelTyCon 2 r) k_co'
+ eta2 = mkSelCo (SelTyCon 3 r) k_co'
+
+ -- k_co :: (t1 ~r t2) ~N (s1 ~r s2)
+ -- k1 = t1 ~r t2
+ -- k2 = s1 ~r s2
+ -- cv1 :: t1 ~r t2
+ -- cv2 :: s1 ~r s2
+ -- eta1 :: t1 ~r s1
+ -- eta2 :: t2 ~r s2
+ -- n_subst = (eta1 ; cv2 ; sym eta2) :: t1 ~r t2
+
+ cv2 = setVarType cv1 (substTy subst k2)
+ n_subst = eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2)
+ subst' = extendCvSubst (extendSubstInScope subst cv2) cv1 n_subst
go_forall_right subst other_co
-- when other_co is not a ForAllCo
@@ -2729,7 +2772,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
go (ForAllTy (Bndr tv1 flag1) ty1) (ForAllTy (Bndr tv2 flag2) ty2)
| isTyVar tv1
= assert (isTyVar tv2) $
- mkForAllCo tv1 flag1 flag2 kind_co (go ty1 ty2')
+ mkForAllCo tv1 flag1 flag2 (kindCoToMKindCo 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]
@@ -2738,7 +2781,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
go (ForAllTy (Bndr cv1 flag1) ty1) (ForAllTy (Bndr cv2 flag2) ty2)
= assert (isCoVar cv1 && isCoVar cv2) $
- mkForAllCo cv1 flag1 flag2 kind_co (go ty1 ty2')
+ mkForAllCo cv1 flag1 flag2 (kindCoToMKindCo kind_co) (go ty1 ty2')
where s1 = varType cv1
s2 = varType cv2
kind_co = go s1 s2
@@ -2755,7 +2798,7 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
eta2 = mkSelCo (SelTyCon 3 r) kind_co'
subst = mkEmptySubst $ mkInScopeSet $
- tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
+ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
ty2' = substTy (extendCvSubst subst cv2 $ mkSymCo eta1 `mkTransCo`
mkCoVarCo cv1 `mkTransCo`
eta2)
=====================================
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 :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> Coercion -> Coercion -> Coercion
+mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> MCoercion -> Coercion -> Coercion
mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
@@ -37,7 +37,6 @@ mkAxiomCo :: CoAxiomRule -> [Coercion] -> Coercion
funRole :: Role -> FunSel -> Role
-isGReflCo :: Coercion -> Bool
isReflCo :: Coercion -> Bool
isReflexiveCo :: Coercion -> Bool
decomposePiCos :: HasDebugCallStack => Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -177,12 +177,12 @@ optCoercion opts env co
= optCoercion' env co
{-
- = pprTrace "optCoercion {" (text "Co:" <> ppr (coercionSize co)) $
+ = pprTrace "optCoercion {" (text "Co:" <> ppr co) $
let result = optCoercion' env co in
pprTrace "optCoercion }"
(vcat [ text "Co:" <+> ppr (coercionSize co)
, text "Optco:" <+> ppWhen (isReflCo result) (text "(refl)")
- <+> ppr (coercionSize result) ]) $
+ <+> ppr result ]) $
result
-}
@@ -317,7 +317,7 @@ opt_co4' env sym rep r (GRefl _r ty (MCo kco))
(text "Expected role:" <+> ppr r $$
text "Found role:" <+> ppr _r $$
text "Type:" <+> ppr ty) $
- if isGReflCo kco || isGReflCo kco'
+ if isReflKindCo kco || isReflKindCo kco'
then wrapSym sym ty_co
else wrapSym sym $ mk_coherence_right_co r' (coercionRKind ty_co) kco' ty_co
-- ty :: k1
@@ -841,55 +841,58 @@ opt_trans_rule is co1 co2@(AppCo co2a co2b)
-- Push transitivity inside forall
-- forall over types.
opt_trans_rule is co1 co2
- | 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 (tv1, visL1, _visR1, kco1, r1) <- splitForAllCo_ty_maybe co1
+ , Just (tv2, _visL2, visR2, kco2, r2) <- etaForAllCo_ty_maybe co2
+ = push_trans tv1 kco1 r1 tv2 kco2 r2 visL1 visR2
- | 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
+ | Just (tv2, _visL2, visR2, kco2, r2) <- splitForAllCo_ty_maybe co2
+ , Just (tv1, visL1, _visR1, kco1, r1) <- etaForAllCo_ty_maybe co1
+ = push_trans tv1 kco1 r1 tv2 kco2 r2 visL1 visR2
where
- push_trans tv1 eta1 r1 tv2 eta2 r2 visL visR
+ push_trans tv1 kco1 r1 tv2 kco2 r2 visL visR
-- Given:
- -- co1 = /\ tv1 : eta1 . r1
- -- co2 = /\ tv2 : eta2 . r2
+ -- co1 = /\ tv1 : kco1 . r1
+ -- co2 = /\ tv2 : kco2 . r2
-- Wanted:
- -- /\tv1 : (eta1;eta2) . (r1; r2[tv2 |-> tv1 |> eta1])
+ -- /\tv1 : (kco1;kco2) . (r1; r2[tv2 |-> tv1 |> kco1])
= fireTransRule "EtaAllTy_ty" co1 co2 $
- mkForAllCo tv1 visL visR (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
+ mkForAllCo tv1 visL visR
+ (kindCoToMKindCo (opt_trans is kco1 kco2))
+ (opt_trans is' r1 r2')
where
is' = is `extendInScopeSet` tv1
- r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
+ r2' = substCoWithInScope is' [tv2] [mkCastTy (TyVarTy tv1) kco1] r2
-- Push transitivity inside forall
-- forall over coercions.
opt_trans_rule is co1 co2
- | 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 (cv1, visL1, _visR1, kco1, r1) <- splitForAllCo_co_maybe co1
+ , Just (cv2, _visL2, visR2, kco2, r2) <- etaForAllCo_co_maybe co2
+ = push_trans cv1 kco1 r1 cv2 kco2 r2 visL1 visR2
- | 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
+ | Just (cv2, _visL2, visR2, kco2, r2) <- splitForAllCo_co_maybe co2
+ , Just (cv1, visL1, _visR1, kco1, r1) <- etaForAllCo_co_maybe co1
+ = push_trans cv1 kco1 r1 cv2 kco2 r2 visL1 visR2
where
- push_trans cv1 eta1 r1 cv2 eta2 r2 visL visR
+ push_trans cv1 kco1 r1 cv2 kco2 r2 visL visR
-- Given:
- -- co1 = /\ (cv1 : eta1) . r1
- -- co2 = /\ (cv2 : eta2) . r2
+ -- co1 = /\ (cv1 : kco1) . r1
+ -- co2 = /\ (cv2 : kco2) . r2
-- Wanted:
- -- n1 = nth 2 eta1
- -- n2 = nth 3 eta1
- -- nco = /\ cv1 : (eta1;eta2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
+ -- n1 = nth 2 kco1
+ -- n2 = nth 3 kco1
+ -- nco = /\ cv1 : (kco1;kco2). (r1; r2[cv2 |-> (sym n1);cv1;n2])
= fireTransRule "EtaAllTy_co" co1 co2 $
- mkForAllCo cv1 visL visR (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
+ mkForAllCo cv1 visL visR (coToMCo (opt_trans is kco1 kco2))
+ (opt_trans is' r1 r2')
where
is' = is `extendInScopeSet` cv1
role = coVarRole cv1
- eta1' = downgradeRole role Nominal eta1
- n1 = mkSelCo (SelTyCon 2 role) eta1'
- n2 = mkSelCo (SelTyCon 3 role) eta1'
+ kco1' = downgradeRole role Nominal kco1
+ n1 = mkSelCo (SelTyCon 2 role) kco1'
+ n2 = mkSelCo (SelTyCon 3 role) kco1'
r2' = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mk_trans_co`
(mkCoVarCo cv1) `mk_trans_co` n2])
r2
@@ -1285,7 +1288,8 @@ Here,
eta2 = mkSelCo (SelTyCon 3 r) h1 :: (s2 ~ s4)
h2 = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
-}
-etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
+etaForAllCo_ty_maybe :: Coercion
+ -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion)
-- Try to make the coercion be of form (forall tv:kind_co. co)
etaForAllCo_ty_maybe co
| Just (tv, visL, visR, kind_co, r) <- splitForAllCo_ty_maybe co
@@ -1305,7 +1309,8 @@ etaForAllCo_ty_maybe co
| otherwise
= Nothing
-etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
+etaForAllCo_co_maybe :: Coercion
+ -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, KindCoercion, Coercion)
-- Try to make the coercion be of form (forall cv:kind_co. co)
etaForAllCo_co_maybe co
| Just (cv, visL, visR, kind_co, r) <- splitForAllCo_co_maybe co
@@ -1428,13 +1433,17 @@ But if sym=Swapped, things are trickier. Here is an identity that helps:
-}
optForAllCoBndr :: LiftingContext -> SwapFlag
- -> TyCoVar -> Coercion
- -> (LiftingContext, TyCoVar, Coercion)
+ -> TyCoVar -> MCoercionN
+ -> (LiftingContext, TyCoVar, MCoercionN)
-- See Note [Optimising ForAllCo]
-optForAllCoBndr env sym tcv kco
- = (env', tcv', kco')
+optForAllCoBndr env sym tcv k_mco
+ = (env', tcv', k_mco')
where
- kco' = opt_co4 env sym False Nominal kco -- Push sym into kco
+ -- Push sym into kco
+ k_mco' = case k_mco of
+ MRefl -> MRefl
+ MCo co -> MCo (opt_co4 env sym False Nominal co)
+
(env', tcv') = updateLCSubst env upd_subst
upd_subst :: Subst -> (Subst, TyCoVar)
@@ -1443,26 +1452,32 @@ optForAllCoBndr env sym tcv kco
| otherwise = upd_subst_cv subst
upd_subst_tv subst
- | notSwapped sym || isReflCo kco' = (subst1, tv1)
- | otherwise = (subst2, tv2)
+ = case k_mco' of
+ MCo k_co' | isSwapped sym -> (subst2, tv2)
+ where
+ -- In the Swapped case, we re-kind the type variable, AND
+ -- override the substitution for the original variable to the
+ -- re-kinded one, suitably casted
+ tv2 = tv1 `setTyVarKind` coercionLKind k_co'
+ subst2 = (extendTvSubst subst1 tcv (mkTyVarTy tv2 `CastTy` k_co'))
+ `extendSubstInScope` tv2
+
+ _ -> (subst1, tv1)
where
-- subst1,tv1: apply the substitution to the binder and its kind
-- NB: varKind tv = coercionLKind kco
(subst1, tv1) = substTyVarBndr subst tcv
- -- In the Swapped case, we re-kind the type variable, AND
- -- override the substitution for the original variable to the
- -- re-kinded one, suitably casted
- tv2 = tv1 `setTyVarKind` coercionLKind kco'
- subst2 = (extendTvSubst subst1 tcv (mkTyVarTy tv2 `CastTy` kco'))
- `extendSubstInScope` tv2
upd_subst_cv subst -- ToDo: probably not right yet
- | notSwapped sym || isReflCo kco' = (subst1, cv1)
- | otherwise = (subst2, cv2)
- where
+ = case k_mco' of
+ MCo k_co' | isSwapped sym -> (subst2, cv2)
+ where
+ cv2 = cv1 `setTyVarKind` coercionLKind k_co'
+ subst2 = subst1 `extendSubstInScope` cv2
+
+ _ -> (subst1, cv1)
+ where
(subst1, cv1) = substCoVarBndr subst tcv
- cv2 = cv1 `setTyVarKind` coercionLKind kco'
- subst2 = subst1 `extendSubstInScope` cv2
{- **********************************************************************
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2424,15 +2424,19 @@ lintCoercion co@(ForAllCo {})
go :: [OutTyCoVar] -- Binders in reverse order
-> InCoercion -> LintM Role
go tcvs co@(ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
- , fco_kind = kind_co, fco_body = body_co })
+ , fco_kind = kind_mco, fco_body = body_co })
| not (isTyCoVar tcv)
= failWithL (text "Non tyco binder in ForAllCo:" <+> ppr co)
| otherwise
- = do { lk <- lintStarCoercion kind_co
+ = do { mb_lk <- case kind_mco of
+ MRefl -> return Nothing
+ MCo kind_co -> Just <$> lintStarCoercion kind_co
; lintTyCoBndr tcv $ \tcv' ->
- do { ensureEqTys (varType tcv') lk $
- text "Kind mis-match in ForallCo" <+> ppr co
+ do { case mb_lk of
+ Nothing -> return ()
+ Just lk -> ensureEqTys (varType tcv') lk $
+ text "Kind mis-match in ForallCo" <+> ppr co
-- I'm not very sure about this part, because it traverses body_co
-- but at least it's on a cold path (a ForallCo for a CoVar)
=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -2367,8 +2367,7 @@ mkEtaForAllMCo (Bndr tcv vis) ty mco
| otherwise -> mk_fco (mkRepReflCo ty)
MCo co -> mk_fco co
where
- mk_fco co = MCo (mkForAllCo tcv vis coreTyLamForAllTyFlag
- (mkNomReflCo (varType tcv)) co)
+ mk_fco co = MCo (mkForAllCo tcv vis coreTyLamForAllTyFlag MRefl co)
-- coreTyLamForAllTyFlag: See Note [The EtaInfo mechanism], particularly
-- the (EtaInfo Invariant). (sym co) wraps a lambda that always has
-- a ForAllTyFlag of coreTyLamForAllTyFlag; see Note [Required foralls in Core]
@@ -2808,11 +2807,10 @@ tryEtaReduce rec_ids bndrs body eval_sd
| Just tv <- getTyVar_maybe arg_ty
, bndr == tv = case splitForAllForAllTyBinder_maybe fun_ty of
Just (Bndr _ vis, _) -> Just (fco, [])
- where !fco = mkForAllCo tv vis coreTyLamForAllTyFlag kco co
+ where !fco = mkForAllCo tv vis coreTyLamForAllTyFlag MRefl co
-- The lambda we are eta-reducing always has visibility
-- 'coreTyLamForAllTyFlag' which may or may not match
-- the visibility on the inner function (#24014)
- kco = mkNomReflCo (tyVarKind tv)
Nothing -> pprPanic "tryEtaReduce: type arg to non-forall type"
(text "fun:" <+> ppr bndr
$$ text "arg:" <+> ppr arg_ty
=====================================
compiler/GHC/Core/Reduction.hs
=====================================
@@ -373,7 +373,7 @@ mkForAllRedn :: ForAllTyFlag
-> Reduction
mkForAllRedn vis tv1 (Reduction h ki') (Reduction co ty)
= mkReduction
- (mkForAllCo tv1 vis vis h co)
+ (mkForAllCo tv1 vis vis (kindCoToMKindCo h) co)
(mkForAllTy (Bndr tv2 vis) ty)
where
tv2 = setTyVarKind tv1 ki'
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -51,7 +51,6 @@ module GHC.Core.TyCo.FVs
import GHC.Prelude
import {-# SOURCE #-} GHC.Core.Type( partitionInvisibleTypes, coreView, rewriterView )
-import {-# SOURCE #-} GHC.Core.Coercion( coercionLKind )
import GHC.Builtin.Types.Prim( funTyFlagTyCon )
@@ -641,8 +640,10 @@ tyCoVarsOfCoList :: Coercion -> [TyCoVar]
tyCoVarsOfCoList co = fvVarList $ tyCoFVsOfCo co
tyCoFVsOfMCo :: MCoercion -> FV
-tyCoFVsOfMCo MRefl = emptyFV
-tyCoFVsOfMCo (MCo co) = tyCoFVsOfCo co
+tyCoFVsOfMCo mco fv_cand in_scope acc
+ = case mco of
+ MRefl -> emptyFV fv_cand in_scope acc
+ MCo co -> tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo :: Coercion -> FV
-- Extracts type and coercion variables from a coercion
@@ -655,7 +656,7 @@ tyCoFVsOfCo (TyConAppCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand
tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
= (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) 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
+ = (tyCoFVsVarBndr tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfMCo 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
tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
@@ -693,6 +694,10 @@ almostDevoidCoVarOfCo :: CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo cv co =
almost_devoid_co_var_of_co co cv
+almost_devoid_co_var_of_mco :: MCoercion -> CoVar -> Bool
+almost_devoid_co_var_of_mco MRefl _ = True
+almost_devoid_co_var_of_mco (MCo co) cv = almost_devoid_co_var_of_co co cv
+
almost_devoid_co_var_of_co :: Coercion -> CoVar -> Bool
almost_devoid_co_var_of_co (Refl {}) _ = True -- covar is allowed in Refl and
almost_devoid_co_var_of_co (GRefl {}) _ = True -- GRefl, so we don't look into
@@ -703,7 +708,7 @@ 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 { fco_tcv = v, fco_kind = kind_co, fco_body = co }) cv
- = almost_devoid_co_var_of_co kind_co cv
+ = almost_devoid_co_var_of_mco 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
= almost_devoid_co_var_of_co w cv
@@ -1032,7 +1037,7 @@ tyConsOfType ty
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 { fco_kind = kind_co, fco_body = co })
- = go_co kind_co `unionUniqSets` go_co co
+ = go_mco 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 (AxiomCo ax args) = go_ax ax `unionUniqSets` go_cos args
@@ -1230,14 +1235,14 @@ occCheckExpand vs_to_avoid ty
go_co cxt (SubCo co) = do { co' <- go_co cxt co
; return (SubCo 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
+ go_co cxt@(as, env) co@(ForAllCo { fco_tcv = tcv, fco_kind = kind_co, fco_body = body_co })
+ = do { ki' <- go cxt (varType tcv)
+ ; let tcv' = setVarType tcv ki'
+ env' = extendVarEnv env tcv tcv'
+ as' = as `delVarSet` tcv
+ ; kind_co' <- go_mco cxt kind_co
; body' <- go_co (as', env') body_co
- ; return (co { fco_tcv = tv', fco_kind = kind_co', fco_body = body' }) }
+ ; return (co { fco_tcv = tcv', 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
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -39,7 +39,7 @@ module GHC.Core.TyCo.Rep (
UnivCoProvenance(..),
CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
CoercionN, CoercionR, CoercionP, KindCoercion,
- MCoercion(..), MCoercionR, MCoercionN,
+ MCoercion(..), MCoercionR, MCoercionN, KindMCoercion,
-- * Functions over types
mkNakedTyConTy, mkTyVarTy, mkTyVarTys,
@@ -806,6 +806,34 @@ tcMkScaledFunTy (Scaled mult arg) res = tcMkVisFunTy mult arg res
%************************************************************************
-}
+type CoercionN = Coercion -- always Nominal
+type CoercionR = Coercion -- always Representational
+type CoercionP = Coercion -- always Phantom
+
+type MCoercionN = MCoercion -- alwyas Nominal
+type MCoercionR = MCoercion -- always Representational
+
+{- Note [KindCoercion]
+~~~~~~~~~~~~~~~~~~~~~~
+A KindCoercion kco :: k1 ~r k2 is a Coercion with these properties:
+ (a) It is Nominal; that is r=Nominal
+ (b) Both (k1::Type) and (k2::Type); it is homogeneous
+
+The coercion in (a) ForAllCo and (b) CastTy is a KindCoercion.
+
+The invariants of KindCoercion allow `isReflKindCo` to elminate GRefl,
+whereas isReflCo cannot. In particular, consider a KindCoercion
+ kco = GRefl r k (MCo kk)) :: k ~ (k |> kk)
+Since `kco`is a KindCoercion, we know that
+ r = Nominal
+ k :: Type and (k |> kk) :: Type
+Hence kk must be Refl. And hence kco = GRefl N k MRefl, which is
+the same as Refl. See `isReflKindCo`.
+-}
+
+type KindCoercion = CoercionN -- See Note [KindCoercion]
+type KindMCoercion = MCoercionN -- See Note [KindCoercion]
+
-- | A 'Coercion' is concrete evidence of the equality/convertibility
-- of two types.
@@ -829,7 +857,7 @@ data Coercion
-- GRefl :: "e" -> _ -> Maybe N -> e
-- See Note [Generalized reflexive coercion]
- | GRefl Role Type MCoercionN -- See Note [Refl invariant]
+ | GRefl Role Type KindMCoercion -- See Note [Refl invariant]
-- Use (Refl ty), not (GRefl Nominal ty MRefl)
-- Use (GRefl Representational _ _), not (SubCo (GRefl Nominal _ _))
@@ -853,7 +881,7 @@ data Coercion
, fco_visL :: !ForAllTyFlag -- Visibility of coercionLKind
, fco_visR :: !ForAllTyFlag -- Visibility of coercionRKind
-- See (FC7) of Note [ForAllCo]
- , fco_kind :: KindCoercion
+ , fco_kind :: KindMCoercion -- See (FC8) of Note [ForAllCo]
, fco_body :: Coercion }
-- ForAllCo :: _ -> N -> e -> e
@@ -911,6 +939,15 @@ data Coercion
-- Only present during typechecking
deriving Data.Data
+-- | A semantically more meaningful type to represent what may or may not be a
+-- useful 'Coercion'.
+data MCoercion
+ = MRefl
+ -- A trivial Reflexivity coercion
+ | MCo Coercion
+ -- Other coercions
+ deriving Data.Data
+
data CoSel -- See Note [SelCo]
= SelTyCon Int Role -- Decomposes (T co1 ... con); zero-indexed
-- Invariant: Given: SelCo (SelTyCon i r) co
@@ -932,11 +969,6 @@ data FunSel -- See Note [SelCo]
| SelRes -- Result of function
deriving( Eq, Data.Data, Ord )
-type CoercionN = Coercion -- always nominal
-type CoercionR = Coercion -- always representational
-type CoercionP = Coercion -- always phantom
-type KindCoercion = CoercionN -- always nominal
-
instance Outputable Coercion where
ppr = pprCo
@@ -980,17 +1012,6 @@ instance NFData CoSel where
rnf SelForAll = ()
rnf (SelFun fs) = rnf fs `seq` ()
--- | A semantically more meaningful type to represent what may or may not be a
--- useful 'Coercion'.
-data MCoercion
- = MRefl
- -- A trivial Reflexivity coercion
- | MCo Coercion
- -- Other coercions
- deriving Data.Data
-type MCoercionR = MCoercion
-type MCoercionN = MCoercion
-
instance Outputable MCoercion where
ppr MRefl = text "MRefl"
ppr (MCo co) = text "MCo" <+> ppr co
@@ -1278,6 +1299,14 @@ Several things to note here
fco_visL = fco_visR = coreTyLamForAllTyFlag
c.f. (FT2) in Note [ForAllTy]
+(FC8) We /represent/ a ForAllCo { fco_tcv = tcv, fco_kind = kmco } as follows:
+ * The tcv::TyCoVar has a kind (like any Var), say tcv::ki
+ * The kind-coercion `kmco` is a KindMCoercion:
+ - If kmco = MRefl, then the coercion in the typing rule is (Refl ki)
+ - If kmco = MCo kco, then the coercion in the typing rule is `co`,
+ /and/ ki = coercionLKind kco
+ So in the common MRefl case, the kind of `tcv` plays a useful role.
+
Note [Predicate coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
@@ -1937,11 +1966,14 @@ 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 _vis1 _vis2 kind_co co)
- = go_co env kind_co `mappend` go_ty env (varType tv)
- `mappend` go_co env' co
+ go_co env (ForAllCo { fco_tcv = tcv, fco_kind = kind_co, fco_body = co })
+ = go_mco env kind_co `mappend` go_ty env (varType tcv)
+ `mappend` go_co env' co
where
- env' = tycobinder env tv Inferred
+ env' = tycobinder env tcv Inferred
+
+ go_mco _ MRefl = mempty
+ go_mco env (MCo co) = go_co env co
-- | A view function that looks through nothing.
noView :: Type -> Maybe Type
@@ -1983,18 +2015,19 @@ typesSize tys = foldr ((+) . typeSize) 0 tys
coercionSize :: Coercion -> Int
coercionSize (Refl ty) = typeSize ty
-coercionSize (GRefl _ ty MRefl) = typeSize ty
-coercionSize (GRefl _ ty (MCo co)) = 1 + typeSize ty + coercionSize co
+coercionSize (GRefl _ ty mco) = typeSize ty + mCoercionSize mco
coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (AppCo co arg) = coercionSize co + coercionSize arg
coercionSize (ForAllCo { fco_kind = h, fco_body = co })
- = 1 + coercionSize co + coercionSize h
+ = 1 + coercionSize co + mCoercionSize h
coercionSize (FunCo _ _ _ w c1 c2) = 1 + coercionSize c1 + coercionSize c2
+ coercionSize w
coercionSize (CoVarCo _) = 1
coercionSize (HoleCo _) = 1
coercionSize (AxiomCo _ cs) = 1 + sum (map coercionSize cs)
-coercionSize (UnivCo { uco_lty = t1, uco_rty = t2 }) = 1 + typeSize t1 + typeSize t2
+coercionSize (UnivCo { uco_lty = t1, uco_rty = t2, uco_deps = deps })
+ = 1 + typeSize t1 + typeSize t2
+ + sum (map coercionSize deps)
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
coercionSize (SelCo _ co) = 1 + coercionSize co
@@ -2003,6 +2036,10 @@ coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg
coercionSize (KindCo co) = 1 + coercionSize co
coercionSize (SubCo co) = 1 + coercionSize co
+mCoercionSize :: MCoercion -> Int
+mCoercionSize MRefl = 0
+mCoercionSize (MCo co) = coercionSize co
+
{-
************************************************************************
* *
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -29,11 +29,10 @@ module GHC.Core.TyCo.Subst
mkTvSubstPrs,
substTyWith, substTyWithCoVars, substTysWith, substTysWithCoVars,
- substCoWith,
+ substCoWithInScope,
substTy, substTyAddInScope, substScaledTy,
substTyUnchecked, substTysUnchecked, substScaledTysUnchecked, substThetaUnchecked,
substTyWithUnchecked, substScaledTyUnchecked,
- substCoUnchecked, substCoWithUnchecked,
substTyWithInScope,
substTys, substScaledTys, substTheta,
lookupTyVar,
@@ -44,8 +43,8 @@ module GHC.Core.TyCo.Subst
substCoVarBndr, substDCoVarSet,
substTyVar, substTyVars, substTyVarToTyVar,
substTyCoVars,
- substTyCoBndr, substForAllCoBndr,
- substVarBndrUsing, substForAllCoBndrUsing,
+ substTyCoBndr,
+ substVarBndrUsing,
checkValidSubst, isValidTCvSubst,
) where
@@ -60,7 +59,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
, mkAxiomCo, mkAppCo, mkGReflCo
, mkInstCo, mkLRCo, mkTyConAppCo
, mkCoercionType
- , coercionLKind, coVarTypesRole )
+ , coVarTypesRole )
import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprTyVar )
import {-# SOURCE #-} GHC.Core.Ppr ( ) -- instance Outputable CoreExpr
import {-# SOURCE #-} GHC.Core ( CoreExpr )
@@ -618,28 +617,19 @@ substTyWithUnchecked tvs tys
-- Pre-condition: the 'in_scope' set should satisfy Note [The substitution
-- invariant]; specifically it should include the free vars of 'tys',
-- and of 'ty' minus the domain of the subst.
-substTyWithInScope :: HasDebugCallStack => InScopeSet -> [TyVar] -> [Type] -> Type -> Type
+substTyWithInScope :: HasDebugCallStack
+ => InScopeSet -> [TyVar] -> [Type] -> Type -> Type
substTyWithInScope in_scope tvs tys ty =
assert (tvs `equalLength` tys )
substTy (mkTvSubst in_scope tenv) ty
where tenv = zipTyEnv tvs tys
-- | Coercion substitution, see 'zipTvSubst'
-substCoWith :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
-substCoWith tvs tys = assert (tvs `equalLength` tys )
- substCo (zipTvSubst tvs tys)
-
--- | Coercion substitution, see 'zipTvSubst'. Disables sanity checks.
--- The problems that the sanity checks in substCo catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substCoUnchecked to
--- substCo and remove this function. Please don't use in new code.
-substCoWithUnchecked :: [TyVar] -> [Type] -> Coercion -> Coercion
-substCoWithUnchecked tvs tys
+substCoWithInScope :: HasDebugCallStack
+ => InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
+substCoWithInScope in_scope tvs tys co
= assert (tvs `equalLength` tys )
- substCoUnchecked (zipTvSubst tvs tys)
-
-
+ substCo (mkTvSubst in_scope (zipTyEnv tvs tys)) co
-- | Substitute covars within a type
substTyWithCoVars :: [CoVar] -> [Coercion] -> Type -> Type
@@ -800,10 +790,10 @@ subst_ty subst ty
!res' = go res
in ty { ft_mult = mult', ft_arg = arg', ft_res = res' }
go (ForAllTy (Bndr tv vis) ty)
- = case substVarBndrUnchecked subst tv of
- (subst', tv') ->
- (ForAllTy $! ((Bndr $! tv') vis)) $!
- (subst_ty subst' ty)
+ = (ForAllTy $! ((Bndr $! tv') vis)) $! (subst_ty subst' ty)
+ where
+ !(subst',tv') = substVarBndrUnchecked subst tv
+ -- Unchecked because subst_ty is used from substTyUnchecked
go (LitTy n) = LitTy $! n
go (CastTy ty co) = (mkCastTy $! (go ty)) $! (subst_co subst co)
go (CoercionTy co) = CoercionTy $! (subst_co subst co)
@@ -850,16 +840,6 @@ substCo subst co
| isEmptyTCvSubst subst = co
| otherwise = checkValidSubst subst [] [co] $ subst_co subst co
--- | Substitute within a 'Coercion' disabling sanity checks.
--- The problems that the sanity checks in substCo catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substCoUnchecked to
--- substCo and remove this function. Please don't use in new code.
-substCoUnchecked :: Subst -> Coercion -> Coercion
-substCoUnchecked subst co
- | isEmptyTCvSubst subst = co
- | otherwise = subst_co subst co
-
-- | Substitute within several 'Coercion's
-- The substitution has to satisfy the invariants described in
-- Note [The substitution invariant].
@@ -868,7 +848,7 @@ substCos subst cos
| isEmptyTCvSubst subst = cos
| otherwise = checkValidSubst subst [] cos $ map (subst_co subst) cos
-subst_co :: Subst -> Coercion -> Coercion
+subst_co :: HasDebugCallStack => Subst -> Coercion -> Coercion
subst_co subst co
= go co
where
@@ -885,10 +865,14 @@ subst_co subst co
go (TyConAppCo r tc args)= mkTyConAppCo r tc $! go_cos args
go (AxiomCo con cos) = mkAxiomCo con $! go_cos cos
go (AppCo co arg) = (mkAppCo $! go co) $! go arg
- go (ForAllCo tv visL visR kind_co co)
- = case substForAllCoBndrUnchecked subst tv kind_co of
- (subst', tv', kind_co') ->
- ((mkForAllCo $! tv') visL visR $! kind_co') $! subst_co subst' co
+ go (ForAllCo { fco_tcv = tcv, fco_visL = visL, fco_visR = visR
+ , fco_kind = kind_co, fco_body = co })
+ = ((mkForAllCo $! tcv') visL visR
+ $! go_mco kind_co)
+ $! subst_co subst' co
+ where
+ !(subst', tcv') = substVarBndrUnchecked subst tcv
+ -- Unchecked because used from substTyUnchecked
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 (UnivCo { uco_prov = p, uco_role = r
@@ -917,75 +901,6 @@ substDCoVarSet :: Subst -> DCoVarSet -> DCoVarSet
substDCoVarSet subst cvs = coVarsOfCosDSet $ map (substCoVar subst) $
dVarSetElems cvs
-substForAllCoBndr :: Subst -> TyCoVar -> KindCoercion
- -> (Subst, TyCoVar, Coercion)
-substForAllCoBndr subst
- = substForAllCoBndrUsing (substCo subst) subst
-
--- | Like 'substForAllCoBndr', but disables sanity checks.
--- The problems that the sanity checks in substCo catch are described in
--- Note [The substitution invariant].
--- The goal of #11371 is to migrate all the calls of substCoUnchecked to
--- substCo and remove this function. Please don't use in new code.
-substForAllCoBndrUnchecked :: Subst -> TyCoVar -> KindCoercion
- -> (Subst, TyCoVar, Coercion)
-substForAllCoBndrUnchecked subst
- = substForAllCoBndrUsing (substCoUnchecked subst) subst
-
--- See Note [Sym and ForAllCo]
-substForAllCoBndrUsing :: (Coercion -> Coercion) -- transformation to kind co
- -> Subst -> TyCoVar -> KindCoercion
- -> (Subst, TyCoVar, KindCoercion)
-substForAllCoBndrUsing sco subst old_var
- | isTyVar old_var = substForAllCoTyVarBndrUsing sco subst old_var
- | otherwise = substForAllCoCoVarBndrUsing sco subst old_var
-
-substForAllCoTyVarBndrUsing :: (Coercion -> Coercion) -- transformation to kind co
- -> Subst -> TyVar -> KindCoercion
- -> (Subst, TyVar, KindCoercion)
-substForAllCoTyVarBndrUsing sco (Subst in_scope idenv tenv cenv) old_var old_kind_co
- = assert (isTyVar old_var )
- ( Subst (in_scope `extendInScopeSet` new_var) idenv new_env cenv
- , new_var, new_kind_co )
- where
- new_env | no_change = delVarEnv tenv old_var
- | otherwise = extendVarEnv tenv old_var (TyVarTy new_var)
-
- no_kind_change = noFreeVarsOfCo old_kind_co
- no_change = no_kind_change && (new_var == old_var)
-
- new_kind_co | no_kind_change = old_kind_co
- | otherwise = sco old_kind_co
-
- new_ki1 = coercionLKind new_kind_co
- -- We could do substitution to (tyVarKind old_var). We don't do so because
- -- we already substituted new_kind_co, which contains the kind information
- -- we want. We don't want to do substitution once more. Also, in most cases,
- -- new_kind_co is a Refl, in which case coercionKind is really fast.
-
- new_var = uniqAway in_scope (setTyVarKind old_var new_ki1)
-
-substForAllCoCoVarBndrUsing :: (Coercion -> Coercion) -- transformation to kind co
- -> Subst -> CoVar -> KindCoercion
- -> (Subst, CoVar, KindCoercion)
-substForAllCoCoVarBndrUsing sco (Subst in_scope idenv tenv cenv)
- old_var old_kind_co
- = assert (isCoVar old_var )
- ( Subst (in_scope `extendInScopeSet` new_var) idenv tenv new_cenv
- , new_var, new_kind_co )
- where
- new_cenv | no_change = delVarEnv cenv old_var
- | otherwise = extendVarEnv cenv old_var (mkCoVarCo new_var)
-
- no_kind_change = noFreeVarsOfCo old_kind_co
- no_change = no_kind_change && (new_var == old_var)
-
- new_kind_co | no_kind_change = old_kind_co
- | otherwise = sco old_kind_co
-
- new_ki1 = coercionLKind new_kind_co
- new_var = uniqAway in_scope $ mkCoVar (varName old_var) new_ki1
-
substCoVar :: Subst -> CoVar -> Coercion
substCoVar (Subst _ _ _ cenv) cv
= case lookupVarEnv cenv cv of
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -334,7 +334,7 @@ tidyCo env co
go (TyConAppCo r tc cos) = TyConAppCo r tc $! strictMap go cos
go (AppCo co1 co2) = (AppCo $! go co1) $! go co2
go (ForAllCo tv visL visR h co)
- = ((((ForAllCo $! tvp) $! visL) $! visR) $! (go h)) $! (tidyCo envp co)
+ = ((((ForAllCo $! tvp) $! visL) $! visR) $! (go_mco 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.
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -210,7 +210,7 @@ module GHC.Core.Type (
substTyAddInScope,
substTyUnchecked, substTysUnchecked, substScaledTyUnchecked, substScaledTysUnchecked,
substThetaUnchecked, substTyWithUnchecked,
- substCo, substCoUnchecked, substCoWithUnchecked,
+ substCo, substCoWithInScope,
substTyVarBndr, substTyVarBndrs, substTyVar, substTyVars,
substVarBndr, substVarBndrs,
substTyCoBndr, substTyVarToTyVar,
@@ -530,10 +530,13 @@ 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 { fco_tcv = tv, fco_visL = visL, fco_visR = visR
+ go_co subst (ForAllCo { fco_tcv = tcv, 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' visL visR kind_co' (go_co subst' co)
+ = mkForAllCo tcv' visL visR
+ (go_mco subst kind_co)
+ (go_co subst' co)
+ where
+ (subst', tcv') = substVarBndr subst tcv
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)
@@ -559,8 +562,6 @@ expandTypeSynonyms ty
go_co _ (HoleCo h)
= pprPanic "expandTypeSynonyms hit a hole" (ppr h)
- go_cobndr subst = substForAllCoBndrUsing (go_co subst) subst
-
{- Notes on type synonyms
~~~~~~~~~~~~~~~~~~~~~~~~~
The various "split" functions (splitFunTy, splitRhoTy, splitForAllTy) try
@@ -971,7 +972,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
= mkTyConAppCo r tc <$> go_cos env cos
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
+ = do { kind_co' <- go_mco env kind_co
; tycobinder env tv visL $ \env' tv' -> do
; co' <- go_co env' co
; return $ mkForAllCo tv' visL visR kind_co' co' }
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -2414,14 +2414,15 @@ ty_co_match menv subst (FunTy { ft_mult = w, ft_arg = ty1, ft_res = ty2 })
-- not doing so caused #21205.
ty_co_match menv subst (ForAllTy (Bndr tv1 vis1t) ty1)
- (ForAllCo tv2 vis1c vis2c kind_co2 co2)
+ (ForAllCo tv2 vis1c vis2c kind_mco2 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
+ = do { subst1 <- ty_co_match menv subst (tyVarKind tv1)
+ (forAllCoKindCo tv2 kind_mco2)
ki_ki_co ki_ki_co
; let rn_env0 = me_env menv
rn_env1 = rnBndr2 rn_env0 tv1 tv2
@@ -2522,6 +2523,6 @@ pushRefl co =
-> Just (TyConAppCo r tc (zipWith mkReflCo (tyConRoleListX r tc) tys))
Just (ForAllTy (Bndr tv vis) ty, r)
-> Just (ForAllCo { fco_tcv = tv, fco_visL = vis, fco_visR = vis
- , fco_kind = mkNomReflCo (varType tv)
+ , fco_kind = MRefl
, fco_body = mkReflCo r ty })
_ -> Nothing
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -312,7 +312,7 @@ toIfaceCoercionX fr co
= IfaceForAllCo (toIfaceBndr tv)
visL
visR
- (toIfaceCoercionX fr' k)
+ (go_mco k)
(toIfaceCoercionX fr' co)
where
fr' = fr `delVarSet` tv
=====================================
compiler/GHC/Iface/Rename.hs
=====================================
@@ -689,7 +689,7 @@ rnIfaceCo (IfaceAxiomCo ax cos) = IfaceAxiomCo ax <$> mapM rnIfaceCo cos
rnIfaceCo (IfaceKindCo c) = IfaceKindCo <$> rnIfaceCo c
rnIfaceCo (IfaceForAllCo bndr visL visR co1 co2)
= (\bndr' co1' co2' -> IfaceForAllCo bndr' visL visR co1' co2')
- <$> rnIfaceBndr bndr <*> rnIfaceCo co1 <*> rnIfaceCo co2
+ <$> rnIfaceBndr bndr <*> rnIfaceMCo co1 <*> rnIfaceCo co2
rnIfaceCo (IfaceUnivCo s r t1 t2 deps)
= IfaceUnivCo s r <$> rnIfaceType t1 <*> rnIfaceType t2 <*> mapM rnIfaceCo deps
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -2076,7 +2076,7 @@ freeNamesIfCoercion (IfaceTyConAppCo _ tc cos)
freeNamesIfCoercion (IfaceAppCo c1 c2)
= freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
freeNamesIfCoercion (IfaceForAllCo _tcv _visL _visR kind_co co)
- = freeNamesIfCoercion kind_co &&& freeNamesIfCoercion co
+ = freeNamesIfMCoercion kind_co &&& freeNamesIfCoercion co
freeNamesIfCoercion (IfaceFreeCoVar _) = emptyNameSet
freeNamesIfCoercion (IfaceCoVarCo _) = emptyNameSet
freeNamesIfCoercion (IfaceHoleCo _) = emptyNameSet
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -132,7 +132,7 @@ data IfaceBndr -- Local (non-top-level) binders
deriving (Eq, Ord)
-type IfaceIdBndr = (IfaceType, IfLclName, IfaceType)
+type IfaceIdBndr = (IfaceType, IfLclName, IfaceType) -- (multiplicity, name, type)
type IfaceTvBndr = (IfLclName, IfaceKind)
ifaceTvBndrName :: IfaceTvBndr -> IfLclName
@@ -479,7 +479,7 @@ data IfaceCoercion
| IfaceFunCo Role IfaceCoercion IfaceCoercion IfaceCoercion
| IfaceTyConAppCo Role IfaceTyCon [IfaceCoercion]
| IfaceAppCo IfaceCoercion IfaceCoercion
- | IfaceForAllCo IfaceBndr !ForAllTyFlag !ForAllTyFlag IfaceCoercion IfaceCoercion
+ | IfaceForAllCo IfaceBndr !ForAllTyFlag !ForAllTyFlag IfaceMCoercion IfaceCoercion
| IfaceCoVarCo IfLclName
| IfaceAxiomCo IfaceAxiomRule [IfaceCoercion]
-- ^ There are only a fixed number of CoAxiomRules, so it suffices
@@ -1454,10 +1454,9 @@ pprIfaceForAllPartMust :: [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
pprIfaceForAllPartMust tvs ctxt sdoc
= ppr_iface_forall_part ShowForAllMust tvs ctxt sdoc
-pprIfaceForAllCoPart :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)]
+pprIfaceForAllCoPart :: [(IfaceBndr, IfaceMCoercion, ForAllTyFlag, ForAllTyFlag)]
-> SDoc -> SDoc
-pprIfaceForAllCoPart tvs sdoc
- = sep [ pprIfaceForAllCo tvs, sdoc ]
+pprIfaceForAllCoPart tvs sdoc = sep [ pprIfaceForAllCo tvs, sdoc ]
ppr_iface_forall_part :: ShowForAllFlag
-> [IfaceForAllBndr] -> [IfacePredType] -> SDoc -> SDoc
@@ -1494,11 +1493,11 @@ ppr_itv_bndrs all_bndrs@(bndr@(Bndr _ vis) : bndrs) vis1
| otherwise = (all_bndrs, [])
ppr_itv_bndrs [] _ = ([], [])
-pprIfaceForAllCo :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc
+pprIfaceForAllCo :: [(IfaceBndr, IfaceMCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc
pprIfaceForAllCo [] = empty
pprIfaceForAllCo tvs = text "forall" <+> pprIfaceForAllCoBndrs tvs <> dot
-pprIfaceForAllCoBndrs :: [(IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc
+pprIfaceForAllCoBndrs :: [(IfaceBndr, IfaceMCoercion, ForAllTyFlag, ForAllTyFlag)] -> SDoc
pprIfaceForAllCoBndrs bndrs = hsep $ map pprIfaceForAllCoBndr bndrs
pprIfaceForAllBndr :: IfaceForAllBndr -> SDoc
@@ -1513,10 +1512,17 @@ pprIfaceForAllBndr bndr =
-- See Note [Suppressing binder signatures]
suppress_sig = SuppressBndrSig False
-pprIfaceForAllCoBndr :: (IfLclName, IfaceCoercion, ForAllTyFlag, ForAllTyFlag) -> SDoc
-pprIfaceForAllCoBndr (tv, kind_co, visL, visR)
- = parens (ppr tv <> pp_vis <+> dcolon <+> pprIfaceCoercion kind_co)
+pprIfaceForAllCoBndr :: (IfaceBndr, IfaceMCoercion, ForAllTyFlag, ForAllTyFlag) -> SDoc
+pprIfaceForAllCoBndr (tcv, kind_mco, visL, visR)
+ = parens (ppr (ifaceBndrName tcv) <> pp_vis
+ <+> text "::~" <+> pprIfaceCoercion kind_co)
+ -- We print (tcv ::~ kind_co), with the "::~" reminding us the type of tcv
+ -- isn't kind_co; rather it's (coercionLKind kind_co). We used "::" previously
+ -- which grievously confused me.
where
+ kind_co = case kind_mco of
+ IfaceMRefl -> IfaceReflCo (ifaceBndrType tcv)
+ IfaceMCo co -> co
pp_vis | visL == coreTyLamForAllTyFlag
, visR == coreTyLamForAllTyFlag
= empty
@@ -2069,10 +2075,8 @@ ppr_co ctxt_prec co@(IfaceForAllCo {})
where
(tvs, inner_co) = split_co 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 (IfaceForAllCo bndr visL visR kind_co co')
+ = let (tvs, co'') = split_co co' in ((bndr,kind_co,visL,visR):tvs,co'')
split_co co' = ([], co')
-- Why these three? See Note [Free TyVars and CoVars in IfaceType]
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1576,9 +1576,12 @@ 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 visL visR k c) = do { k' <- go k
- ; bindIfaceBndr tv $ \ tv' ->
- ForAllCo tv' visL visR k' <$> go c }
+ go (IfaceForAllCo tcv visL visR k co)
+ = do { k' <- go_mco k
+ ; bindIfaceBndr tcv $ \ tv' ->
+ do { co' <- go co
+ ; return (ForAllCo { fco_tcv = tv', fco_visL = visL, fco_visR = visR
+ , fco_kind = k', fco_body = co' }) } }
go (IfaceCoVarCo n) = CoVarCo <$> go_var n
go (IfaceUnivCo p r t1 t2 ds) = do { t1' <- tcIfaceType t1; t2' <- tcIfaceType t2
; ds' <- mapM go ds
=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -135,7 +135,7 @@ synonymTyConsOfType ty
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 { fco_kind = kind_co, fco_body = body_co })
- = go_co kind_co `plusNameEnv` go_co body_co
+ = go_mco 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
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1586,7 +1586,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 { fco_tcv = tcv, fco_kind = kind_co, fco_body = co })
- = do { dv1 <- go_co dv kind_co
+ = do { dv1 <- go_mco dv kind_co
; collect_cand_qtvs_co orig_ty cur_lvl (bound `extendVarSet` tcv) dv1 co }
go_mco dv MRefl = return dv
=====================================
compiler/GHC/Tc/Utils/TcType.hs
=====================================
@@ -176,7 +176,6 @@ module GHC.Tc.Utils.TcType (
substTyUnchecked, substTysUnchecked, substScaledTyUnchecked,
substThetaUnchecked,
substTyWithUnchecked,
- substCoUnchecked, substCoWithUnchecked,
substTheta,
isUnliftedType,
=====================================
compiler/GHC/Types/Id/Make.hs
=====================================
@@ -1206,10 +1206,11 @@ wrapCo co rep_ty (unbox_rep, box_rep) -- co :: arg_ty ~ rep_ty
boxer = Boxer $ \ subst ->
do { (rep_ids, rep_expr)
<- case box_rep of
- UnitBox -> do { rep_id <- newLocal (fsLit "cowrap_bx") (linear $ TcType.substTy subst rep_ty)
+ UnitBox -> do { rep_id <- newLocal (fsLit "cowrap_bx")
+ (linear $ TcType.substTy subst rep_ty)
; return ([rep_id], Var rep_id) }
Boxer boxer -> boxer subst
- ; let sco = substCoUnchecked subst co
+ ; let sco = substCo subst co
; return (rep_ids, rep_expr `Cast` mkSymCo sco) }
------------------------
=====================================
testsuite/tests/simplCore/should_compile/OpaqueNoCastWW.stderr
=====================================
@@ -1,24 +1,24 @@
==================== Tidy Core ====================
Result size of Tidy Core
- = {terms: 82, types: 52, coercions: 29, joins: 0/0}
+ = {terms: 82, types: 52, coercions: 26, joins: 0/0}
-- RHS size: {terms: 3, types: 3, coercions: 0, joins: 0/0}
unsafeToInteger1 :: forall (n :: Nat). Signed n -> Signed n
[GblId, Arity=1, Unf=OtherCon []]
unsafeToInteger1 = \ (@(n :: Nat)) (ds :: Signed n) -> ds
--- RHS size: {terms: 1, types: 0, coercions: 8, joins: 0/0}
+-- RHS size: {terms: 1, types: 0, coercions: 7, joins: 0/0}
unsafeToInteger :: forall (n :: Nat). Signed n -> Integer
[GblId[[RecSel]], Arity=1, Unf=OtherCon []]
unsafeToInteger
= unsafeToInteger1
- `cast` (forall (n :: <Nat>_N).
+ `cast` (forall (n ::~ <Nat>_N).
<Signed n>_R %<Many>_N ->_R OpaqueNoCastWW.N:Signed <n>_P
:: (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}
+-- RHS size: {terms: 8, types: 7, coercions: 19, joins: 0/0}
times [InlPrag=OPAQUE]
:: forall (m :: Nat) (n :: Nat).
Signed m -> Signed n -> Signed (m + n)
@@ -33,7 +33,7 @@ times
(ds `cast` (OpaqueNoCastWW.N:Signed <m>_P :: Signed m ~R# Integer))
(ds1
`cast` (OpaqueNoCastWW.N:Signed <n>_P :: Signed n ~R# Integer)))
- `cast` (forall (m :: <Nat>_N) (n :: <Nat>_N).
+ `cast` (forall (m ::~ <Nat>_N) (n ::~ <Nat>_N).
<Signed m>_R
%<Many>_N ->_R <Signed n>_R
%<Many>_N ->_R Sym (OpaqueNoCastWW.N:Signed _P)
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2897da11f158099cb3c6e9834e7fe0c5...
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/2897da11f158099cb3c6e9834e7fe0c5...
You're receiving this email because of your account on gitlab.haskell.org.
