Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 FastString 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
- coercionKindRole :: Coercion -> (Pair Type, 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 :: FastString -> Role -> Type -> Type -> Coercion
- mkSubCo :: Coercion -> Coercion
- mkPhantomCo :: Coercion -> Coercion
- mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
- downgradeRole :: Role -> Role -> Coercion -> Coercion
- mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
- instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
- type NormaliseStepper = RecTcChecker -> TyCon -> [Type] -> NormaliseStepResult
- data NormaliseStepResult
- composeSteppers :: NormaliseStepper -> NormaliseStepper -> NormaliseStepper
- modifyStepResultCo :: (Coercion -> Coercion) -> NormaliseStepResult -> NormaliseStepResult
- unwrapNewTypeStepper :: NormaliseStepper
- topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
- topNormaliseTypeX_maybe :: NormaliseStepper -> 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]
- setNominalRole_maybe :: Coercion -> Maybe 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
- 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
data Coercion
A Coercion
is concrete evidence of the equality/convertibility
of two types.
Constructors
Instances
data Var
data LeftOrRight
pickLR :: LeftOrRight -> (a, a) -> a
data Role
Constructors
Nominal | |
Representational | |
Phantom |
Functions over coercions
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
isReflCo_maybe :: Coercion -> Maybe Type
coercionRole :: Coercion -> Role
Retrieve the role from a coercion.
coercionKindRole :: Coercion -> (Pair Type, Role)
Get a coercion's kind and role. Why both at once? See Note [Computing a coercion kind and role]
mkCoercionType :: Role -> Type -> Type -> Type
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] -> Coercion
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> Coercion
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> Type
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> Type
mkSymCo :: Coercion -> Coercion
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
.
mkNthCoRole :: Role -> Int -> Coercion -> Coercion
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkAppCoFlexible :: Coercion -> Role -> Coercion -> Coercion
mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
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 -> Coercion
mkUnsafeCo :: Type -> Type -> Coercion
Manufacture an unsafe coercion from thin air.
Currently (May 14) this is used only to implement the
unsafeCoerce#
primitive. Optimise by pushing
down through type constructors.
mkPhantomCo :: Coercion -> Coercion
mkNewTypeCo :: Name -> TyCon -> [TyVar] -> [Role] -> Type -> CoAxiom Unbranched
downgradeRole :: Role -> Role -> Coercion -> Coercion
mkAxiomRuleCo :: CoAxiomRule -> [Type] -> [Coercion] -> Coercion
Decomposition
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
If co :: T ts ~ rep_ty
then:
instNewTyCon_maybe T ts = Just (rep_ty, co)
Checks for a newtype, and for being saturated
type NormaliseStepper = RecTcChecker -> TyCon -> [Type] -> NormaliseStepResult
A function to check if we can reduce a type by one step. Used
with topNormaliseTypeX_maybe
.
data NormaliseStepResult
The result of stepping in a normalisation function.
See topNormaliseTypeX_maybe
.
composeSteppers :: NormaliseStepper -> NormaliseStepper -> NormaliseStepper
Try one stepper and then try the next, if the first doesn't make progress.
modifyStepResultCo :: (Coercion -> Coercion) -> NormaliseStepResult -> NormaliseStepResult
unwrapNewTypeStepper :: NormaliseStepper
A NormaliseStepper
that unwraps newtypes, careful not to fall into
a loop. If it would fall into a loop, it produces NS_Abort
.
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
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
, or responds False to ok_tc. Specifically, here's the invariant:
topNormaliseNewType_maybe 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
topNormaliseTypeX_maybe :: NormaliseStepper -> Type -> Maybe (Coercion, Type)
A general function for normalising the top-level of a type. It continues
to use the provided NormaliseStepper
until that function fails, and then
this function returns. The roles of the coercions produced by the
NormaliseStepper
must all be the same, which is the role returned from
the call to topNormaliseTypeX_maybe
.
decomposeCo :: Arity -> Coercion -> [Coercion]
getCoVar_maybe :: Coercion -> Maybe CoVar
Attempts to obtain the type variable underlying a Coercion
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
Attempt to take a coercion application apart.
splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)
tyConRolesX :: Role -> TyCon -> [Role]
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
mkCvSubst :: InScopeSet -> [(Var, Coercion)] -> CvSubst
zipOpenCvSubst :: [Var] -> [Coercion] -> CvSubst
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)
Lifting
liftCoMatch :: TyVarSet -> Type -> Coercion -> Maybe LiftCoSubst
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.
liftCoSubstTyVar :: LiftCoSubst -> Role -> TyVar -> Maybe Coercion
Comparison
coreEqCoercion :: Coercion -> Coercion -> Bool
Determines syntactic equality of coercions
coreEqCoercion2 :: RnEnv2 -> Coercion -> Coercion -> Bool
Forcing evaluation of coercions
Pretty-printing
pprParendCo :: Coercion -> SDoc
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc