Safe Haskell | None |
---|---|
Language | Haskell98 |
Coercion
Contents
Description
Module for (a) type kinds and (b) type coercions,
as used in System FC. See Expr
for
more on System FC and how coercions fit into it.
- data Coercion
- = Refl Role Type
- | TyConAppCo Role TyCon [Coercion]
- | AppCo Coercion Coercion
- | ForAllCo TyVar Coercion
- | CoVarCo CoVar
- | AxiomInstCo (CoAxiom Branched) BranchIndex [Coercion]
- | UnivCo Role Type Type
- | SymCo Coercion
- | TransCo Coercion Coercion
- | AxiomRuleCo CoAxiomRule [Type] [Coercion]
- | NthCo Int Coercion
- | LRCo LeftOrRight Coercion
- | InstCo Coercion Type
- | SubCo Coercion
- data Var
- type CoVar = Id
- data LeftOrRight
- pickLR :: LeftOrRight -> (a, a) -> a
- data Role
- ltRole :: Role -> Role -> Bool
- coVarKind :: CoVar -> (Type, Type)
- coVarRole :: CoVar -> Role
- coercionType :: Coercion -> Type
- coercionKind :: Coercion -> Pair Type
- coercionKinds :: [Coercion] -> Pair [Type]
- isReflCo :: Coercion -> Bool
- isReflCo_maybe :: Coercion -> Maybe Type
- coercionRole :: Coercion -> Role
- mkCoercionType :: Role -> Type -> Type -> Type
- mkReflCo :: Role -> Type -> Coercion
- mkCoVarCo :: CoVar -> Coercion
- mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> Coercion
- mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> Coercion
- mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
- mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
- mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> Type
- mkPiCo :: Role -> Var -> Coercion -> Coercion
- mkPiCos :: Role -> [Var] -> Coercion -> Coercion
- mkCoCast :: Coercion -> Coercion -> Coercion
- mkSymCo :: Coercion -> Coercion
- mkTransCo :: Coercion -> Coercion -> Coercion
- mkNthCo :: Int -> Coercion -> Coercion
- mkNthCoRole :: Role -> Int -> Coercion -> Coercion
- mkLRCo :: LeftOrRight -> Coercion -> Coercion
- mkInstCo :: Coercion -> Type -> Coercion
- mkAppCo :: Coercion -> Coercion -> Coercion
- mkAppCoFlexible :: Coercion -> Role -> Coercion -> Coercion
- mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
- mkFunCo :: Role -> Coercion -> Coercion -> Coercion
- mkForAllCo :: Var -> Coercion -> Coercion
- mkUnsafeCo :: Type -> Type -> Coercion
- mkUnivCo :: Role -> Type -> Type -> Coercion
- mkSubCo :: Coercion -> Coercion
- mkPhantomCo :: Coercion -> Coercion
- mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
- maybeSubCo :: Role -> Coercion -> Coercion
- maybeSubCo2 :: Role -> Role -> Coercion -> Coercion
- mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
- instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
- topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
- decomposeCo :: Arity -> Coercion -> [Coercion]
- getCoVar_maybe :: Coercion -> Maybe CoVar
- splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
- splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
- nthRole :: Role -> TyCon -> Int -> Role
- tyConRolesX :: Role -> TyCon -> [Role]
- nextRole :: Coercion -> Role
- 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
- mkCvSubst :: InScopeSet -> [(Var, Coercion)] -> CvSubst
- zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
- substTy :: CvSubst -> Type -> Type
- extendTvSubst :: CvSubst -> TyVar -> Type -> CvSubst
- extendCvSubstAndInScope :: CvSubst -> CoVar -> Coercion -> CvSubst
- extendTvSubstAndInScope :: CvSubst -> TyVar -> Type -> CvSubst
- substTyVarBndr :: CvSubst -> TyVar -> (CvSubst, TyVar)
- substCoVarBndr :: CvSubst -> CoVar -> (CvSubst, CoVar)
- liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
- liftCoSubstTyVar :: LiftCoSubst -> Role -> TyVar -> Maybe Coercion
- liftCoSubstWith :: Role -> [TyVar] -> [Coercion] -> Type -> Coercion
- coreEqCoercion :: Coercion -> Coercion -> Bool
- coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
- seqCo :: Coercion -> ()
- pprCo :: Coercion -> SDoc
- pprParendCo :: Coercion -> SDoc
- pprCoAxiom :: CoAxiom br -> SDoc
- pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
- pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
- tidyCo :: TidyEnv -> Coercion -> Coercion
- tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
- applyCo :: Type -> Coercion -> Type
Main data type
A Coercion
is concrete evidence of the equality/convertibility
of two types.
Constructors
data LeftOrRightSource
pickLR :: LeftOrRight -> (a, a) -> aSource
Constructors
Nominal | |
Representational | |
Phantom |
Functions over coercions
coercionType :: Coercion -> TypeSource
coercionKind :: Coercion -> Pair TypeSource
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]Source
Apply coercionKind
to multiple Coercion
s
coercionRole :: Coercion -> RoleSource
mkCoercionType :: Role -> Type -> Type -> TypeSource
Makes a coercion type from two types: the types whose equality
is proven by the relevant Coercion
Constructing coercions
mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> CoercionSource
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> CoercionSource
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> TypeSource
mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> TypeSource
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> TypeSource
mkSymCo :: Coercion -> CoercionSource
Create a symmetric version of the given Coercion
that asserts
equality between the same types but in the other "direction", so
a kind of t1 ~ t2
becomes the kind t2 ~ t1
.
mkLRCo :: LeftOrRight -> Coercion -> CoercionSource
mkTyConAppCo :: Role -> TyCon -> [Coercion] -> CoercionSource
Apply a type constructor to a list of coercions. It is the caller's responsibility to get the roles correct on argument coercions.
mkForAllCo :: Var -> Coercion -> CoercionSource
mkUnsafeCo :: Type -> Type -> CoercionSource
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.
mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom UnbranchedSource
maybeSubCo :: Role -> Coercion -> CoercionSource
mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> CoercionSource
Decomposition
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)Source
If co :: T ts ~ rep_ty
then:
instNewTyCon_maybe T ts = Just (rep_ty, co)
Checks for a newtype, and for being saturated
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)Source
Sometimes we want to look through a newtype
and get its associated coercion.
This function strips off newtype
layers enough to reveal something that isn't
a newtype
. Specifically, here's the invariant:
topNormaliseNewType_maybe rec_nts ty = Just (co, ty')
then (a) co : ty0 ~ ty'
.
(b) ty' is not a newtype.
The function returns Nothing
for non-newtypes
,
or unsaturated applications
This function does *not* look through type families, because it has no access to the type family environment. If you do have that at hand, consider to use topNormaliseType_maybe, which should be a drop-in replacement for topNormaliseNewType_maybe
decomposeCo :: Arity -> Coercion -> [Coercion]Source
getCoVar_maybe :: Coercion -> Maybe CoVarSource
Attempts to obtain the type variable underlying a Coercion
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)Source
Attempt to take a coercion application apart.
tyConRolesX :: Role -> TyCon -> [Role]Source
Coercion variables
isCoVarType :: Type -> BoolSource
setCoVarName :: CoVar -> Name -> CoVarSource
setCoVarUnique :: CoVar -> Unique -> CoVarSource
Free variables
tyCoVarsOfCo :: Coercion -> VarSetSource
tyCoVarsOfCos :: [Coercion] -> VarSetSource
coVarsOfCo :: Coercion -> VarSetSource
coercionSize :: Coercion -> IntSource
Substitution
type CvSubstEnv = VarEnv CoercionSource
isEmptyCvSubst :: CvSubst -> BoolSource
substCoVar :: CvSubst -> CoVar -> CoercionSource
substCoVars :: CvSubst -> [CoVar] -> [Coercion]Source
substCoWithTy :: InScopeSet -> TyVar -> Type -> Coercion -> CoercionSource
substCoWithTys :: InScopeSet -> [TyVar] -> [Type] -> Coercion -> CoercionSource
zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubstSource
Lifting
liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubstSource
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.
Comparison
coreEqCoercion :: Coercion -> Coercion -> BoolSource
Determines syntactic equality of coercions
Forcing evaluation of coercions
Pretty-printing
pprParendCo :: Coercion -> SDocSource
pprCoAxiom :: CoAxiom br -> SDocSource
pprCoAxBranch :: TyCon -> CoAxBranch -> SDocSource
pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDocSource