Coercion
Contents
Description
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.
- data Coercion
- data Var
- type CoVar = Id
- 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
- isUbxTupleKind, isUnliftedTypeKind, isArgTypeKind, isOpenTypeKind :: Kind -> Bool
- isKind :: Kind -> Bool
- isTySuperKind :: 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
- mkCoType :: Type -> Type -> Type
- coVarKind :: CoVar -> (Type, Type)
- coVarKind_maybe :: CoVar -> Maybe (Type, Type)
- coercionType :: Coercion -> Type
- coercionKind :: Coercion -> Pair Type
- coercionKinds :: [Coercion] -> Pair [Type]
- isReflCo :: Coercion -> Bool
- mkReflCo :: Type -> Coercion
- mkCoVarCo :: CoVar -> Coercion
- mkAxInstCo :: CoAxiom -> [Type] -> Coercion
- mkPiCo :: Var -> Coercion -> Coercion
- mkPiCos :: [Var] -> Coercion -> Coercion
- mkSymCo :: Coercion -> Coercion
- mkTransCo :: Coercion -> Coercion -> Coercion
- mkNthCo :: Int -> Coercion -> Coercion
- mkInstCo :: Coercion -> Type -> Coercion
- mkAppCo :: Coercion -> Coercion -> Coercion
- mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
- mkFunCo :: Coercion -> Coercion -> Coercion
- mkForAllCo :: Var -> Coercion -> Coercion
- mkUnsafeCo :: Type -> Type -> Coercion
- mkNewTypeCo :: Name -> TyCon -> [TyVar] -> Type -> CoAxiom
- mkFamInstCo :: Name -> [TyVar] -> TyCon -> [Type] -> TyCon -> CoAxiom
- mkPredCo :: Pred Coercion -> Coercion
- splitCoPredTy_maybe :: Type -> Maybe (Type, Type, Type)
- splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
- instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
- decomposeCo :: Arity -> Coercion -> [Coercion]
- getCoVar_maybe :: Coercion -> Maybe CoVar
- splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
- splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
- splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
- mkCoVar :: Name -> Type -> CoVar
- isCoVar :: Var -> Bool
- isCoVarType :: Type -> Bool
- coVarName :: CoVar -> Name
- setCoVarName :: CoVar -> Name -> CoVar
- setCoVarUnique :: CoVar -> Unique -> CoVar
- tyCoVarsOfCo :: Coercion -> VarSet
- tyCoVarsOfCos :: [Coercion] -> VarSet
- coVarsOfCo :: Coercion -> VarSet
- coercionSize :: Coercion -> Int
- type CvSubstEnv = VarEnv Coercion
- emptyCvSubstEnv :: CvSubstEnv
- data CvSubst = CvSubst InScopeSet TvSubstEnv CvSubstEnv
- emptyCvSubst :: CvSubst
- lookupTyVar :: CvSubst -> TyVar -> Maybe Type
- lookupCoVar :: CvSubst -> Var -> Maybe Coercion
- isEmptyCvSubst :: CvSubst -> Bool
- zapCvSubstEnv :: CvSubst -> CvSubst
- getCvInScope :: CvSubst -> InScopeSet
- substCo :: CvSubst -> Coercion -> Coercion
- substCos :: CvSubst -> [Coercion] -> [Coercion]
- substCoVar :: CvSubst -> CoVar -> Coercion
- substCoVars :: CvSubst -> [CoVar] -> [Coercion]
- substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
- substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
- cvTvSubst :: CvSubst -> TvSubst
- tvCvSubst :: TvSubst -> CvSubst
- zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
- substTy :: CvSubst -> Type -> Type
- extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
- substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
- substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
- liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe CvSubst
- liftCoSubst :: CvSubst -> Type -> Coercion
- liftCoSubstTyVar :: CvSubst -> TyVar -> Maybe Coercion
- liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
- coreEqCoercion :: Coercion -> Coercion -> Bool
- coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
- seqCo :: Coercion -> ()
- pprCo, pprParendCo :: Coercion -> SDoc
- pprCoAxiom :: CoAxiom -> SDoc
- applyCo :: Type -> Coercion -> Type
- coVarPred :: CoVar -> PredType
Main data type
data Coercion
A Coercion
is concrete evidence of the equality/convertibility
of two types.
data Var
Deconstructing Kinds
kindFunResult :: Kind -> Kind
Essentially funResultTy
on kinds
kindAppResult :: Kind -> [arg] -> Kind
synTyConResKind :: TyCon -> Kind
splitKindFunTys :: Kind -> ([Kind], Kind)
Essentially splitFunTys
on kinds
splitKindFunTysN :: Int -> Kind -> ([Kind], Kind)
Essentially splitFunTysN
on kinds
splitKindFunTy_maybe :: Kind -> Maybe (Kind, Kind)
Predicates on Kinds
isLiftedTypeKind :: Kind -> Bool
isTySuperKind :: SuperKind -> Bool
isSuperKind :: Type -> Bool
Is this a super-kind (i.e. a type-of-kinds)?
isCoercionKind :: Kind -> Bool
mkArrowKind :: Kind -> Kind -> Kind
Given two kinds k1
and k2
, creates the Kind
k1 -> k2
mkArrowKinds :: [Kind] -> Kind -> Kind
Iterated application of mkArrowKind
isSubArgTypeKind :: Kind -> Bool
True of any sub-kind of ArgTypeKind
isSubOpenTypeKind :: Kind -> Bool
True of any sub-kind of OpenTypeKind (i.e. anything except arrow)
defaultKind :: Kind -> Kind
Used when generalising: default kind ? and ?? to *. See Type for more information on what that means
isSubKindCon :: TyCon -> TyCon -> Bool
kc1 `isSubKindCon` kc2
checks that kc1
<: kc2
mkCoType :: Type -> Type -> Type
Makes a coercion type from two types: the types whose equality
is proven by the relevant Coercion
coVarKind_maybe :: CoVar -> Maybe (Type, Type)
coercionType :: Coercion -> Type
coercionKind :: Coercion -> Pair Type
If it is the case that
c :: (t1 ~ t2)
i.e. the kind of c
relates t1
and t2
, then coercionKind c = Pair t1 t2
.
coercionKinds :: [Coercion] -> Pair [Type]
Apply coercionKind
to multiple Coercion
s
Constructing coercions
mkAxInstCo :: CoAxiom -> [Type] -> Coercion
mkTyConAppCo :: TyCon -> [Coercion] -> Coercion
Apply a type constructor to a list of coercions.
mkForAllCo :: Var -> Coercion -> Coercion
mkUnsafeCo :: Type -> Type -> Coercion
Manufacture a coercion from thin 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
to implement the unsafeCoerce#
primitive. Optimise by pushing
down through type constructors.
Arguments
:: Name | Unique name for the coercion tycon |
-> [TyVar] | Type parameters of the coercion ( |
-> TyCon | Family tycon ( |
-> [Type] | Type instance ( |
-> TyCon | Representation tycon ( |
-> CoAxiom | Coercion constructor ( |
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 constructor built here, F
the family tycon and R
the (derived)
representation tycon.
Decomposition
splitNewTypeRepCo_maybe :: Type -> Maybe (Type, Coercion)
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, Coercion)
If co :: T ts ~ rep_ty
then:
instNewTyCon_maybe T ts = Just (rep_ty, co)
decomposeCo :: Arity -> Coercion -> [Coercion]
getCoVar_maybe :: Coercion -> Maybe CoVar
Attempts to obtain the type variable underlying a Coercion
splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
Attempts to tease a coercion apart into a type constructor and the application of a number of coercion arguments to that constructor
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
Attempt to take a coercion application apart.
splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
Coercion variables
isCoVarType :: Type -> Bool
setCoVarName :: CoVar -> Name -> CoVar
setCoVarUnique :: CoVar -> Unique -> CoVar
Free variables
tyCoVarsOfCo :: Coercion -> VarSet
tyCoVarsOfCos :: [Coercion] -> VarSet
coVarsOfCo :: Coercion -> VarSet
coercionSize :: Coercion -> Int
Substitution
type CvSubstEnv = VarEnv Coercion
lookupTyVar :: CvSubst -> TyVar -> Maybe Type
lookupCoVar :: CvSubst -> Var -> Maybe Coercion
isEmptyCvSubst :: CvSubst -> Bool
zapCvSubstEnv :: CvSubst -> CvSubst
getCvInScope :: CvSubst -> InScopeSet
substCoVar :: CvSubst -> CoVar -> Coercion
substCoVars :: CvSubst -> [CoVar] -> [Coercion]
substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> Coercion
substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> Coercion
zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
Lifting
liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe CvSubst
liftCoMatch
is sort of inverse to liftCoSubst
. In particular, if
liftCoMatch vars ty co == Just s
, then tyCoSubst s ty == co
.
That is, it matches a type against a coercion of the same
shape, and returns a lifting substitution which could have been
used to produce the given coercion from the given type.
liftCoSubst :: CvSubst -> Type -> Coercion
The "lifting" operation which substitutes coercions for type variables in a type to produce a coercion.
For the inverse operation, see liftCoMatch
liftCoSubstTyVar :: CvSubst -> TyVar -> Maybe Coercion
liftCoSubstWith :: [TyVar] -> [Coercion] -> Type -> Coercion
Comparison
coreEqCoercion :: Coercion -> Coercion -> Bool
Determines syntactic equality of coercions
coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
Forcing evaluation of coercions
Pretty-printing
pprCo, pprParendCo :: Coercion -> SDoc
pprCoAxiom :: CoAxiom -> SDoc