Module for (a) type kinds and (b) type coercions,
as used in System FC. See CoreSyn.Expr
for
more on System FC and how coercions fit into it.
Coercions are represented as types, and their kinds tell what types the coercion works on. The coercion kind constructor is a special TyCon that must always be saturated, like so:
typeKind (symCoercion type) :: TyConApp CoTyCon{...} [type, type]
- type Coercion = Type
- type Kind = Type
- typeKind :: Type -> Kind
- kindFunResult :: Kind -> Kind
- kindAppResult :: Kind -> [arg] -> Kind
- synTyConResKind :: TyCon -> Kind
- splitKindFunTys :: Kind -> ([Kind], Kind)
- splitKindFunTysN :: Int -> Kind -> ([Kind], Kind)
- splitKindFunTy_maybe :: Kind -> Maybe (Kind, Kind)
- isLiftedTypeKind :: Kind -> Bool
- isUnliftedTypeKind :: Kind -> Bool
- isOpenTypeKind :: Kind -> Bool
- isUbxTupleKind :: Kind -> Bool
- isArgTypeKind :: Kind -> Bool
- isKind :: Kind -> Bool
- isTySuperKind :: SuperKind -> Bool
- isCoSuperKind :: SuperKind -> Bool
- isSuperKind :: Type -> Bool
- isCoercionKind :: Kind -> Bool
- mkArrowKind :: Kind -> Kind -> Kind
- mkArrowKinds :: [Kind] -> Kind -> Kind
- isSubArgTypeKind :: Kind -> Bool
- isSubOpenTypeKind :: Kind -> Bool
- isSubKind :: Kind -> Kind -> Bool
- defaultKind :: Kind -> Kind
- eqKind :: Kind -> Kind -> Bool
- isSubKindCon :: TyCon -> TyCon -> Bool
- mkCoKind :: Type -> Type -> CoercionKind
- mkCoPredTy :: Type -> Type -> Type -> Type
- coVarKind :: CoVar -> (Type, Type)
- coVarKind_maybe :: CoVar -> Maybe (Type, Type)
- coercionKind :: Coercion -> (Type, Type)
- coercionKinds :: [Coercion] -> ([Type], [Type])
- isIdentityCoercion :: Coercion -> Bool
- isEqPred :: PredType -> Bool
- mkEqPred :: (Type, Type) -> PredType
- getEqPredTys :: PredType -> (Type, Type)
- isEqPredTy :: Type -> Bool
- mkCoercion :: TyCon -> [Type] -> Coercion
- mkSymCoercion :: Coercion -> Coercion
- mkTransCoercion :: Coercion -> Coercion -> Coercion
- mkLeftCoercion :: Coercion -> Coercion
- mkRightCoercion :: Coercion -> Coercion
- mkInstCoercion :: Coercion -> Type -> Coercion
- mkAppCoercion :: Coercion -> Coercion -> Coercion
- mkTyConCoercion :: TyCon -> [Coercion] -> Coercion
- mkFunCoercion :: Coercion -> Coercion -> Coercion
- mkForAllCoercion :: Var -> Coercion -> Coercion
- mkInstsCoercion :: Coercion -> [Type] -> Coercion
- mkUnsafeCoercion :: Type -> Type -> Coercion
- mkNewTypeCoercion :: Name -> TyCon -> [TyVar] -> Type -> TyCon
- mkFamInstCoercion :: Name -> [TyVar] -> TyCon -> [Type] -> TyCon -> TyCon
- mkAppsCoercion :: Coercion -> [Coercion] -> Coercion
- mkCsel1Coercion :: Coercion -> Coercion
- mkCsel2Coercion :: Coercion -> Coercion
- mkCselRCoercion :: Coercion -> Coercion
- mkClassPPredCo :: Class -> [Coercion] -> Coercion
- mkIParamPredCo :: IPName Name -> Coercion -> Coercion
- mkEqPredCo :: Coercion -> Coercion -> Coercion
- mkCoVarCoercion :: CoVar -> Coercion
- mkCoPredCo :: Coercion -> Coercion -> Coercion -> Coercion
- unsafeCoercionTyCon :: TyCon
- symCoercionTyCon :: TyCon
- transCoercionTyCon :: TyCon
- leftCoercionTyCon :: TyCon
- rightCoercionTyCon :: TyCon
- instCoercionTyCon :: TyCon
- csel1CoercionTyCon :: TyCon
- csel2CoercionTyCon :: TyCon
- cselRCoercionTyCon :: TyCon
- decompLR_maybe :: (Type, Type) -> Maybe ((Type, Type), (Type, Type))
- decompCsel_maybe :: (Type, Type) -> Maybe ((Type, Type), (Type, Type), (Type, Type))
- decompInst_maybe :: (Type, Type) -> Maybe ((TyVar, TyVar), (Type, Type))
- splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
- splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
- instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)
- decomposeCo :: Arity -> Coercion -> [Coercion]
- coreEqCoercion :: Coercion -> Coercion -> Bool
- coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
- data CoercionI
- isIdentityCoI :: CoercionI -> Bool
- mkSymCoI :: CoercionI -> CoercionI
- mkTransCoI :: CoercionI -> CoercionI -> CoercionI
- mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionI
- mkAppTyCoI :: CoercionI -> CoercionI -> CoercionI
- mkFunTyCoI :: CoercionI -> CoercionI -> CoercionI
- mkForAllTyCoI :: TyVar -> CoercionI -> CoercionI
- fromCoI :: CoercionI -> Type
- mkClassPPredCoI :: Class -> [CoercionI] -> CoercionI
- mkIParamPredCoI :: IPName Name -> CoercionI -> CoercionI
- mkEqPredCoI :: CoercionI -> CoercionI -> CoercionI
- mkCoPredCoI :: CoercionI -> CoercionI -> CoercionI -> CoercionI
Main data type
The key type representing kinds in the compiler. Invariant: a kind is always in one of these forms:
FunTy k1 k2 TyConApp PrimTyCon [...] TyVar kv -- (during inference only) ForAll ... -- (for top-level coercions)
Deconstructing Kinds
kindFunResult :: Kind -> KindSource
Essentially funResultTy
on kinds
kindAppResult :: Kind -> [arg] -> KindSource
synTyConResKind :: TyCon -> KindSource
splitKindFunTys :: Kind -> ([Kind], Kind)Source
Essentially splitFunTys
on kinds
splitKindFunTysN :: Int -> Kind -> ([Kind], Kind)Source
Essentially splitFunTysN
on kinds
Predicates on Kinds
isLiftedTypeKind :: Kind -> BoolSource
isUnliftedTypeKind :: Kind -> BoolSource
isUbxTupleKind :: Kind -> BoolSource
isArgTypeKind :: Kind -> BoolSource
isTySuperKind :: SuperKind -> BoolSource
isCoSuperKind :: SuperKind -> BoolSource
isSuperKind :: Type -> BoolSource
Is this a super-kind (i.e. a type-of-kinds)?
isCoercionKind :: Kind -> BoolSource
mkArrowKinds :: [Kind] -> Kind -> KindSource
Iterated application of mkArrowKind
isSubArgTypeKind :: Kind -> BoolSource
True of any sub-kind of ArgTypeKind
isSubOpenTypeKind :: Kind -> BoolSource
True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
defaultKind :: Kind -> KindSource
Used when generalising: default kind ? and ?? to *. See Type for more information on what that means
isSubKindCon :: TyCon -> TyCon -> BoolSource
kc1 `isSubKindCon` kc2
checks that kc1
<: kc2
mkCoKind :: Type -> Type -> CoercionKindSource
Makes a CoercionKind
from two types: the types whose equality
is proven by the relevant Coercion
coercionKind :: Coercion -> (Type, Type)Source
If it is the case that
c :: (t1 ~ t2)
i.e. the kind of c
is a CoercionKind
relating t1
and t2
,
then coercionKind c = (t1, t2)
.
coercionKinds :: [Coercion] -> ([Type], [Type])Source
Apply coercionKind
to multiple Coercion
s
Equality predicates
getEqPredTys :: PredType -> (Type, Type)Source
Splits apart a type equality predicate, if the supplied PredType
is one.
Panics otherwise
isEqPredTy :: Type -> BoolSource
Tests whether a type is just a type equality predicate
Coercion transformations
mkCoercion :: TyCon -> [Type] -> CoercionSource
mkTransCoercion :: Coercion -> Coercion -> CoercionSource
mkInstCoercion :: Coercion -> Type -> CoercionSource
mkAppCoercion :: Coercion -> Coercion -> CoercionSource
mkTyConCoercion :: TyCon -> [Coercion] -> CoercionSource
Apply a type constructor to a list of coercions.
mkFunCoercion :: Coercion -> Coercion -> CoercionSource
mkForAllCoercion :: Var -> Coercion -> CoercionSource
mkInstsCoercion :: Coercion -> [Type] -> CoercionSource
As mkInstCoercion
, but instantiates the coercion with a number of type arguments, left-to-right
mkUnsafeCoercion :: Type -> Type -> CoercionSource
Manufacture a coercion from this air. Needless to say, this is not usually safe,
but it is used when we know we are dealing with bottom, which is one case in which
it is safe. This is also used implement the unsafeCoerce#
primitive.
Optimise by pushing down through type constructors
:: Name | Unique name for the coercion tycon |
-> [TyVar] | Type parameters of the coercion ( |
-> TyCon | Family tycon ( |
-> [Type] | Type instance ( |
-> TyCon | Representation tycon ( |
-> TyCon | Coercion tycon ( |
Create a coercion identifying a data
, newtype
or type
representation type
and its family instance. It has the form Co tvs :: F ts ~ R tvs
, where Co
is
the coercion tycon built here, F
the family tycon and R
the (derived)
representation tycon.
mkAppsCoercion :: Coercion -> [Coercion] -> CoercionSource
Applies multiple Coercion
s to another Coercion
, from left to right.
See also mkAppCoercion
mkClassPPredCo :: Class -> [Coercion] -> CoercionSource
mkEqPredCo :: Coercion -> Coercion -> CoercionSource
transCoercionTyCon :: TyConSource
Coercion type constructors: avoid using these directly and instead use
the mk*Coercion
and split*Coercion
family of functions if possible.
Each coercion TyCon is built with the special CoercionTyCon record and carries its own kinding rule. Such CoercionTyCons must be fully applied by any TyConApp in which they are applied, however they may also be over applied (see example above) and the kinding function must deal with this.
Decomposition
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)Source
Sometimes we want to look through a newtype
and get its associated coercion.
This function only strips *one layer* of newtype
off, so the caller will usually call
itself recursively. Furthermore, this function should only be applied to types of kind *
,
hence the newtype is always saturated. If co : ty ~ ty'
then:
splitNewTypeRepCo_maybe ty = Just (ty', co)
The function returns Nothing
for non-newtypes
or fully-transparent newtype
s.
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, CoercionI)Source
If co :: T ts ~ rep_ty
then:
instNewTyCon_maybe T ts = Just (rep_ty, co)
decomposeCo :: Arity -> Coercion -> [Coercion]Source
Comparison
coreEqCoercion :: Coercion -> Coercion -> BoolSource
Determines syntactic equality of coercions
CoercionI
isIdentityCoI :: CoercionI -> BoolSource
mkSymCoI :: CoercionI -> CoercionISource
Smart constructor for sym
on CoercionI
, see also mkSymCoercion
mkTransCoI :: CoercionI -> CoercionI -> CoercionISource
Smart constructor for trans
on CoercionI
, see also mkTransCoercion
mkTyConAppCoI :: TyCon -> [CoercionI] -> CoercionISource
Smart constructor for type constructor application on CoercionI
, see also mkAppCoercion
mkAppTyCoI :: CoercionI -> CoercionI -> CoercionISource
Smart constructor for honest-to-god Coercion
application on CoercionI
, see also mkAppCoercion
mkFunTyCoI :: CoercionI -> CoercionI -> CoercionISource
mkForAllTyCoI :: TyVar -> CoercionI -> CoercionISource
Smart constructor for quantified Coercion
s on CoercionI
, see also mkForAllCoercion
mkClassPPredCoI :: Class -> [CoercionI] -> CoercionISource
mkIParamPredCoI :: IPName Name -> CoercionI -> CoercionISource
Smart constructor for implicit parameter Coercion
s on CoercionI
. Similar to mkClassPPredCoI
mkEqPredCoI :: CoercionI -> CoercionI -> CoercionISource
Smart constructor for type equality Coercion
s on CoercionI
. Similar to mkClassPPredCoI