[Git][ghc/ghc][wip/T21623] Move from NthCo to SelCo
Simon Peyton Jones (@simonpj)
gitlab at gitlab.haskell.org
Tue Aug 16 01:25:50 UTC 2022
Simon Peyton Jones pushed to branch wip/T21623 at Glasgow Haskell Compiler / GHC
Commits:
ac9c8ca6 by Simon Peyton Jones at 2022-08-16T02:25:54+01:00
Move from NthCo to SelCo
- - - - -
29 changed files:
- compiler/GHC/Builtin/Types.hs
- compiler/GHC/Builtin/Types/Prim.hs
- compiler/GHC/Core/Coercion.hs
- compiler/GHC/Core/Coercion.hs-boot
- compiler/GHC/Core/Coercion/Opt.hs
- compiler/GHC/Core/FVs.hs
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Opt/Arity.hs
- compiler/GHC/Core/Opt/Simplify/Iteration.hs
- compiler/GHC/Core/TyCo/FVs.hs
- compiler/GHC/Core/TyCo/Rep.hs
- compiler/GHC/Core/TyCo/Rep.hs-boot
- 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/Module.hs
- compiler/GHC/Tc/Solver/Canonical.hs
- compiler/GHC/Tc/TyCl/Utils.hs
- compiler/GHC/Tc/Types/Evidence.hs
- compiler/GHC/Tc/Utils/TcMType.hs
- compiler/GHC/Types/Basic.hs
- compiler/GHC/Types/Literal.hs
- libraries/ghc-prim/GHC/Types.hs
Changes:
=====================================
compiler/GHC/Builtin/Types.hs
=====================================
@@ -1478,7 +1478,7 @@ unrestrictedFunTyConName = mkWiredInTyConName BuiltInSyntax gHC_TYPES (fsLit "->
********************************************************************* -}
-- For these synonyms, see
--- Note [SORT, TYPE, and CONSTRAINT] in GHC.Builtin.Types.Prim, and
+-- Note [TYPE and CONSTRAINT] in GHC.Builtin.Types.Prim, and
-- Note [Using synonyms to compress types] in GHC.Core.Type
{- Note [Naked FunTy]
=====================================
compiler/GHC/Builtin/Types/Prim.hs
=====================================
@@ -656,33 +656,28 @@ tcArrowTyCon = mkPrimTyCon tcArrowTyConName tc_bndrs constraintKind tc_roles
* *
************************************************************************
-Note [SORT, TYPE, and CONSTRAINT]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-All types that classify values have a kind of the form (SORT t_or_c rr), where
+Note [TYPE and CONSTRAINT]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+GHC distinguishes Type from Constraint throughout the compiler.
+See GHC Proposal #518, and tickets #21623 and #11715.
- -- Primitive
- type SORT :: TypeOrConstraint -> RuntimeRep -> Type
+All types that classify values have a kind of the form
+ (TYPE rr) or (CONSTRAINT rr)
+where the `RuntimeRep` parameter, rr, tells us how the value is represented
+at runtime. TYPE and CONSTRAINT are primitive type constructors.
-* The `TypeOrConstraint` tells whether this value is
- a regular type or a constraint; see Note [Type vs Constraint]
+There are a bunch of type synonyms and data types defined in in the
+library ghc-prim:GHC.Types. All of them are also wired in to GHC, in
+GHC.Builtin.Types
-* The `RuntimeRep` parameter tells us how the value is represented at runtime.
-
-There are a bunch of type synonyms and data types defined in
-in the library ghc-prim:GHC.Types. All of them are also wired in to GHC,
-in GHC.Builtin.Types
-
- type CONSTRAINT = SORT ConstraintLike :: RuntimeRep -> Type
type Constraint = CONSTRAINT LiftedRep :: Type
- type TYPE = SORT TypeLike :: RuntimeRep -> Type
type Type = TYPE LiftedRep :: Type
type UnliftedType = TYPE UnliftedRep :: Type
type LiftedRep = BoxedRep Lifted :: RuntimeRep
type UnliftedRep = BoxedRep Unlifted :: RuntimeRep
-
data RuntimeRep -- Defined in ghc-prim:GHC.Types
= BoxedRep Levity
| IntRep
@@ -691,7 +686,8 @@ in GHC.Builtin.Types
data Levity = Lifted | Unlifted
- data TypeOrConstraint = TypeLike | ConstraintLike
+We abbreviate '*' specially:
+ type * = Type
So for example:
Int :: TYPE (BoxedRep Lifted)
@@ -701,15 +697,12 @@ So for example:
Maybe :: TYPE (BoxedRep Lifted) -> TYPE (BoxedRep Lifted)
(# , #) :: TYPE r1 -> TYPE r2 -> TYPE (TupleRep [r1, r2])
-We abbreviate '*' specially:
- type * = Type
-
-Note [Type vs Constraint]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-GHC distinguishes Type from Constraint, via the TypeOrConstraint
-parameter of SORT. See GHC Proposal #518, and tickets #21623 and #11715.
+ Eq Int :: CONSTRAINT (BoxedRep Lifted)
+ IP "foo" Int :: CONSTRAINT (BoxedRep Lifted)
+ a ~ b :: CONSTRAINT (BoxedRep Lifted)
+ a ~# b :: CONSTRAINT (TupleRep [])
-There are a number of wrinkles
+Note that:
* Type and Constraint are considered distinct throughout GHC. But they
are not /apart/: see Note [Type and Constraint are not apart]
@@ -717,13 +710,6 @@ There are a number of wrinkles
* Constraints are mostly lifted, but unlifted ones are useful too.
Specifically (a ~# b) :: CONSTRAINT (TupleRep [])
-Examples:
-
- Eq Int :: CONSTRAINT (BoxedRep Lifted)
- IP "foo" Int :: CONSTRAINT (BoxedRep Lifted)
- a ~ b :: CONSTRAINT (BoxedRep Lifted)
- a ~# b :: CONSTRAINT (TupleRep [])
-
Note [Type and Constraint are not apart]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Type and Constraint are not equal (eqType) but they are not /apart/
@@ -733,17 +719,17 @@ either. Reason (c.f. #7451):
class C a where { op :: a -> a }
* The axiom for such a class will look like
- axiom axC a :: C a ~# (a->a)
+ axiom axC a :: (C a :: Constraint) ~# (a->a :: Type)
* This axion connects a type of kind Type with one of kind Constraint
That is dangerous: kindCo (axC Int) :: Type ~ Constraint
In general, having a "contradictory proof" like (Int ~ Bool) would be very
- bad; but it's fine provide they are not Apart.
+ bad; but it's fine provided they are not Apart.
So we ensure that Type and Constraint are not apart; or, more
precisely, that TYPE and CONSTRAINT are not apart. This
-non-apart-ness check is implemented in GHC.Core.Unify.unify_ty: look for
-`maybeApart MARTypeVsConstraint`.
+non-apart-ness check is implemented in GHC.Core.Unify.unify_ty: look
+for `maybeApart MARTypeVsConstraint`.
Note that, as before, nothing prevents writing instances like:
@@ -799,7 +785,6 @@ tYPEKind :: Type
tYPEKind = mkTyConTy tYPETyCon
----------------------
--- type CONSTRAINT = SORT ConstraintLike
cONSTRAINTTyCon :: TyCon
cONSTRAINTTyCon = mkPrimTyCon cONSTRAINTTyConName
(mkTemplateAnonTyConBinders [runtimeRepTy])
=====================================
compiler/GHC/Core/Coercion.hs
=====================================
@@ -12,7 +12,9 @@
--
module GHC.Core.Coercion (
-- * Main data type
- Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionN, MCoercionR,
+ Coercion, CoercionN, CoercionR, CoercionP,
+ MCoercion(..), MCoercionN, MCoercionR,
+ CoSel(..), FunSel(..),
UnivCoProvenance, CoercionHole(..),
coHoleCoVar, setCoHoleCoVar,
LeftOrRight(..),
@@ -34,7 +36,7 @@ module GHC.Core.Coercion (
mkAxInstLHS, mkUnbranchedAxInstLHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo,
- mkNthCo, getNthFun, getNthFromType, nthCoRole, mkLRCo,
+ mkSelCo, getNthFun, getNthFromType, nthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunResCo,
mkForAllCo, mkForAllCos, mkHomoForAllCos,
mkPhantomCo,
@@ -62,8 +64,8 @@ module GHC.Core.Coercion (
splitForAllCo_maybe,
splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
- nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
- nthFunRole, funRolesX,
+ tyConRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
+ funRole,
pickLR,
isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
@@ -418,7 +420,7 @@ decomposeCo :: Arity -> Coercion
-- entries as the Arity provided
-> [Coercion]
decomposeCo arity co rs
- = [mkNthCo r n co | (n,r) <- [0..(arity-1)] `zip` rs ]
+ = [mkSelCo r (SelTyCon n) co | (n,r) <- [0..(arity-1)] `zip` rs ]
-- Remember, Nth is zero-indexed
decomposeFunCo :: HasDebugCallStack
@@ -430,11 +432,13 @@ decomposeFunCo :: HasDebugCallStack
-- See Note [Function coercions] for the "3" and "4"
decomposeFunCo _ (FunCo _ w co1 co2) = (w, co1, co2)
- -- Short-circuits the calls to mkNthCo
+ -- Short-circuits the calls to mkSelCo
decomposeFunCo r co
= assertPpr all_ok (ppr co) $
- (mkNthCo Nominal 0 co, mkNthCo r 1 co, mkNthCo r 2 co)
+ ( mkSelCo Nominal (SelFun SelMult) co
+ , mkSelCo r (SelFun SelArg) co
+ , mkSelCo r (SelFun SelRes) co )
where
Pair s1t1 s2t2 = coercionKind co
all_ok = isFunTy s1t1 && isFunTy s2t2
@@ -495,7 +499,7 @@ decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
-- ty :: s2
-- need arg_co :: s2 ~ s1
-- res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
- = let arg_co = mkNthCo Nominal 0 (mkSymCo co)
+ = let arg_co = mkSelCo Nominal SelForAll (mkSymCo co)
res_co = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
subst2' = extendTCvSubst subst2 b ty
@@ -547,7 +551,7 @@ splitAppCo_maybe (TyConAppCo r tc args)
| not (mustBeSaturated tc)
-- Never create unsaturated type family apps!
, Just (args', arg') <- snocView args
- , Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
+ , Just arg'' <- setNominalRole_maybe (tyConRole r tc (length args')) arg'
= Just ( mkTyConAppCo r tc args', arg'' )
-- Use mkTyConAppCo to preserve the invariant
-- that identity coercions are always represented by Refl
@@ -625,7 +629,7 @@ eqTyConRole tc
-- produce a coercion @rep_co :: r1 ~ r2 at .
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo co
- = mkNthCo Nominal 0 kind_co
+ = mkSelCo Nominal (SelTyCon 0) kind_co
where
kind_co = mkKindCo co -- kind_co :: TYPE r1 ~ TYPE r2
@@ -1066,50 +1070,52 @@ mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
= GRefl r t1 (MCo $ mkTransCo co1 co2)
mkTransCo co1 co2 = TransCo co1 co2
-mkNthCo :: HasDebugCallStack
+mkSelCo :: HasDebugCallStack
=> Role -- The role of the coercion you're creating
- -> Int -- Zero-indexed
+ -> CoSel
-> Coercion
-> Coercion
-mkNthCo r n co = mkNthCo_maybe r n co `orElse` NthCo r n co
+mkSelCo r n co = mkSelCo_maybe r n co `orElse` SelCo r n co
-mkNthCo_maybe :: HasDebugCallStack
+mkSelCo_maybe :: HasDebugCallStack
=> Role -- The role of the coercion you're creating
- -> Int -- Zero-indexed
+ -> CoSel
-> Coercion
-> Maybe Coercion
--- mkNthCo_maybe tries to optimise call to mkNthCo
-mkNthCo_maybe r n co
+-- mkSelCo_maybe tries to optimise call to mkSelCo
+mkSelCo_maybe r cs co
= assertPpr good_call bad_call_msg $
- go n co
+ go cs co
where
Pair ty1 ty2 = coercionKind co
- go n co
+ go cs co
| Just (ty, _) <- isReflCo_maybe co
- = Just (mkReflCo r (getNthFromType n ty))
+ = Just (mkReflCo r (getNthFromType cs ty))
- go 0 (ForAllCo _ kind_co _)
+ go SelForAll (ForAllCo _ kind_co _)
= assert (r == Nominal)
Just kind_co
-- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
- -- then (nth 0 co :: k1 ~N k2)
+ -- then (nth SelForAll co :: k1 ~N k2)
-- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
- -- then (nth 0 co :: (t1 ~ t2) ~N (t3 ~ t4))
+ -- then (nth SelForAll co :: (t1 ~ t2) ~N (t3 ~ t4))
- go n (FunCo _ w arg res)
- = Just (getNthFun n w arg res)
+ go (SelFun fs) (FunCo r0 w arg res)
+ = assertPpr (r == funRole r0 fs) (ppr r <+> ppr fs $$ ppr co) $
+ Just (getNthFun fs w arg res)
- go n (TyConAppCo r0 tc arg_cos) = assertPpr (r == nthRole r0 tc n)
- (vcat [ ppr tc
- , ppr arg_cos
- , ppr r0
- , ppr n
- , ppr r ]) $
- Just (arg_cos `getNth` n)
+ go (SelTyCon i) (TyConAppCo r0 tc arg_cos)
+ = assertPpr (r == tyConRole r0 tc i)
+ (vcat [ ppr tc
+ , ppr arg_cos
+ , ppr r0
+ , ppr i
+ , ppr r ]) $
+ Just (arg_cos `getNth` i)
- go n (SymCo co) -- Recurse, hoping to get to a TyConAppCo or FunCo
- = do { co' <- go n co; return (mkSymCo co') }
+ go cs (SymCo co) -- Recurse, hoping to get to a TyConAppCo or FunCo
+ = do { co' <- go cs co; return (mkSymCo co') }
go _ _ = Nothing
@@ -1117,14 +1123,15 @@ mkNthCo_maybe r n co
bad_call_msg = vcat [ text "Coercion =" <+> ppr co
, text "LHS ty =" <+> ppr ty1
, text "RHS ty =" <+> ppr ty2
- , text "n =" <+> ppr n, text "r =" <+> ppr r
+ , text "cs =" <+> ppr cs, text "r =" <+> ppr r
, text "coercion role =" <+> ppr (coercionRole co) ]
good_call
-- If the Coercion passed in is between forall-types, then the Int must
-- be 0 and the role must be Nominal.
| Just (_tv1, _) <- splitForAllTyCoVar_maybe ty1
, Just (_tv2, _) <- splitForAllTyCoVar_maybe ty2
- = n == 0 && r == Nominal
+ , SelForAll <- cs
+ = r == Nominal
-- If the Coercion passed in is between T tys and T tys', then the Int
-- must be less than the length of tys/tys' (which must be the same
@@ -1135,59 +1142,58 @@ mkNthCo_maybe r n co
-- role passed in must be tyConRolesRepresentational T !! n. If the role
-- of the Coercion is Phantom, then the role passed in must be Phantom.
--
- -- See also Note [NthCo Cached Roles] if you're wondering why it's
+ -- See also Note [SelCo Cached Roles] if you're wondering why it's
-- glaringly obvious that we should be *computing* this role instead of
-- npassing it in.
| isFunTy ty1, isFunTy ty2
- = n < 3 && r == nthFunRole (coercionRole co) n
+ , SelFun fs <- cs
+ = r == funRole (coercionRole co) fs
| Just (tc1, tys1) <- splitTyConApp_maybe ty1
, Just (tc2, tys2) <- splitTyConApp_maybe ty2
, tc1 == tc2
+ , SelTyCon n <- cs
= let len1 = length tys1
len2 = length tys2
in len1 == len2
&& n < len1
- && r == nthRole (coercionRole co) tc1 n
+ && r == tyConRole (coercionRole co) tc1 n
| otherwise
- = True
+ = False
-- | Extract the nth field of a FunCo
-getNthFun :: Int -- ^ "n"
+getNthFun :: FunSel
-> a -- ^ multiplicity
-> a -- ^ argument
-> a -- ^ result
- -> a -- ^ One of rhe above three
+ -> a -- ^ One of the above three
-- See Note [Function coercions]
-- If FunCo _ mult arg_co res_co :: (s1:TYPE sk1 :mult-> s2:TYPE sk2)
-- ~ (t1:TYPE tk1 :mult-> t2:TYPE tk2)
-- Then we want to behave as if co was
-- TyConAppCo mult argk_co resk_co arg_co res_co
-- where
--- argk_co :: sk1 ~ tk1 = mkNthCo 0 (mkKindCo arg_co)
--- resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co)
+-- argk_co :: sk1 ~ tk1 = mkSelCo 0 (mkKindCo arg_co)
+-- resk_co :: sk2 ~ tk2 = mkSelCo 0 (mkKindCo res_co)
-- i.e. mkRuntimeRepCo
-getNthFun n mult arg res
- = case n of
- 0 -> mult
- 1 -> arg
- 2 -> res
- _ -> bad_n
- where
- bad_n = pprPanic "getNthFun" (ppr n)
+getNthFun SelMult mult _ _ = mult
+getNthFun SelArg _ arg _ = arg
+getNthFun SelRes _ _ res = res
--- | If you're about to call @mkNthCo r n co@, then @r@ should be
+-- | If you're about to call @mkSelCo r n co@, then @r@ should be
-- whatever @nthCoRole n co@ returns.
-nthCoRole :: Int -> Coercion -> Role
-nthCoRole n co
- | isFunTy lty
- = nthFunRole r n
+nthCoRole :: CoSel -> Coercion -> Role
+nthCoRole cs co
+ | SelFun fs <- cs, isFunTy lty
+ = funRole r fs
- | Just (tc, _) <- splitTyConApp_maybe lty
- = nthRole r tc n
+ | SelTyCon n <- cs
+ , Just (tc, _) <- splitTyConApp_maybe lty
+ = tyConRole r tc n
- | Just _ <- splitForAllTyCoVar_maybe lty
+ | SelForAll <- cs
+ , Just _ <- splitForAllTyCoVar_maybe lty
= Nominal
| otherwise
@@ -1359,10 +1365,10 @@ setNominalRole_maybe r co
= 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 (NthCo _r n co)
+ setNominalRole_maybe_helper (SelCo _r n co)
-- NB, this case recurses via setNominalRole_maybe, not
-- setNominalRole_maybe_helper!
- = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
+ = SelCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
setNominalRole_maybe_helper (InstCo co arg)
= InstCo <$> setNominalRole_maybe_helper co <*> pure arg
setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
@@ -1399,27 +1405,25 @@ tyConRolesX :: Role -> TyCon -> [Role]
tyConRolesX Representational tc = tyConRolesRepresentational tc
tyConRolesX role _ = repeat role
-funRolesX :: Role -> [Role]
-funRolesX Representational = funRolesRepresentational
-funRolesX role = repeat role
-
-- Returns the roles of the parameters of a tycon, with an infinite tail
-- of Nominal
tyConRolesRepresentational :: TyCon -> [Role]
tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
-funRolesRepresentational :: [Role]
-funRolesRepresentational = [Nominal,Representational,Representational]
+tyConRole :: Role -> TyCon -> Int -> Role
+tyConRole Nominal _ _ = Nominal
+tyConRole Phantom _ _ = Phantom
+tyConRole Representational tc n = tyConRolesRepresentational tc `getNth` n
-nthRole :: Role -> TyCon -> Int -> Role
-nthRole Nominal _ _ = Nominal
-nthRole Phantom _ _ = Phantom
-nthRole Representational tc n = tyConRolesRepresentational tc `getNth` n
+funRole :: Role -> FunSel -> Role
+funRole Nominal _ = Nominal
+funRole Phantom _ = Phantom
+funRole Representational fs = funRoleRepresentational fs
-nthFunRole :: Role -> Int -> Role
-nthFunRole Nominal _ = Nominal
-nthFunRole Phantom _ = Phantom
-nthFunRole Representational n = funRolesRepresentational `getNth` n
+funRoleRepresentational :: FunSel -> Role
+funRoleRepresentational SelMult = Nominal
+funRoleRepresentational SelArg = Representational
+funRoleRepresentational SelRes = Representational
ltRole :: Role -> Role -> Bool
-- Is one role "less" than another?
@@ -1498,8 +1502,8 @@ promoteCoercion co = case co of
TransCo co1 co2
-> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
- NthCo r n co1
- | Just co' <- mkNthCo_maybe r n co1
+ SelCo r n co1
+ | Just co' <- mkSelCo_maybe r n co1
-> promoteCoercion co'
| otherwise
@@ -1552,10 +1556,12 @@ instCoercion (Pair lty rty) g w
-- w :: s1 ~ s2
-- returns mkInstCo g w' :: t2 [t1 |-> s1 ] ~ t3 [t1 |-> s2]
= Just $ mkInstCo g w'
+
| isFunTy lty && isFunTy rty
-- g :: (t1 -> t2) ~ (t3 -> t4)
-- returns t2 ~ t4
- = Just $ mkNthCo Nominal 4 g -- extract result type, which is the 5th argument to (->)
+ = Just $ mkSelCo Nominal (SelFun SelRes) g -- extract result type
+
| otherwise -- one forall, one funty...
= Nothing
@@ -2202,8 +2208,8 @@ liftCoSubstCoVarBndrUsing view_co fun lc@(LC subst cenv) old_var
role = coVarRole old_var
eta' = downgradeRole role Nominal eta
- eta1 = mkNthCo role 2 eta'
- eta2 = mkNthCo role 3 eta'
+ eta1 = mkSelCo role (SelTyCon 2) eta'
+ eta2 = mkSelCo role (SelTyCon 3) eta'
co1 = mkCoVarCo new_var
co2 = mkSymCo eta1 `mkTransCo` co1 `mkTransCo` eta2
@@ -2298,7 +2304,7 @@ seqCo (UnivCo p r t1 t2)
= seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
seqCo (SymCo co) = seqCo co
seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
-seqCo (NthCo r n co) = r `seq` n `seq` seqCo co
+seqCo (SelCo r n co) = r `seq` n `seq` seqCo co
seqCo (LRCo lr co) = lr `seq` seqCo co
seqCo (InstCo co arg) = seqCo co `seq` seqCo arg
seqCo (KindCo co) = seqCo co
@@ -2364,7 +2370,7 @@ coercionLKind co
go (InstCo aco arg) = go_app aco [go arg]
go (KindCo co) = typeKind (go co)
go (SubCo co) = go co
- go (NthCo _ d co) = getNthFromType d (go co)
+ go (SelCo _ d co) = getNthFromType d (go co)
go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
go (AxiomRuleCo ax cos) = pFst $ expectJust "coercionKind" $
coaxrProves ax $ map coercionKind cos
@@ -2387,25 +2393,22 @@ coercionLKind co
go_app (InstCo co arg) args = go_app co (go arg:args)
go_app co args = piResultTys (go co) args
-getNthFromType :: HasDebugCallStack => Int -> Type -> Type
-getNthFromType d ty
+getNthFromType :: HasDebugCallStack => CoSel -> Type -> Type
+getNthFromType (SelFun fs) ty
| Just (_af, mult, arg, res) <- splitFunTy_maybe ty
- = getNthFun d mult arg res
+ = getNthFun fs mult arg res
+getNthFromType (SelTyCon n) ty
| Just args <- tyConAppArgs_maybe ty
- = assertPpr (args `lengthExceeds` d) bad_doc $
- args `getNth` d
+ = assertPpr (args `lengthExceeds` n) (ppr n $$ ppr ty) $
+ args `getNth` n
- | d == 0
- , Just (tv,_) <- splitForAllTyCoVar_maybe ty
- -- Works for both tyvar and covar
- -- nth:0 pulls out a kind coercion from a hetero forall
+getNthFromType SelForAll ty -- Works for both tyvar and covar
+ | Just (tv,_) <- splitForAllTyCoVar_maybe ty
= tyVarKind tv
- | otherwise
- = pprPanic "getNthFromType" bad_doc
- where
- bad_doc = ppr d $$ ppr ty
+getNthFromType cs ty
+ = pprPanic "getNthFromType" (ppr cs $$ ppr ty)
coercionRKind :: Coercion -> Type
coercionRKind co
@@ -2426,7 +2429,7 @@ coercionRKind co
go (InstCo aco arg) = go_app aco [go arg]
go (KindCo co) = typeKind (go co)
go (SubCo co) = go co
- go (NthCo _ d co) = getNthFromType d (go co)
+ go (SelCo _ d co) = getNthFromType d (go co)
go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
go (AxiomRuleCo ax cos) = pSnd $ expectJust "coercionKind" $
coaxrProves ax $ map coercionKind cos
@@ -2471,10 +2474,11 @@ coercionRKind co
| isCoVar cv1
= mkTyCoInvForAllTy cv2 (go_forall subst' co)
where
- k2 = coercionRKind k_co
- r = coVarRole cv1
- eta1 = mkNthCo r 2 (downgradeRole r Nominal k_co)
- eta2 = mkNthCo r 3 (downgradeRole r Nominal k_co)
+ k2 = coercionRKind k_co
+ r = coVarRole cv1
+ k_co' = downgradeRole r Nominal k_co
+ eta1 = mkSelCo r (SelTyCon 2) k_co'
+ eta2 = mkSelCo r (SelTyCon 3) k_co'
-- k_co :: (t1 ~r t2) ~N (s1 ~r s2)
-- k1 = t1 ~r t2
@@ -2528,7 +2532,7 @@ coercionRole = go
go (UnivCo _ r _ _) = r
go (SymCo co) = go co
go (TransCo co1 _co2) = go co1
- go (NthCo r _d _co) = r
+ go (SelCo r _d _co) = r
go (LRCo {}) = Nominal
go (InstCo co _) = go co
go (KindCo {}) = Nominal
@@ -2669,8 +2673,8 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
r = coVarRole cv1
kind_co' = downgradeRole r Nominal kind_co
- eta1 = mkNthCo r 2 kind_co'
- eta2 = mkNthCo r 3 kind_co'
+ eta1 = mkSelCo r (SelTyCon 2) kind_co'
+ eta2 = mkSelCo r (SelTyCon 3) kind_co'
subst = mkEmptySubst $ mkInScopeSet $
tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
=====================================
compiler/GHC/Core/Coercion.hs-boot
=====================================
@@ -24,7 +24,7 @@ mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkUnivCo :: UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkSymCo :: Coercion -> Coercion
mkTransCo :: Coercion -> Coercion -> Coercion
-mkNthCo :: HasDebugCallStack => Role -> Int -> Coercion -> Coercion
+mkSelCo :: HasDebugCallStack => Role -> CoSel -> Coercion -> Coercion
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkInstCo :: Coercion -> Coercion -> Coercion
mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
=====================================
compiler/GHC/Core/Coercion/Opt.hs
=====================================
@@ -338,31 +338,30 @@ opt_co4 env sym rep r (TransCo co1 co2)
co2' = opt_co4_wrap env sym rep r co2
in_scope = lcInScopeSet env
-opt_co4 env _sym rep r (NthCo _r n co)
+opt_co4 env _sym rep r (SelCo _r n co)
| Just (ty, _) <- isReflCo_maybe co
= assert (r == _r ) $
liftCoSubst (chooseRole rep r) env (getNthFromType n ty)
-opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
+opt_co4 env sym rep r (SelCo r1 (SelTyCon n) (TyConAppCo _ _ cos))
= assert (r == r1 )
opt_co4_wrap env sym rep r (cos `getNth` n)
-- see the definition of GHC.Builtin.Types.Prim.funTyCon
-opt_co4 env sym rep r (NthCo r1 n (FunCo _r2 w co1 co2))
+opt_co4 env sym rep r (SelCo r1 (SelFun fs) (FunCo _r2 w co1 co2))
= assert (r == r1 )
- opt_co4_wrap env sym rep r (getNthFun n w co1 co2)
+ opt_co4_wrap env sym rep r (getNthFun fs w co1 co2)
-opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _))
+opt_co4 env sym rep r (SelCo _r SelForAll (ForAllCo _ eta _))
-- works for both tyvar and covar
= assert (r == _r )
- assert (n == 0 )
opt_co4_wrap env sym rep Nominal eta
-opt_co4 env sym rep r (NthCo _r n co)
- | Just nth_co <- case co' of
- TyConAppCo _ _ cos -> Just (cos `getNth` n)
- FunCo _ w co1 co2 -> Just (getNthFun n w co1 co2)
- ForAllCo _ eta _ -> Just eta
+opt_co4 env sym rep r (SelCo _r 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
_ -> Nothing
= if rep && (r == Nominal)
-- keep propagating the SubCo
@@ -370,7 +369,7 @@ opt_co4 env sym rep r (NthCo _r n co)
else nth_co
| otherwise
- = wrapRole rep r $ NthCo r n co'
+ = wrapRole rep r $ SelCo r n co'
where
co' = opt_co1 env sym co
@@ -453,8 +452,8 @@ opt_co4 env sym rep r (InstCo co1 arg)
-- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2)
r2 = coVarRole cv
kind_co' = downgradeRole r2 Nominal kind_co
- n1 = mkNthCo r2 2 kind_co'
- n2 = mkNthCo r2 3 kind_co'
+ n1 = mkSelCo r2 (SelTyCon 2) kind_co'
+ n2 = mkSelCo r2 (SelTyCon 3) kind_co'
in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1
(n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2))
@@ -575,9 +574,9 @@ opt_univ env sym prov role oty1 oty2
eta = mkUnivCo prov' Nominal k1 k2
eta_d = downgradeRole r' Nominal eta
-- eta gets opt'ed soon, but not yet.
- n_co = (mkSymCo $ mkNthCo r' 2 eta_d) `mkTransCo`
+ n_co = (mkSymCo $ mkSelCo r' (SelTyCon 2) eta_d) `mkTransCo`
(mkCoVarCo cv1) `mkTransCo`
- (mkNthCo r' 3 eta_d)
+ (mkSelCo r' (SelTyCon 3) eta_d)
ty2' = substTyWithCoVars [cv2] [n_co] ty2
(env', cv1', eta') = optForAllCoBndr env sym cv1 eta
@@ -649,13 +648,13 @@ opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
mkGReflRightCo r1 t1 (opt_trans is co1 co2)
-- Push transitivity through matching destructors
-opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
+opt_trans_rule is in_co1@(SelCo r1 d1 co1) in_co2@(SelCo r2 d2 co2)
| d1 == d2
, coercionRole co1 == coercionRole co2
, co1 `compatible_co` co2
= assert (r1 == r2) $
fireTransRule "PushNth" in_co1 in_co2 $
- mkNthCo r1 d1 (opt_trans is co1 co2)
+ mkSelCo r1 d1 (opt_trans is co1 co2)
opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
| d1 == d2
@@ -770,8 +769,8 @@ opt_trans_rule is co1 co2
is' = is `extendInScopeSet` cv1
role = coVarRole cv1
eta1' = downgradeRole role Nominal eta1
- n1 = mkNthCo role 2 eta1'
- n2 = mkNthCo role 3 eta1'
+ n1 = mkSelCo role (SelTyCon 2) eta1'
+ n2 = mkSelCo role (SelTyCon 3) eta1'
r2' = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mkTransCo`
(mkCoVarCo cv1) `mkTransCo` n2])
r2
@@ -1132,9 +1131,9 @@ Similarly, we do this
Here,
- h1 = mkNthCo Nominal 0 g :: (s1~s2)~(s3~s4)
- eta1 = mkNthCo r 2 h1 :: (s1 ~ s3)
- eta2 = mkNthCo r 3 h1 :: (s2 ~ s4)
+ h1 = mkSelCo Nominal 0 g :: (s1~s2)~(s3~s4)
+ eta1 = mkSelCo r (SelTyCon 2) h1 :: (s1 ~ s3)
+ eta2 = mkSelCo r (SelTyCon 3) h1 :: (s2 ~ s4)
h2 = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
-}
etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
@@ -1146,7 +1145,7 @@ etaForAllCo_ty_maybe co
| Pair ty1 ty2 <- coercionKind co
, Just (tv1, _) <- splitForAllTyVar_maybe ty1
, isForAllTy_ty ty2
- , let kind_co = mkNthCo Nominal 0 co
+ , let kind_co = mkSelCo Nominal SelForAll co
= Just ( tv1, kind_co
, mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
@@ -1162,13 +1161,13 @@ etaForAllCo_co_maybe co
| Pair ty1 ty2 <- coercionKind co
, Just (cv1, _) <- splitForAllCoVar_maybe ty1
, isForAllTy_co ty2
- = let kind_co = mkNthCo Nominal 0 co
+ = let kind_co = mkSelCo Nominal SelForAll co
r = coVarRole cv1
l_co = mkCoVarCo cv1
kind_co' = downgradeRole r Nominal kind_co
- r_co = (mkSymCo (mkNthCo r 2 kind_co')) `mkTransCo`
- l_co `mkTransCo`
- (mkNthCo r 3 kind_co')
+ r_co = mkSymCo (mkSelCo r (SelTyCon 2) kind_co')
+ `mkTransCo` l_co
+ `mkTransCo` mkSelCo r (SelTyCon 3) kind_co'
in Just ( cv1, kind_co
, mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co))
@@ -1205,7 +1204,7 @@ etaTyConAppCo_maybe tc co
, Just (tc1, tys1) <- splitTyConApp_maybe ty1
, Just (tc2, tys2) <- splitTyConApp_maybe ty2
, tc1 == tc2
- , isInjectiveTyCon tc r -- See Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
+ , isInjectiveTyCon tc r -- See Note [SelCo and newtypes] in GHC.Core.TyCo.Rep
, let n = length tys1
, tys2 `lengthIs` n -- This can fail in an erroneous program
-- E.g. T a ~# T a b
=====================================
compiler/GHC/Core/FVs.hs
=====================================
@@ -398,7 +398,7 @@ orphNamesOfCo (UnivCo p _ t1 t2) = orphNamesOfProv p `unionNameSet` orphNames
`unionNameSet` orphNamesOfType t2
orphNamesOfCo (SymCo co) = orphNamesOfCo co
orphNamesOfCo (TransCo co1 co2) = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
-orphNamesOfCo (NthCo _ _ co) = orphNamesOfCo co
+orphNamesOfCo (SelCo _ _ co) = orphNamesOfCo co
orphNamesOfCo (LRCo _ co) = orphNamesOfCo co
orphNamesOfCo (InstCo co arg) = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg
orphNamesOfCo (KindCo co) = orphNamesOfCo co
=====================================
compiler/GHC/Core/Lint.hs
=====================================
@@ -2041,7 +2041,7 @@ that returned coercion. If we get long chains, that can be asymptotically
inefficient, notably in
* TransCo
* InstCo
-* NthCo (cf #9233)
+* SelCo (cf #9233)
* LRCo
But the code is simple. And this is only Lint. Let's wait to see if
@@ -2299,33 +2299,34 @@ lintCoercion co@(TransCo co1 co2)
; lintRole co (coercionRole co1) (coercionRole co2)
; return (TransCo co1' co2') }
-lintCoercion the_co@(NthCo r0 n co)
+lintCoercion the_co@(SelCo r0 cs co)
= do { co' <- lintCoercion co
; let (Pair s t, r) = coercionKindRole co'
; case (splitForAllTyCoVar_maybe s, splitForAllTyCoVar_maybe t) of
{ (Just _, Just _)
-- works for both tyvar and covar
- | n == 0
+ | SelForAll <- cs
, (isForAllTy_ty s && isForAllTy_ty t)
|| (isForAllTy_co s && isForAllTy_co t)
-> do { lintRole the_co Nominal r0
- ; return (NthCo r0 n co') }
+ ; return (SelCo r0 cs co') }
; _ -> case (isFunTy s, isFunTy t) of
{ (True, True)
- | n < 3
- -> do { lintRole the_co (nthFunRole r n) r0
- ; return (NthCo r0 n co') }
+ | SelFun fs <- cs
+ -> do { lintRole the_co (funRole r fs) r0
+ ; return (SelCo r0 cs co') }
; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
{ (Just (tc_s, tys_s), Just (tc_t, tys_t))
| tc_s == tc_t
+ , SelTyCon n <- cs
, isInjectiveTyCon tc_s r
- -- see Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
+ -- see Note [SelCo and newtypes] in GHC.Core.TyCo.Rep
, tys_s `equalLength` tys_t
, tys_s `lengthExceeds` n
- -> do { lintRole the_co (nthRole r tc_s n) r0
- ; return (NthCo r0 n co') }
+ -> do { lintRole the_co (tyConRole r tc_s n) r0
+ ; return (SelCo r0 cs co') }
; _ -> failWithL (hang (text "Bad getNth:")
2 (ppr the_co $$ ppr s $$ ppr t)) }}}}
=====================================
compiler/GHC/Core/Opt/Arity.hs
=====================================
@@ -2564,11 +2564,11 @@ pushCoTyArg co ty
-- tyL = forall (a1 :: k1). ty1
-- tyR = forall (a2 :: k2). ty2
- co1 = mkSymCo (mkNthCo Nominal 0 co)
+ co1 = mkSymCo (mkSelCo Nominal SelForAll co)
-- co1 :: k2 ~N k1
- -- Note that NthCo can extract a Nominal equality between the
+ -- Note that SelCo can extract a Nominal equality between the
-- kinds of the types related by a coercion between forall-types.
- -- See the NthCo case in GHC.Core.Lint.
+ -- See the SelCo case in GHC.Core.Lint.
co2 = mkInstCo co (mkGReflLeftCo Nominal ty co1)
-- co2 :: ty1[ (ty|>co1)/a1 ] ~ ty2[ ty/a2 ]
@@ -2759,14 +2759,14 @@ collectBindersPushingCo e
, let Pair tyL tyR = coercionKind co
, assert (isForAllTy_ty tyL) $
isForAllTy_ty tyR
- , isReflCo (mkNthCo Nominal 0 co) -- See Note [collectBindersPushingCo]
+ , isReflCo (mkSelCo Nominal SelForAll co) -- See Note [collectBindersPushingCo]
= go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkTyVarTy b)))
| isCoVar b
, let Pair tyL tyR = coercionKind co
, assert (isForAllTy_co tyL) $
isForAllTy_co tyR
- , isReflCo (mkNthCo Nominal 0 co) -- See Note [collectBindersPushingCo]
+ , isReflCo (mkSelCo Nominal SelForAll co) -- See Note [collectBindersPushingCo]
, let cov = mkCoVarCo b
= go_c (b:bs) e (mkInstCo co (mkNomReflCo (mkCoercionTy cov)))
=====================================
compiler/GHC/Core/Opt/Simplify/Iteration.hs
=====================================
@@ -1543,7 +1543,7 @@ In particular, we want to behave well on
* (f |> co) @t1 @t2 ... @tn x1 .. xm
Here we will use pushCoTyArg and pushCoValArg successively, which
- build up NthCo stacks. Silly to do that if co is reflexive.
+ build up SelCo stacks. Silly to do that if co is reflexive.
However, we don't want to call isReflexiveCo too much, because it uses
type equality which is expensive on big types (#14737 comment:7).
=====================================
compiler/GHC/Core/TyCo/FVs.hs
=====================================
@@ -630,7 +630,7 @@ tyCoFVsOfCo (UnivCo p _ t1 t2) fv_cand in_scope acc
`unionFV` tyCoFVsOfType t2) fv_cand in_scope acc
tyCoFVsOfCo (SymCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (TransCo co1 co2) fv_cand in_scope acc = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
-tyCoFVsOfCo (NthCo _ _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
+tyCoFVsOfCo (SelCo _ _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (LRCo _ co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
tyCoFVsOfCo (InstCo co arg) fv_cand in_scope acc = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
tyCoFVsOfCo (KindCo co) fv_cand in_scope acc = tyCoFVsOfCo co fv_cand in_scope acc
@@ -690,7 +690,7 @@ almost_devoid_co_var_of_co (SymCo co) cv
almost_devoid_co_var_of_co (TransCo co1 co2) cv
= almost_devoid_co_var_of_co co1 cv
&& almost_devoid_co_var_of_co co2 cv
-almost_devoid_co_var_of_co (NthCo _ _ co) cv
+almost_devoid_co_var_of_co (SelCo _ _ co) cv
= almost_devoid_co_var_of_co co cv
almost_devoid_co_var_of_co (LRCo _ co) cv
= almost_devoid_co_var_of_co co cv
=====================================
compiler/GHC/Core/TyCo/Rep.hs
=====================================
@@ -36,7 +36,7 @@ module GHC.Core.TyCo.Rep (
ArgFlag(..), AnonArgFlag(..),
-- * Coercions
- Coercion(..),
+ Coercion(..), CoSel(..), FunSel(..),
UnivCoProvenance(..),
CoercionHole(..), coHoleCoVar, setCoHoleCoVar,
CoercionN, CoercionR, CoercionP, KindCoercion,
@@ -97,10 +97,12 @@ import GHC.Utils.Outputable
import GHC.Data.FastString
import GHC.Utils.Misc
import GHC.Utils.Panic
+import GHC.Utils.Binary
-- libraries
import qualified Data.Data as Data hiding ( TyCon )
import Data.IORef ( IORef ) -- for CoercionHole
+import Control.DeepSeq
{- **********************************************************************
* *
@@ -1208,7 +1210,7 @@ data Coercion
| ForAllCo TyCoVar KindCoercion Coercion
-- ForAllCo :: _ -> N -> e -> e
- | FunCo Role CoercionN Coercion Coercion -- lift FunTy
+ | FunCo Role CoercionN Coercion Coercion -- See Note [FunCo]
-- FunCo :: "e" -> N -> e -> e -> e
-- These are special
@@ -1236,14 +1238,7 @@ data Coercion
| SymCo Coercion -- :: e -> e
| TransCo Coercion Coercion -- :: e -> e -> e
- | NthCo Role Int Coercion -- Zero-indexed; decomposes (T t0 ... tn)
- -- :: "e" -> _ -> e0 -> e (inverse of TyConAppCo, see Note [TyConAppCo roles])
- -- Using NthCo on a ForAllCo gives an N coercion always
- -- See Note [NthCo and newtypes]
- --
- -- Invariant: (NthCo r i co), it is always the case that r = role of (Nth i co)
- -- That is: the role of the entire coercion is redundantly cached here.
- -- See Note [NthCo Cached Roles]
+ | SelCo Role CoSel Coercion -- See Note [SelCo]
| LRCo LeftOrRight CoercionN -- Decomposes (t_left t_right)
-- :: _ -> N -> N
@@ -1263,6 +1258,18 @@ data Coercion
-- Only present during typechecking
deriving Data.Data
+data CoSel -- See Note [SelCo]
+ = SelTyCon Int -- Decomposes (T co1 ... con); zero-indexed
+ | SelFun FunSel -- Decomposes (co1 -> co2)
+ | SelForAll -- Decomposes (forall a. co)
+ deriving( Eq, Data.Data )
+
+data FunSel -- See Note [SelCo]
+ = SelMult -- Multiplicity
+ | SelArg -- Argument of function
+ | SelRes -- Result of function
+ deriving( Eq, Data.Data )
+
type CoercionN = Coercion -- always nominal
type CoercionR = Coercion -- always representational
type CoercionP = Coercion -- always phantom
@@ -1271,6 +1278,36 @@ type KindCoercion = CoercionN -- always nominal
instance Outputable Coercion where
ppr = pprCo
+instance Outputable CoSel where
+ ppr (SelTyCon n) = text "Tc" <> parens (int n)
+ ppr SelForAll = text "All"
+ ppr (SelFun fs) = text "Fun" <> parens (ppr fs)
+
+instance Outputable FunSel where
+ ppr SelMult = text "mult"
+ ppr SelArg = text "arg"
+ ppr SelRes = text "res"
+
+instance Binary CoSel where
+ put_ bh (SelTyCon n) = do { putByte bh 0; put_ bh n }
+ put_ bh SelForAll = putByte bh 1
+ put_ bh (SelFun SelMult) = putByte bh 2
+ put_ bh (SelFun SelArg) = putByte bh 3
+ put_ bh (SelFun SelRes) = putByte bh 4
+
+ get bh = do { h <- getByte bh
+ ; case h of
+ 0 -> do { n <- get bh; return (SelTyCon n) }
+ 1 -> return SelForAll
+ 2 -> return (SelFun SelMult)
+ 3 -> return (SelFun SelArg)
+ _ -> return (SelFun SelRes) }
+
+instance NFData CoSel where
+ rnf (SelTyCon n) = n `seq` ()
+ rnf SelForAll = ()
+ rnf (SelFun fs) = fs `seq` ()
+
-- | A semantically more meaningful type to represent what may or may not be a
-- useful 'Coercion'.
data MCoercion
@@ -1343,6 +1380,71 @@ It is easy to see that
A nominal reflexive coercion is quite common, so we keep the special form Refl to
save allocation.
+Note [Coercion selection]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+The Coercion form SelCo allows us to decompose a structural coercion, one
+between ForallTys, or TyConApps, or FunTys.
+
+Invariant: (SelCo r cs co), it is always the case that
+ r = role of (Nth cs co)
+ That is: the role of the entire coercion is redundantly cached here.
+ See Note [SelCo Cached Roles]
+
+There are three forms, split by the CoSel field inside the SelCo:
+SelTyCon, SelForAll, and SelFun.
+
+* SelTyCon:
+
+ co : (T s1..sn) ~r0 (T t1..tn)
+ T is a data type not a newtype
+ r = tyConRole tc r0 i
+ i < n (i is zero-indexed)
+ ----------------------------------
+ SelCo r (SelTyCon i) : si ~r ti
+
+ See Note [SelCo and newtypes]
+
+
+* SelForAll:
+ co : forall (a:k1).t1 ~r0 forall (a:k2).t2
+ ----------------------------------
+ SelCo N SelForAll : k1 ~N k2
+
+ NB: SelForAll always gives a Nominal coercion.
+
+* The SelFun form, for functions, has three sub-forms for the three
+ components of the function type (multiplicity, argument, result).
+
+ co : (s1 %{m1}-> t1) ~r0 (s2 %{m2}-> t2)
+ r = funRole r0 SelMult
+ ----------------------------------
+ SelCo r (SelFun SelMult) : m1 ~r m2
+
+ co : (s1 %{m1}-> t1) ~r0 (s2 %{m2}-> t2)
+ r = funRole r0 SelArg
+ ----------------------------------
+ SelCo r (SelFun SelArg) : s1 ~r s2
+
+ co : (s1 %{m1}-> t1) ~r0 (s2 %{m2}-> t2)
+ r = funRole r0 SelRes
+ ----------------------------------
+ SelCo r (SelFun SelRes) : t1 ~r t2
+
+Note [FunCo]
+~~~~~~~~~~~~
+You might think that a FunCo (which connects two function types should
+contain the AnonArgFlag from the function types. But we are allowed to
+have an axiom (and hence a coercion) connecting Type and Constraint, thus
+ co :: (t::Type) ~ (c::Constraint)
+c.f. GHC.Builtin.Types.Prim Note [Type and Constraint are not apart]
+Given such a coercion we can use FunCo to make
+ FunCo co <Int> :: (t -> Int) ~ (c => Int)
+Note that the two arrows are different: those FunTys have different
+AnonArgFlags! That's why:
+
+* FunCo does not store an AnonArgFlag
+* We use mkFuntionType in the FunCo case of coercionLKind/coercoinRKind,
+
Note [Coercion axioms applied to coercions]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The reason coercion axioms can be applied to coercions and not just
@@ -1575,7 +1677,7 @@ TyConAppCo Phantom Foo (UnivCo Phantom Int Bool) : Foo Int ~P Foo Bool
The rules here dictate the roles of the parameters to mkTyConAppCo
(should be checked by Lint).
-Note [NthCo and newtypes]
+Note [SelCo and newtypes]
~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have
@@ -1592,20 +1694,20 @@ We can then build
co = NTCo:N a ; sym (NTCo:N b)
for any `a` and `b`. Because of the role annotation on N, if we use
-NthCo, we'll get out a representational coercion. That is:
+SelCo, we'll get out a representational coercion. That is:
- NthCo r 0 co :: forall a b. a ~R b
+ SelCo r 0 co :: forall a b. a ~R b
Yikes! Clearly, this is terrible. The solution is simple: forbid
-NthCo to be used on newtypes if the internal coercion is representational.
+SelCo to be used on newtypes if the internal coercion is representational.
This is not just some corner case discovered by a segfault somewhere;
it was discovered in the proof of soundness of roles and described
in the "Safe Coercions" paper (ICFP '14).
-Note [NthCo Cached Roles]
+Note [SelCo Cached Roles]
~~~~~~~~~~~~~~~~~~~~~~~~~
-Why do we cache the role of NthCo in the NthCo constructor?
+Why do we cache the role of SelCo in the SelCo constructor?
Because computing role(Nth i co) involves figuring out that
co :: T tys1 ~ T tys2
@@ -1615,7 +1717,7 @@ at the tyConRoles of T. Avoiding bad asymptotic behaviour here means
we have to compute the kind and role of a coercion simultaneously,
which makes the code complicated and inefficient.
-This only happens for NthCo. Caching the role solves the problem, and
+This only happens for SelCo. Caching the role solves the problem, and
allows coercionKind and coercionRole to be simple.
See #11735
@@ -1982,7 +2084,7 @@ foldTyCo (TyCoFolder { tcf_view = view
go_co env (SymCo co) = go_co env co
go_co env (TransCo c1 c2) = go_co env c1 `mappend` go_co env c2
go_co env (AxiomRuleCo _ cos) = go_cos env cos
- go_co env (NthCo _ _ co) = go_co env co
+ go_co env (SelCo _ _ co) = go_co env co
go_co env (LRCo _ co) = go_co env co
go_co env (InstCo co arg) = go_co env co `mappend` go_co env arg
go_co env (KindCo co) = go_co env co
@@ -2046,7 +2148,7 @@ coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
-coercionSize (NthCo _ _ co) = 1 + coercionSize co
+coercionSize (SelCo _ _ co) = 1 + coercionSize co
coercionSize (LRCo _ co) = 1 + coercionSize co
coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg
coercionSize (KindCo co) = 1 + coercionSize co
=====================================
compiler/GHC/Core/TyCo/Rep.hs-boot
=====================================
@@ -8,6 +8,7 @@ import {-# SOURCE #-} GHC.Core.TyCon ( TyCon )
data Type
data Coercion
+data CoSel
data UnivCoProvenance
data TyLit
data TyCoBinder
=====================================
compiler/GHC/Core/TyCo/Subst.hs
=====================================
@@ -56,7 +56,7 @@ import GHC.Prelude
import {-# SOURCE #-} GHC.Core.Type
( mkCastTy, mkAppTy, isCoercionTy, mkTyConApp )
import {-# SOURCE #-} GHC.Core.Coercion
- ( mkCoVarCo, mkKindCo, mkNthCo, mkTransCo
+ ( mkCoVarCo, mkKindCo, mkSelCo, mkTransCo
, mkNomReflCo, mkSubCo, mkSymCo
, mkFunCo, mkForAllCo, mkUnivCo
, mkAxiomInstCo, mkAppCo, mkGReflCo
@@ -886,7 +886,7 @@ subst_co subst co
(go_ty t1)) $! (go_ty t2)
go (SymCo co) = mkSymCo $! (go co)
go (TransCo co1 co2) = (mkTransCo $! (go co1)) $! (go co2)
- go (NthCo r d co) = mkNthCo r d $! (go co)
+ go (SelCo r d co) = mkSelCo r d $! (go co)
go (LRCo lr co) = mkLRCo lr $! (go co)
go (InstCo co arg) = (mkInstCo $! (go co)) $! go arg
go (KindCo co) = mkKindCo $! (go co)
=====================================
compiler/GHC/Core/TyCo/Tidy.hs
=====================================
@@ -242,7 +242,7 @@ tidyCo env@(_, subst) co
tidyType env t1) $! tidyType env t2
go (SymCo co) = SymCo $! go co
go (TransCo co1 co2) = (TransCo $! go co1) $! go co2
- go (NthCo r d co) = NthCo r d $! go co
+ go (SelCo r d co) = SelCo r d $! go co
go (LRCo lr co) = LRCo lr $! go co
go (InstCo co ty) = (InstCo $! go co) $! go ty
go (KindCo co) = KindCo $! go co
=====================================
compiler/GHC/Core/Type.hs
=====================================
@@ -281,7 +281,7 @@ import {-# SOURCE #-} GHC.Core.Coercion
( mkNomReflCo, mkGReflCo, mkReflCo
, mkTyConAppCo, mkAppCo, mkCoVarCo, mkAxiomRuleCo
, mkForAllCo, mkFunCo, mkAxiomInstCo, mkUnivCo
- , mkSymCo, mkTransCo, mkNthCo, mkLRCo, mkInstCo
+ , mkSymCo, mkTransCo, mkSelCo, mkLRCo, mkInstCo
, mkKindCo, mkSubCo
, decomposePiCos, coercionKind, coercionLKind
, coercionRKind, coercionType
@@ -605,8 +605,8 @@ expandTypeSynonyms ty
= mkSymCo (go_co subst co)
go_co subst (TransCo co1 co2)
= mkTransCo (go_co subst co1) (go_co subst co2)
- go_co subst (NthCo r n co)
- = mkNthCo r n (go_co subst co)
+ go_co subst (SelCo r n co)
+ = mkSelCo r n (go_co subst co)
go_co subst (LRCo lr co)
= mkLRCo lr (go_co subst co)
go_co subst (InstCo co arg)
@@ -667,16 +667,15 @@ kindRep k = case kindRep_maybe k of
Just r -> r
Nothing -> pprPanic "kindRep" (ppr k)
--- | Given a kind (SORT _ rr), extract its RuntimeRep classifier rr.
+-- | Given a kind (TYPE rr) or (CONSTRAINT rr), extract its RuntimeRep classifier rr.
-- For example, @kindRep_maybe * = Just LiftedRep@
-- Returns 'Nothing' if the kind is not of form (TYPE rr)
--- Treats * and Constraint as the same
kindRep_maybe :: HasDebugCallStack => Kind -> Maybe RuntimeRepType
kindRep_maybe kind
| Just (_, rep) <- sORTKind_maybe kind = Just rep
| otherwise = Nothing
--- | Returns True if the argument is a lifted SORT
+-- | Returns True if the argument is a lifted type or constraint
-- See Note [Kind Constraint and kind Type]
isLiftedTypeKind :: Kind -> Bool
isLiftedTypeKind kind
@@ -969,7 +968,7 @@ mapTyCoX (TyCoMapper { tcm_tyvar = tyvar
go_co env (SymCo co) = mkSymCo <$> go_co env co
go_co env (TransCo c1 c2) = mkTransCo <$> go_co env c1 <*> go_co env c2
go_co env (AxiomRuleCo r cos) = AxiomRuleCo r <$> go_cos env cos
- go_co env (NthCo r i co) = mkNthCo r i <$> go_co env co
+ go_co env (SelCo r i co) = mkSelCo r i <$> go_co env co
go_co env (LRCo lr co) = mkLRCo lr <$> go_co env co
go_co env (InstCo co arg) = mkInstCo <$> go_co env co <*> go_co env arg
go_co env (KindCo co) = mkKindCo <$> go_co env co
@@ -3083,22 +3082,22 @@ isPredTy ty = case typeTypeOrConstraint ty of
-- | Does this classify a type allowed to have values? Responds True to things
-- like *, TYPE Lifted, TYPE IntRep, TYPE v, Constraint.
classifiesTypeWithValues :: Kind -> Bool
--- ^ True of a kind `SORT _ _`
+-- ^ True of a kind `TYPE _` or `CONSTRAINT _`
classifiesTypeWithValues k = isJust (sORTKind_maybe k)
isConstraintKind :: Kind -> Bool
--- True of (SORT ConstraintLike _)
+-- True of (CONSTRAINT _)
isConstraintKind kind
| Just (ConstraintLike, _) <- sORTKind_maybe kind
= True
| otherwise
= False
--- | Is this kind equivalent to 'Type' i.e. SORT TypeLike LiftedRep?
+tcIsLiftedTypeKind :: Kind -> Bool
+-- ^ Is this kind equivalent to 'Type' i.e. TYPE LiftedRep?
--
-- This considers 'Constraint' to be distinct from 'Type'. For a version that
-- treats them as the same type, see 'isLiftedTypeKind'.
-tcIsLiftedTypeKind :: Kind -> Bool
tcIsLiftedTypeKind kind
| Just (TypeLike, rep) <- sORTKind_maybe kind
= isLiftedRuntimeRep rep
@@ -3355,8 +3354,8 @@ occCheckExpand vs_to_avoid ty
go_co cxt (TransCo co1 co2) = do { co1' <- go_co cxt co1
; co2' <- go_co cxt co2
; return (mkTransCo co1' co2') }
- go_co cxt (NthCo r n co) = do { co' <- go_co cxt co
- ; return (mkNthCo r n co') }
+ go_co cxt (SelCo r n co) = do { co' <- go_co cxt co
+ ; return (mkSelCo r n co') }
go_co cxt (LRCo lr co) = do { co' <- go_co cxt co
; return (mkLRCo lr co') }
go_co cxt (InstCo co arg) = do { co' <- go_co cxt co
@@ -3416,7 +3415,7 @@ tyConsOfType ty
go_co (HoleCo {}) = emptyUniqSet
go_co (SymCo co) = go_co co
go_co (TransCo co1 co2) = go_co co1 `unionUniqSets` go_co co2
- go_co (NthCo _ _ co) = go_co co
+ go_co (SelCo _ _ co) = go_co co
go_co (LRCo _ co) = go_co co
go_co (InstCo co arg) = go_co co `unionUniqSets` go_co arg
go_co (KindCo co) = go_co co
@@ -3514,7 +3513,7 @@ during type inference.
-- | Checks that a kind of the form 'Type', 'Constraint'
-- or @'TYPE r@ is concrete. See 'isConcrete'.
--
--- __Precondition:__ The type has kind `SORT blah`
+-- __Precondition:__ The type has kind `TYPE blah` or `CONSTRAINT blah`
isFixedRuntimeRepKind :: HasDebugCallStack => Kind -> Bool
isFixedRuntimeRepKind k
= assertPpr (classifiesTypeWithValues k) (ppr k) $
@@ -3976,7 +3975,7 @@ mkTYPEapp_maybe :: RuntimeRepType -> Maybe Type
-- because those inner types should already have been rewritten
-- to LiftedRep and UnliftedRep respectively, by mkTyConApp
--
--- see Note [SORT, TYPE, and CONSTRAINT] in GHC.Builtin.Types.Prim.
+-- see Note [TYPE and CONSTRAINT] in GHC.Builtin.Types.Prim.
-- See Note [Using synonyms to compress types] in GHC.Core.Type
{-# NOINLINE mkTYPEapp_maybe #-}
mkTYPEapp_maybe (TyConApp tc args)
@@ -4010,7 +4009,7 @@ mkBoxedRepApp_maybe :: Type -> Maybe Type
-- On the fly, rewrite
-- BoxedRep Lifted --> liftedRepTy (a synonym)
-- BoxedRep Unlifted --> unliftedRepTy (ditto)
--- See Note [SORT, TYPE, and CONSTRAINT] in GHC.Builtin.Types.Prim.
+-- See Note [TYPE and CONSTRAINT] in GHC.Builtin.Types.Prim.
-- See Note [Using synonyms to compress types] in GHC.Core.Type
{-# NOINLINE mkBoxedRepApp_maybe #-}
mkBoxedRepApp_maybe (TyConApp tc args)
@@ -4024,7 +4023,7 @@ mkTupleRepApp_maybe :: Type -> Maybe Type
-- ^ Given a `[RuntimeRep]`, apply `TupleRep` to it
-- On the fly, rewrite
-- TupleRep [] -> zeroBitRepTy (a synonym)
--- See Note [SORT, TYPE, and CONSTRAINT] in GHC.Builtin.Types.Prim.
+-- See Note [TYPE and CONSTRAINT] in GHC.Builtin.Types.Prim.
-- See Note [Using synonyms to compress types] in GHC.Core.Type
{-# NOINLINE mkTupleRepApp_maybe #-}
mkTupleRepApp_maybe (TyConApp tc args)
=====================================
compiler/GHC/Core/Unify.hs
=====================================
@@ -1117,7 +1117,7 @@ unify_ty env ty1 ty2 _kco
= maybeApart MARTypeFamily
-- TYPE and CONSTRAINT are not Apart
- -- See Note [Type vs Constraint] in GHC.Builtin.Types.Prim
+ -- See Note [Type and Constraint are not apart] in GHC.Builtin.Types.Prim
-- NB: at this point we know that the two TyCons do not match
| Just {} <- sORTKind_maybe ty1
, Just {} <- sORTKind_maybe ty2
@@ -1637,9 +1637,9 @@ ty_co_match menv subst (ForAllTy (Bndr tv1 _) ty1)
-- 1. Given:
-- cv1 :: (s1 :: k1) ~r (s2 :: k2)
-- kind_co2 :: (s1' ~ s2') ~N (t1 ~ t2)
--- eta1 = mkNthCo role 2 (downgradeRole r Nominal kind_co2)
+-- eta1 = mkSelCo role (SelTyCon 2) (downgradeRole r Nominal kind_co2)
-- :: s1' ~ t1
--- eta2 = mkNthCo role 3 (downgradeRole r Nominal kind_co2)
+-- eta2 = mkSelCo role (SelTyCon 3) (downgradeRole r Nominal kind_co2)
-- :: s2' ~ t2
-- Wanted:
-- subst1 <- ty_co_match menv subst s1 eta1 kco1 kco2
=====================================
compiler/GHC/CoreToIface.hs
=====================================
@@ -289,7 +289,7 @@ toIfaceCoercionX fr co
go (AppCo co1 co2) = IfaceAppCo (go co1) (go co2)
go (SymCo co) = IfaceSymCo (go co)
go (TransCo co1 co2) = IfaceTransCo (go co1) (go co2)
- go (NthCo _r d co) = IfaceNthCo d (go co)
+ go (SelCo _r d co) = IfaceSelCo d (go co)
go (LRCo lr co) = IfaceLRCo lr (go co)
go (InstCo co arg) = IfaceInstCo (go co) (go arg)
go (KindCo c) = IfaceKindCo (go c)
=====================================
compiler/GHC/Iface/Rename.hs
=====================================
@@ -697,7 +697,7 @@ rnIfaceCo (IfaceTransCo c1 c2)
= IfaceTransCo <$> rnIfaceCo c1 <*> rnIfaceCo c2
rnIfaceCo (IfaceInstCo c1 c2)
= IfaceInstCo <$> rnIfaceCo c1 <*> rnIfaceCo c2
-rnIfaceCo (IfaceNthCo d c) = IfaceNthCo d <$> rnIfaceCo c
+rnIfaceCo (IfaceSelCo d c) = IfaceSelCo d <$> rnIfaceCo c
rnIfaceCo (IfaceLRCo lr c) = IfaceLRCo lr <$> rnIfaceCo c
rnIfaceCo (IfaceSubCo c) = IfaceSubCo <$> rnIfaceCo c
rnIfaceCo (IfaceAxiomRuleCo ax cos)
=====================================
compiler/GHC/Iface/Syntax.hs
=====================================
@@ -1693,7 +1693,7 @@ freeNamesIfCoercion (IfaceSymCo c)
= freeNamesIfCoercion c
freeNamesIfCoercion (IfaceTransCo c1 c2)
= freeNamesIfCoercion c1 &&& freeNamesIfCoercion c2
-freeNamesIfCoercion (IfaceNthCo _ co)
+freeNamesIfCoercion (IfaceSelCo _ co)
= freeNamesIfCoercion co
freeNamesIfCoercion (IfaceLRCo _ co)
= freeNamesIfCoercion co
=====================================
compiler/GHC/Iface/Type.hs
=====================================
@@ -74,7 +74,7 @@ import {-# SOURCE #-} GHC.Builtin.Types
, manyDataConTyCon
, liftedRepTyCon, liftedDataConTyCon )
import GHC.Core.Type ( isRuntimeRepTy, isMultiplicityTy, isLevityTy, anonArgTyCon )
-
+import GHC.Core.TyCo.Rep( CoSel )
import GHC.Core.TyCon hiding ( pprPromotionQuote )
import GHC.Core.Coercion.Axiom
import GHC.Types.Var
@@ -383,7 +383,7 @@ data IfaceCoercion
| IfaceUnivCo IfaceUnivCoProv Role IfaceType IfaceType
| IfaceSymCo IfaceCoercion
| IfaceTransCo IfaceCoercion IfaceCoercion
- | IfaceNthCo Int IfaceCoercion
+ | IfaceSelCo CoSel IfaceCoercion
| IfaceLRCo LeftOrRight IfaceCoercion
| IfaceInstCo IfaceCoercion IfaceCoercion
| IfaceKindCo IfaceCoercion
@@ -585,7 +585,7 @@ substIfaceType env ty
go_co (IfaceUnivCo prov r t1 t2) = IfaceUnivCo (go_prov prov) r (go t1) (go t2)
go_co (IfaceSymCo co) = IfaceSymCo (go_co co)
go_co (IfaceTransCo co1 co2) = IfaceTransCo (go_co co1) (go_co co2)
- go_co (IfaceNthCo n co) = IfaceNthCo n (go_co co)
+ go_co (IfaceSelCo n co) = IfaceSelCo n (go_co co)
go_co (IfaceLRCo lr co) = IfaceLRCo lr (go_co co)
go_co (IfaceInstCo c1 c2) = IfaceInstCo (go_co c1) (go_co c2)
go_co (IfaceKindCo co) = IfaceKindCo (go_co co)
@@ -1786,8 +1786,8 @@ ppr_co ctxt_prec (IfaceTransCo co1 co2)
ppr_trans c = [semi <+> ppr_co opPrec c]
in maybeParen ctxt_prec opPrec $
vcat (ppr_co topPrec co1 : ppr_trans co2)
-ppr_co ctxt_prec (IfaceNthCo d co)
- = ppr_special_co ctxt_prec (text "Nth:" <> int d) [co]
+ppr_co ctxt_prec (IfaceSelCo d co)
+ = ppr_special_co ctxt_prec (text "Nth:" <> ppr d) [co]
ppr_co ctxt_prec (IfaceLRCo lr co)
= ppr_special_co ctxt_prec (ppr lr) [co]
ppr_co ctxt_prec (IfaceSubCo co)
@@ -2077,7 +2077,7 @@ instance Binary IfaceCoercion where
putByte bh 11
put_ bh a
put_ bh b
- put_ bh (IfaceNthCo a b) = do
+ put_ bh (IfaceSelCo a b) = do
putByte bh 12
put_ bh a
put_ bh b
@@ -2148,7 +2148,7 @@ instance Binary IfaceCoercion where
return $ IfaceTransCo a b
12-> do a <- get bh
b <- get bh
- return $ IfaceNthCo a b
+ return $ IfaceSelCo a b
13-> do a <- get bh
b <- get bh
return $ IfaceLRCo a b
@@ -2234,7 +2234,7 @@ instance NFData IfaceCoercion where
IfaceUnivCo f1 f2 f3 f4 -> rnf f1 `seq` f2 `seq` rnf f3 `seq` rnf f4
IfaceSymCo f1 -> rnf f1
IfaceTransCo f1 f2 -> rnf f1 `seq` rnf f2
- IfaceNthCo f1 f2 -> rnf f1 `seq` rnf f2
+ IfaceSelCo f1 f2 -> rnf f1 `seq` rnf f2
IfaceLRCo f1 f2 -> f1 `seq` rnf f2
IfaceInstCo f1 f2 -> rnf f1 `seq` rnf f2
IfaceKindCo f1 -> rnf f1
=====================================
compiler/GHC/IfaceToCore.hs
=====================================
@@ -1420,8 +1420,8 @@ tcIfaceCo = go
<*> go c2
go (IfaceInstCo c1 t2) = InstCo <$> go c1
<*> go t2
- go (IfaceNthCo d c) = do { c' <- go c
- ; return $ mkNthCo (nthCoRole d c') d c' }
+ go (IfaceSelCo d c) = do { c' <- go c
+ ; return $ mkSelCo (nthCoRole d c') d c' }
go (IfaceLRCo lr c) = LRCo lr <$> go c
go (IfaceKindCo c) = KindCo <$> go c
go (IfaceSubCo c) = SubCo <$> go c
=====================================
compiler/GHC/Tc/Module.hs
=====================================
@@ -1249,7 +1249,7 @@ checkBootTyCon is_boot tc1 tc2
-- data T a = MkT
--
-- If you write this, we'll treat T as injective, and make inferences
- -- like T a ~R T b ==> a ~N b (mkNthCo). But if we can
+ -- like T a ~R T b ==> a ~N b (mkSelCo). But if we can
-- subsequently replace T with one at phantom role, we would then be able to
-- infer things like T Int ~R T Bool which is bad news.
--
=====================================
compiler/GHC/Tc/Solver/Canonical.hs
=====================================
@@ -1038,7 +1038,7 @@ can_eq_nc' _rewritten _rdr_env _envs ev eq_rel
(FunTy { ft_mult = am1, ft_af = af1, ft_arg = ty1a, ft_res = ty1b }) _ps_ty1
(FunTy { ft_mult = am2, ft_af = af2, ft_arg = ty2a, ft_res = ty2b }) _ps_ty2
| af1 == af2 -- See Note [Decomposing FunTy]
- = canDecomposableFunTy ev eq_rel [am1,ty1a,ty1b] [am2,ty2a,ty2b]
+ = canDecomposableFunTy ev eq_rel (am1,ty1a,ty1b) (am2,ty2a,ty2b)
-- Decompose type constructor applications
-- NB: we have expanded type synonyms already
@@ -1779,8 +1779,8 @@ Conclusion:
It all comes from the fact that newtypes aren't necessarily injective
w.r.t. representational equality.
-Furthermore, as explained in Note [NthCo and newtypes] in GHC.Core.TyCo.Rep, we can't use
-NthCo on representational coercions over newtypes. NthCo comes into play
+Furthermore, as explained in Note [SelCo and newtypes] in GHC.Core.TyCo.Rep, we can't use
+SelCo on representational coercions over newtypes. SelCo comes into play
only when decomposing givens.
Conclusion:
@@ -1892,7 +1892,7 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
-> do { let ev_co = mkCoVarCo evar
; given_evs <- newGivenEvVars loc $
[ ( mkPrimEqPredRole r ty1 ty2
- , evCoercion $ mkNthCo r i ev_co )
+ , evCoercion $ mkSelCo r (SelTyCon i) ev_co )
| (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..]
, r /= Phantom
, not (isCoercionTy ty1) && not (isCoercionTy ty2) ]
@@ -1927,22 +1927,29 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
= new_loc0 ]
++ repeat loc
-canDecomposableFunTy :: CtEvidence -> EqRel -> [Type] -> [Type]
+canDecomposableFunTy :: CtEvidence -> EqRel
+ -> (Type,Type,Type) -- (multiplicity,arg,res)
+ -> (Type,Type,Type) -- (multiplicity,arg,res)
-> TcS (StopOrContinue Ct)
-canDecomposableFunTy ev eq_rel tys1 tys2
+canDecomposableFunTy ev eq_rel f1@(m1,a1,r1) f2@(m2,a2,r2)
= do { traceTcS "canDecomposableFunTy"
- (ppr ev $$ ppr eq_rel $$ ppr tys1 $$ ppr tys2)
+ (ppr ev $$ ppr eq_rel $$ ppr f1 $$ ppr f2)
; case ev of
CtWanted { ctev_dest = dest, ctev_rewriters = rewriters }
- -> do { [mult,arg,res] <- zipWith4M (unifyWanted rewriters) new_locs tc_roles tys1 tys2
+ -> do { mult <- unifyWanted rewriters mult_loc (funRole role SelMult) m1 m2
+ ; arg <- unifyWanted rewriters loc (funRole role SelArg) a1 a2
+ ; res <- unifyWanted rewriters loc (funRole role SelRes) r1 r2
; setWantedEq dest (mkFunCo role mult arg res) }
CtGiven { ctev_evar = evar }
-> do { let ev_co = mkCoVarCo evar
; given_evs <- newGivenEvVars loc $
- [ ( mkPrimEqPredRole r ty1 ty2
- , evCoercion $ mkNthCo r i ev_co )
- | (r, ty1, ty2, i) <- zip4 tc_roles tys1 tys2 [0..] ]
+ [ ( mkPrimEqPredRole role' ty1 ty2
+ , evCoercion $ mkSelCo role' (SelFun fs) ev_co )
+ | (fs, ty1, ty2) <- [(SelMult, m1, m2)
+ ,(SelArg, a1, a2)
+ ,(SelRes, r2, r2)]
+ , let role' = funRole role fs ]
; emitWorkNC given_evs }
; stopWith ev "Decomposed TyConApp" }
@@ -1950,8 +1957,7 @@ canDecomposableFunTy ev eq_rel tys1 tys2
where
loc = ctEvLoc ev
role = eqRelRole eq_rel
- tc_roles = funRolesX role
- new_locs = [updateCtLocOrigin loc toInvisibleOrigin, loc, loc]
+ mult_loc = updateCtLocOrigin loc toInvisibleOrigin
-- | Call when canonicalizing an equality fails, but if the equality is
-- representational, there is some hope for the future.
=====================================
compiler/GHC/Tc/TyCl/Utils.hs
=====================================
@@ -146,7 +146,7 @@ synonymTyConsOfType ty
go_co (UnivCo p _ ty ty') = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
go_co (SymCo co) = go_co co
go_co (TransCo co co') = go_co co `plusNameEnv` go_co co'
- go_co (NthCo _ _ co) = go_co co
+ go_co (SelCo _ _ co) = go_co co
go_co (LRCo _ co) = go_co co
go_co (InstCo co co') = go_co co `plusNameEnv` go_co co'
go_co (KindCo co) = go_co co
=====================================
compiler/GHC/Tc/Types/Evidence.hs
=====================================
@@ -46,7 +46,7 @@ module GHC.Tc.Types.Evidence (
mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
mkTcSymCo, mkTcSymMCo,
mkTcTransCo,
- mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSymCo,
+ mkTcSelCo, mkTcLRCo, mkTcSubCo, maybeTcSymCo,
maybeTcSubCo, tcDowngradeRole,
mkTcAxiomRuleCo, mkTcGReflRightCo, mkTcGReflRightMCo, mkTcGReflLeftCo, mkTcGReflLeftMCo,
mkTcPhantomCo,
@@ -139,7 +139,7 @@ mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
-> [TcCoercion] -> TcCoercionR
mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
-mkTcNthCo :: Role -> Int -> TcCoercion -> TcCoercion
+mkTcSelCo :: Role -> CoSel -> TcCoercion -> TcCoercion
mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
mkTcSubCo :: HasDebugCallStack => TcCoercionN -> TcCoercionR
tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
@@ -177,7 +177,7 @@ mkTcAxInstCo = mkAxInstCo
mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational
mkTcForAllCo = mkForAllCo
mkTcForAllCos = mkForAllCos
-mkTcNthCo = mkNthCo
+mkTcSelCo = mkSelCo
mkTcLRCo = mkLRCo
mkTcSubCo = mkSubCo
tcDowngradeRole = downgradeRole
=====================================
compiler/GHC/Tc/Utils/TcMType.hs
=====================================
@@ -1515,7 +1515,7 @@ collect_cand_qtvs_co orig_ty bound = go_co
collect_cand_qtvs orig_ty True bound dv2 t2
go_co dv (SymCo co) = go_co dv co
go_co dv (TransCo co1 co2) = foldlM go_co dv [co1, co2]
- go_co dv (NthCo _ _ co) = go_co dv co
+ go_co dv (SelCo _ _ co) = go_co dv co
go_co dv (LRCo _ co) = go_co dv co
go_co dv (InstCo co1 co2) = foldlM go_co dv [co1, co2]
go_co dv (KindCo co) = go_co dv co
=====================================
compiler/GHC/Types/Basic.hs
=====================================
@@ -127,13 +127,11 @@ import qualified Data.Semigroup as Semi
import {-# SOURCE #-} Language.Haskell.Syntax.Type (PromotionFlag(..), isPromoted)
import Language.Haskell.Syntax.Basic (Boxity(..), isBoxed, ConTag)
-{-
-************************************************************************
+{- *********************************************************************
* *
Binary choice
* *
-************************************************************************
--}
+********************************************************************* -}
data LeftOrRight = CLeft | CRight
deriving( Eq, Data )
=====================================
compiler/GHC/Types/Literal.hs
=====================================
@@ -134,7 +134,8 @@ data Literal
| LitRubbish -- ^ A nonsense value; See Note [Rubbish literals].
TypeOrConstraint -- t_or_c: whether this is a type or a constraint
Type -- rr: a type of kind RuntimeRep
- -- The type of the literal is forall (a:SORT t_or_c rr). a
+ -- The type of the literal is forall (a:TYPE rr). a
+ -- or forall (a:CONSTRAINT rr). a
--
-- INVARIANT: the Type has no free variables
-- and so substitution etc can ignore it
=====================================
libraries/ghc-prim/GHC/Types.hs
=====================================
@@ -475,7 +475,7 @@ data RuntimeRep = VecRep VecCount VecElem -- ^ a SIMD vector type
-- RuntimeRep is intimately tied to TyCon.RuntimeRep (in GHC proper). See
-- Note [RuntimeRep and PrimRep] in RepType.
-- See also Note [Wiring in RuntimeRep] in GHC.Builtin.Types
--- See also Note [SORT, TYPE, and CONSTRAINT] in GHC.Builtin.Type.Prim
+-- See also Note [TYPE and CONSTRAINT] in GHC.Builtin.Type.Prim
-- | Length of a SIMD vector type
data VecCount = Vec2
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ac9c8ca6e81b88872d89e0781d6db0d7d735c302
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/ac9c8ca6e81b88872d89e0781d6db0d7d735c302
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20220815/9cbfaefb/attachment-0001.html>
More information about the ghc-commits
mailing list