Safe Haskell | None |
---|---|
Language | GHC2021 |
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.
Synopsis
- data Coercion
- type CoercionN = Coercion
- type CoercionR = Coercion
- type CoercionP = Coercion
- data MCoercion
- type MCoercionN = MCoercion
- type MCoercionR = MCoercion
- data CoSel
- data FunSel
- data UnivCoProvenance
- data CoercionHole = CoercionHole {}
- coHoleCoVar :: CoercionHole -> CoVar
- setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole
- data LeftOrRight
- data Var
- type CoVar = Id
- type TyCoVar = Id
- data Role
- ltRole :: Role -> Role -> Bool
- coVarRType :: HasDebugCallStack => CoVar -> Type
- coVarLType :: HasDebugCallStack => CoVar -> Type
- coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
- coVarKind :: CoVar -> Type
- coVarTypesRole :: HasDebugCallStack => CoVar -> (Type, Type, Role)
- coVarRole :: CoVar -> Role
- coercionType :: Coercion -> Type
- mkCoercionType :: Role -> Type -> Type -> Type
- coercionKind :: HasDebugCallStack => Coercion -> Pair Type
- coercionLKind :: HasDebugCallStack => Coercion -> Type
- coercionRKind :: HasDebugCallStack => Coercion -> Type
- coercionKinds :: [Coercion] -> Pair [Type]
- coercionRole :: Coercion -> Role
- coercionKindRole :: Coercion -> (Pair Type, Role)
- mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
- mkGReflMCo :: HasDebugCallStack => Role -> Type -> CoercionN -> Coercion
- mkReflCo :: Role -> Type -> Coercion
- mkRepReflCo :: Type -> Coercion
- mkNomReflCo :: Type -> Coercion
- mkCoVarCo :: CoVar -> Coercion
- mkCoVarCos :: [CoVar] -> [Coercion]
- mkAxInstCo :: Role -> CoAxiomRule -> [Type] -> [Coercion] -> Coercion
- mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
- mkAxInstRHS :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
- mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
- mkAxInstLHS :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
- mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
- mkPiCo :: Role -> Var -> Coercion -> Coercion
- mkPiCos :: Role -> [Var] -> Coercion -> Coercion
- mkCoCast :: Coercion -> CoercionR -> Coercion
- mkSymCo :: Coercion -> Coercion
- mkTransCo :: HasDebugCallStack => Coercion -> Coercion -> Coercion
- mkSelCo :: HasDebugCallStack => CoSel -> Coercion -> Coercion
- mkSelCoResRole :: CoSel -> Role -> Role
- getNthFun :: FunSel -> a -> a -> a -> a
- selectFromType :: HasDebugCallStack => CoSel -> Type -> Type
- mkLRCo :: LeftOrRight -> Coercion -> Coercion
- mkInstCo :: Coercion -> CoercionN -> Coercion
- mkAppCo :: Coercion -> Coercion -> Coercion
- mkAppCos :: Coercion -> [Coercion] -> Coercion
- mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
- mkFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
- mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
- mkFunCoNoFTF :: HasDebugCallStack => Role -> CoercionN -> Coercion -> Coercion -> Coercion
- mkFunResCo :: Role -> Id -> Coercion -> Coercion
- mkNakedFunCo :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
- mkNakedForAllCo :: TyVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
- mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion
- mkHomoForAllCos :: [ForAllTyBinder] -> Coercion -> Coercion
- mkPhantomCo :: Coercion -> Type -> Type -> Coercion
- mkHoleCo :: CoercionHole -> Coercion
- mkUnivCo :: UnivCoProvenance -> [Coercion] -> Role -> Type -> Type -> Coercion
- mkSubCo :: HasDebugCallStack => Coercion -> Coercion
- mkProofIrrelCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion
- downgradeRole :: Role -> Role -> Coercion -> Coercion
- mkAxiomCo :: CoAxiomRule -> [Coercion] -> Coercion
- mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
- mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
- mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
- mkCoherenceRightCo :: HasDebugCallStack => Role -> Type -> CoercionN -> Coercion -> Coercion
- mkKindCo :: Coercion -> Coercion
- castCoercionKind :: Coercion -> CoercionN -> CoercionN -> Coercion
- castCoercionKind1 :: Coercion -> Role -> Type -> Type -> CoercionN -> Coercion
- castCoercionKind2 :: Coercion -> Role -> Type -> Type -> CoercionN -> CoercionN -> Coercion
- instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
- type NormaliseStepper ev = RecTcChecker -> TyCon -> [Type] -> NormaliseStepResult ev
- data NormaliseStepResult ev
- = NS_Done
- | NS_Abort
- | NS_Step RecTcChecker Type ev
- composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
- unwrapNewTypeStepper :: NormaliseStepper Coercion
- topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
- topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
- decomposeCo :: Arity -> Coercion -> Infinite Role -> [Coercion]
- decomposeFunCo :: HasDebugCallStack => Coercion -> (CoercionN, Coercion, Coercion)
- decomposePiCos :: HasDebugCallStack => CoercionN -> Pair Type -> [Type] -> ([CoercionN], CoercionN)
- getCoVar_maybe :: Coercion -> Maybe CoVar
- splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
- splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
- splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
- splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
- splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion)
- tyConRole :: Role -> TyCon -> Int -> Role
- tyConRolesX :: Role -> TyCon -> Infinite Role
- tyConRolesRepresentational :: TyCon -> Infinite Role
- setNominalRole_maybe :: Role -> Coercion -> Maybe CoercionN
- tyConRoleListX :: Role -> TyCon -> [Role]
- tyConRoleListRepresentational :: TyCon -> [Role]
- funRole :: Role -> FunSel -> Role
- pickLR :: LeftOrRight -> (a, a) -> a
- isGReflCo :: Coercion -> Bool
- isReflCo :: Coercion -> Bool
- isReflCo_maybe :: Coercion -> Maybe (Type, Role)
- isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
- isReflexiveCo :: Coercion -> Bool
- isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
- isReflCoVar_maybe :: Var -> Maybe Coercion
- isGReflMCo :: MCoercion -> Bool
- mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion
- mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion
- mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion
- coToMCo :: Coercion -> MCoercion
- mkTransMCo :: MCoercion -> MCoercion -> MCoercion
- mkTransMCoL :: MCoercion -> Coercion -> MCoercion
- mkTransMCoR :: Coercion -> MCoercion -> MCoercion
- mkCastTyMCo :: Type -> MCoercion -> Type
- mkSymMCo :: MCoercion -> MCoercion
- mkFunResMCo :: Id -> MCoercionR -> MCoercionR
- mkPiMCos :: [Var] -> MCoercion -> MCoercion
- isReflMCo :: MCoercion -> Bool
- checkReflexiveMCo :: MCoercion -> MCoercion
- mkCoVar :: Name -> Type -> CoVar
- isCoVar :: Var -> Bool
- coVarName :: CoVar -> Name
- setCoVarName :: CoVar -> Name -> CoVar
- setCoVarUnique :: CoVar -> Unique -> CoVar
- tyCoVarsOfCo :: Coercion -> TyCoVarSet
- tyCoVarsOfCos :: [Coercion] -> TyCoVarSet
- coVarsOfCo :: Coercion -> CoVarSet
- tyCoFVsOfCo :: Coercion -> FV
- tyCoFVsOfCos :: [Coercion] -> FV
- tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet
- coercionSize :: Coercion -> Int
- anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool
- type CvSubstEnv = CoVarEnv Coercion
- emptyCvSubstEnv :: CvSubstEnv
- lookupCoVar :: Subst -> Var -> Maybe Coercion
- substCo :: HasDebugCallStack => Subst -> Coercion -> Coercion
- substCos :: HasDebugCallStack => Subst -> [Coercion] -> [Coercion]
- substCoVar :: Subst -> CoVar -> Coercion
- substCoVars :: Subst -> [CoVar] -> [Coercion]
- substCoWith :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
- substCoVarBndr :: HasDebugCallStack => Subst -> CoVar -> (Subst, CoVar)
- extendTvSubstAndInScope :: Subst -> TyVar -> Type -> Subst
- getCvSubstEnv :: Subst -> CvSubstEnv
- liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
- liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion
- liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
- liftCoSubstWithEx :: Role -> [TyVar] -> [Coercion] -> [TyCoVar] -> [Type] -> (Type -> Coercion, [Type])
- emptyLiftingContext :: InScopeSet -> LiftingContext
- extendLiftingContext :: LiftingContext -> TyCoVar -> Coercion -> LiftingContext
- extendLiftingContextAndInScope :: LiftingContext -> TyCoVar -> Coercion -> LiftingContext
- liftCoSubstVarBndrUsing :: (r -> CoercionN) -> (LiftingContext -> Type -> r) -> LiftingContext -> TyCoVar -> (LiftingContext, TyCoVar, r)
- isMappedByLC :: TyCoVar -> LiftingContext -> Bool
- extendLiftingContextCvSubst :: LiftingContext -> CoVar -> Coercion -> LiftingContext
- mkSubstLiftingContext :: Subst -> LiftingContext
- liftingContextSubst :: LiftingContext -> Subst
- zapLiftingContext :: LiftingContext -> LiftingContext
- substForAllCoBndrUsingLC :: SwapFlag -> (Coercion -> Coercion) -> LiftingContext -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
- lcLookupCoVar :: LiftingContext -> CoVar -> Maybe Coercion
- lcInScopeSet :: LiftingContext -> InScopeSet
- type LiftCoEnv = VarEnv Coercion
- data LiftingContext = LC Subst LiftCoEnv
- liftEnvSubstLeft :: Subst -> LiftCoEnv -> Subst
- liftEnvSubstRight :: Subst -> LiftCoEnv -> Subst
- substRightCo :: LiftingContext -> Coercion -> Coercion
- substLeftCo :: LiftingContext -> Coercion -> Coercion
- swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
- lcSubstLeft :: LiftingContext -> Subst
- lcSubstRight :: LiftingContext -> Subst
- eqCoercion :: Coercion -> Coercion -> Bool
- eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
- seqCo :: Coercion -> ()
- pprCo :: Coercion -> SDoc
- pprParendCo :: Coercion -> SDoc
- pprCoAxiom :: forall (br :: BranchFlag). CoAxiom br -> SDoc
- pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
- pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
- pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
- tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
- etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type)
- tidyCo :: TidyEnv -> Coercion -> Coercion
- tidyCos :: TidyEnv -> [Coercion] -> [Coercion]
- promoteCoercion :: HasDebugCallStack => Coercion -> CoercionN
- buildCoercion :: HasDebugCallStack => Type -> Type -> CoercionN
- multToCo :: Mult -> Coercion
- mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
- hasCoercionHoleTy :: Type -> Bool
- hasCoercionHoleCo :: Coercion -> Bool
- hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool
- setCoHoleType :: CoercionHole -> Type -> CoercionHole
Main data type
A Coercion
is concrete evidence of the equality/convertibility
of two types.
Instances
Outputable Coercion Source # | |
Data Coercion Source # | |
Defined in GHC.Core.TyCo.Rep gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Coercion -> c Coercion # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Coercion # toConstr :: Coercion -> Constr # dataTypeOf :: Coercion -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Coercion) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Coercion) # gmapT :: (forall b. Data b => b -> b) -> Coercion -> Coercion # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Coercion -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Coercion -> r # gmapQ :: (forall d. Data d => d -> u) -> Coercion -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion # | |
Eq (DeBruijn Coercion) Source # | |
A semantically more meaningful type to represent what may or may not be a
useful Coercion
.
Instances
Outputable MCoercion Source # | |
Data MCoercion Source # | |
Defined in GHC.Core.TyCo.Rep gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MCoercion -> c MCoercion # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MCoercion # toConstr :: MCoercion -> Constr # dataTypeOf :: MCoercion -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MCoercion) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercion) # gmapT :: (forall b. Data b => b -> b) -> MCoercion -> MCoercion # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MCoercion -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MCoercion -> r # gmapQ :: (forall d. Data d => d -> u) -> MCoercion -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> MCoercion -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion # |
type MCoercionN = MCoercion Source #
type MCoercionR = MCoercion Source #
Instances
NFData CoSel Source # | |
Defined in GHC.Core.TyCo.Rep | |
Binary CoSel Source # | |
Outputable CoSel Source # | |
Data CoSel Source # | |
Defined in GHC.Core.TyCo.Rep gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoSel -> c CoSel # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoSel # dataTypeOf :: CoSel -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoSel) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoSel) # gmapT :: (forall b. Data b => b -> b) -> CoSel -> CoSel # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoSel -> r # gmapQ :: (forall d. Data d => d -> u) -> CoSel -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CoSel -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoSel -> m CoSel # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoSel -> m CoSel # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoSel -> m CoSel # | |
Eq CoSel Source # | |
Ord CoSel Source # | |
Instances
Outputable FunSel Source # | |
Data FunSel Source # | |
Defined in GHC.Core.TyCo.Rep gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> FunSel -> c FunSel # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c FunSel # toConstr :: FunSel -> Constr # dataTypeOf :: FunSel -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c FunSel) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c FunSel) # gmapT :: (forall b. Data b => b -> b) -> FunSel -> FunSel # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> FunSel -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> FunSel -> r # gmapQ :: (forall d. Data d => d -> u) -> FunSel -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> FunSel -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> FunSel -> m FunSel # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> FunSel -> m FunSel # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> FunSel -> m FunSel # | |
Eq FunSel Source # | |
Ord FunSel Source # | |
data UnivCoProvenance Source #
For simplicity, we have just one UnivCo that represents a coercion from
some type to some other type, with (in general) no restrictions on the
type. The UnivCoProvenance specifies more exactly what the coercion really
is and why a program should (or shouldn't!) trust the coercion.
It is reasonable to consider each constructor of UnivCoProvenance
as a totally independent coercion form; their only commonality is
that they don't tell you what types they coercion between. (That info
is in the UnivCo
constructor of Coercion
.
Instances
data CoercionHole Source #
A coercion to be filled in by the type-checker. See Note [Coercion holes]
Instances
Uniquable CoercionHole Source # | |
Defined in GHC.Core.TyCo.Rep getUnique :: CoercionHole -> Unique Source # | |
Outputable CoercionHole Source # | |
Defined in GHC.Core.TyCo.Rep ppr :: CoercionHole -> SDoc Source # | |
Data CoercionHole Source # | |
Defined in GHC.Core.TyCo.Rep gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoercionHole -> c CoercionHole # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoercionHole # toConstr :: CoercionHole -> Constr # dataTypeOf :: CoercionHole -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoercionHole) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoercionHole) # gmapT :: (forall b. Data b => b -> b) -> CoercionHole -> CoercionHole # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r # gmapQ :: (forall d. Data d => d -> u) -> CoercionHole -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CoercionHole -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole # |
coHoleCoVar :: CoercionHole -> CoVar Source #
setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole Source #
data LeftOrRight Source #
Instances
Variable
Essentially a typed Name
, that may also contain some additional information
about the Var
and its use sites.
Instances
NamedThing Var Source # | |
HasOccName Var Source # | |
Uniquable Var Source # | |
Outputable Var Source # | |
OutputableBndr Var Source # | |
Defined in GHC.Core.Ppr pprBndr :: BindingSite -> Var -> SDoc Source # pprPrefixOcc :: Var -> SDoc Source # pprInfixOcc :: Var -> SDoc Source # bndrIsJoin_maybe :: Var -> JoinPointHood Source # | |
Data Var Source # | |
Defined in GHC.Types.Var gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var -> c Var # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Var # dataTypeOf :: Var -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Var) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var) # gmapT :: (forall b. Data b => b -> b) -> Var -> Var # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r # gmapQ :: (forall d. Data d => d -> u) -> Var -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Var -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var -> m Var # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var # | |
Eq Var Source # | |
Ord Var Source # | |
Eq (DeBruijn CoreAlt) Source # | |
Eq (DeBruijn CoreExpr) Source # | |
Eq (DeBruijn Var) Source # | |
OutputableBndr (Id, TagSig) Source # | |
Defined in GHC.Stg.EnforceEpt.TagSig pprBndr :: BindingSite -> (Id, TagSig) -> SDoc Source # pprPrefixOcc :: (Id, TagSig) -> SDoc Source # pprInfixOcc :: (Id, TagSig) -> SDoc Source # bndrIsJoin_maybe :: (Id, TagSig) -> JoinPointHood Source # | |
type Anno Id Source # | |
Defined in GHC.Hs.Extension |
See Note [Roles] in GHC.Core.Coercion
Order of constructors matters: the Ord instance coincides with the *super*typing relation on roles.
Instances
Binary Role Source # | |
Outputable Role Source # | |
Data Role Source # | |
Defined in Language.Haskell.Syntax.Basic gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role # dataTypeOf :: Role -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) # gmapT :: (forall b. Data b => b -> b) -> Role -> Role # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r # gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role # | |
Eq Role Source # | |
Ord Role Source # | |
type Anno (Maybe Role) Source # | |
Defined in GHC.Hs.Decls |
Functions over coercions
coVarRType :: HasDebugCallStack => CoVar -> Type Source #
coVarLType :: HasDebugCallStack => CoVar -> Type Source #
coVarTypes :: HasDebugCallStack => CoVar -> Pair Type Source #
coVarTypesRole :: HasDebugCallStack => CoVar -> (Type, Type, Role) Source #
coercionType :: Coercion -> Type Source #
mkCoercionType :: Role -> Type -> Type -> Type Source #
Makes a coercion type from two types: the types whose equality
is proven by the relevant Coercion
coercionKind :: HasDebugCallStack => Coercion -> Pair Type Source #
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
.
coercionLKind :: HasDebugCallStack => Coercion -> Type Source #
coercionRKind :: HasDebugCallStack => Coercion -> Type Source #
coercionKinds :: [Coercion] -> Pair [Type] Source #
Apply coercionKind
to multiple Coercion
s
coercionRole :: Coercion -> Role Source #
Retrieve the role from a coercion.
Constructing coercions
mkGReflMCo :: HasDebugCallStack => Role -> Type -> CoercionN -> Coercion Source #
mkRepReflCo :: Type -> Coercion Source #
Make a representational reflexive coercion
mkNomReflCo :: Type -> Coercion Source #
Make a nominal reflexive coercion
mkCoVarCos :: [CoVar] -> [Coercion] Source #
mkAxInstCo :: Role -> CoAxiomRule -> [Type] -> [Coercion] -> Coercion Source #
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion Source #
mkAxInstRHS :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type Source #
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type Source #
mkAxInstLHS :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type Source #
Return the left-hand type of the axiom, when the axiom is instantiated at the types given.
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type Source #
Instantiate the left-hand side of an unbranched axiom
mkPiCo :: Role -> Var -> Coercion -> Coercion Source #
Make a forall Coercion
, where both types related by the coercion
are quantified over the same variable.
mkSymCo :: Coercion -> Coercion Source #
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
.
:: FunSel | |
-> a | multiplicity |
-> a | argument |
-> a | result |
-> a | One of the above three |
Extract the nth field of a FunCo
selectFromType :: HasDebugCallStack => CoSel -> Type -> Type Source #
mkInstCo :: Coercion -> CoercionN -> Coercion Source #
Instantiates a Coercion
.
Works for both tyvar and covar
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion Source #
Apply a type constructor to a list of coercions. It is the caller's responsibility to get the roles correct on argument coercions.
mkFunCo2 :: Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion Source #
mkFunCoNoFTF :: HasDebugCallStack => Role -> CoercionN -> Coercion -> Coercion -> Coercion Source #
mkNakedForAllCo :: TyVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion Source #
mkForAllCo :: HasDebugCallStack => TyCoVar -> ForAllTyFlag -> ForAllTyFlag -> CoercionN -> Coercion -> Coercion Source #
Make a Coercion from a tycovar, a kind coercion, and a body coercion.
mkHomoForAllCos :: [ForAllTyBinder] -> Coercion -> Coercion Source #
Make a Coercion quantified over a type/coercion variable; the variable has the same kind and visibility in both sides of the coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion Source #
Make a phantom coercion between two types. The coercion passed in must be a nominal coercion between the kinds of the types.
mkHoleCo :: CoercionHole -> Coercion Source #
Make a coercion from a coercion hole
:: UnivCoProvenance | |
-> [Coercion] | Coercions on which this depends |
-> Role | role of the built coercion, "r" |
-> Type | t1 :: k1 |
-> Type | t2 :: k2 |
-> Coercion | :: t1 ~r t2 |
Make a universal coercion between two arbitrary types.
:: Role | role of the created coercion, "r" |
-> CoercionN | :: phi1 ~N phi2 |
-> Coercion | g1 :: phi1 |
-> Coercion | g2 :: phi2 |
-> Coercion | :: g1 ~r g2 |
Make a "coercion between coercions".
downgradeRole :: Role -> Role -> Coercion -> Coercion Source #
Like downgradeRole_maybe
, but panics if the change isn't a downgrade.
See Note [Role twiddling functions]
mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion Source #
Given ty :: k1
, co :: k1 ~ k2
,
produces co' :: ty ~r (ty |> co)
mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion Source #
Given r
, ty :: k1
, and co :: k1 ~N k2
,
produces co' :: (ty |> co) ~r ty
mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion Source #
Given ty :: k1
, co :: k1 ~ k2
, co2:: ty ~r ty'
,
produces @co' :: (ty |> co) ~r ty'
It is not only a utility function, but it saves allocation when co
is a GRefl coercion.
mkCoherenceRightCo :: HasDebugCallStack => Role -> Type -> CoercionN -> Coercion -> Coercion Source #
Given ty :: k1
, co :: k1 ~ k2
, co2:: ty' ~r ty
,
produces @co' :: ty' ~r (ty |> co)
It is not only a utility function, but it saves allocation when co
is a GRefl coercion.
castCoercionKind :: Coercion -> CoercionN -> CoercionN -> Coercion Source #
Creates a new coercion with both of its types casted by different casts
castCoercionKind g h1 h2
, where g :: t1 ~r t2
,
has type (t1 |> h1) ~r (t2 |> h2)
.
h1
and h2
must be nominal.
It calls coercionKindRole
, so it's quite inefficient (which I
stands for)
Use castCoercionKind2
instead if t1
, t2
, and r
are known beforehand.
castCoercionKind1 :: Coercion -> Role -> Type -> Type -> CoercionN -> Coercion Source #
castCoercionKind1 g r t1 t2 h
= coercionKind g r t1 t2 h h
That is, it's a specialised form of castCoercionKind, where the two
kind coercions are identical
castCoercionKind1 g r t1 t2 h
, where g :: t1 ~r t2
,
has type (t1 |> h) ~r (t2 |> h)
.
h
must be nominal.
See Note [castCoercionKind1]
castCoercionKind2 :: Coercion -> Role -> Type -> Type -> CoercionN -> CoercionN -> Coercion Source #
Creates a new coercion with both of its types casted by different casts
castCoercionKind2 g r t1 t2 h1 h2
, where g :: t1 ~r t2
,
has type (t1 |> h1) ~r (t2 |> h2)
.
h1
and h2
must be nominal.
Decomposition
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion) Source #
If `instNewTyCon_maybe T ts = Just (rep_ty, co)` then `co :: T ts ~R# rep_ty`
Checks for a newtype, and for being saturated
type NormaliseStepper ev = RecTcChecker -> TyCon -> [Type] -> NormaliseStepResult ev Source #
A function to check if we can reduce a type by one step. Used
with topNormaliseTypeX
.
data NormaliseStepResult ev Source #
The result of stepping in a normalisation function.
See topNormaliseTypeX
.
NS_Done | Nothing more to do |
NS_Abort | Utter failure. The outer function should fail too. |
NS_Step RecTcChecker Type ev | We stepped, yielding new bits; ^ ev is evidence; Usually a co :: old type ~ new type |
Instances
Functor NormaliseStepResult Source # | |
Defined in GHC.Core.Coercion fmap :: (a -> b) -> NormaliseStepResult a -> NormaliseStepResult b # (<$) :: a -> NormaliseStepResult b -> NormaliseStepResult a # | |
Outputable ev => Outputable (NormaliseStepResult ev) Source # | |
Defined in GHC.Core.Coercion ppr :: NormaliseStepResult ev -> SDoc Source # |
composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev Source #
Try one stepper and then try the next, if the first doesn't make progress. So if it returns NS_Done, it means that both steppers are satisfied
unwrapNewTypeStepper :: NormaliseStepper Coercion Source #
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) 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 : ty ~R 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 If topNormliseNewType_maybe ty = Just (co, ty'), then co : ty ~R ty'
topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type) Source #
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
.
Typically ev is Coercion.
If topNormaliseTypeX step plus ty = Just (ev, ty')
then ty ~ev1~ t1 ~ev2~ t2 ... ~evn~ ty'
and ev = ev1 plus
ev2 plus
... plus
evn
If it returns Nothing then no newtype unwrapping could happen
decomposeFunCo :: HasDebugCallStack => Coercion -> (CoercionN, Coercion, Coercion) Source #
decomposePiCos :: HasDebugCallStack => CoercionN -> Pair Type -> [Type] -> ([CoercionN], CoercionN) Source #
getCoVar_maybe :: Coercion -> Maybe CoVar Source #
Extract a covar, if possible. This check is dirty. Be ashamed of yourself. (It's dirty because it cares about the structure of a coercion, which is morally reprehensible.)
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion) Source #
Attempt to take a coercion application apart.
splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion) Source #
splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion) Source #
Like splitForAllCo_maybe
, but only returns Just for tyvar binder
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, ForAllTyFlag, ForAllTyFlag, Coercion, Coercion) Source #
Like splitForAllCo_maybe
, but only returns Just for covar binder
setNominalRole_maybe :: Role -> Coercion -> Maybe CoercionN Source #
Converts a coercion to be nominal, if possible. See Note [Role twiddling functions]
tyConRoleListRepresentational :: TyCon -> [Role] Source #
pickLR :: LeftOrRight -> (a, a) -> a Source #
isGReflCo :: Coercion -> Bool Source #
Tests if this coercion is obviously a generalized reflexive coercion. Guaranteed to work very quickly.
isReflCo :: Coercion -> Bool Source #
Tests if this coercion is obviously reflexive. Guaranteed to work
very quickly. Sometimes a coercion can be reflexive, but not obviously
so. c.f. isReflexiveCo
isReflCo_maybe :: Coercion -> Maybe (Type, Role) Source #
Returns the type coerced if this coercion is reflexive. Guaranteed
to work very quickly. Sometimes a coercion can be reflexive, but not
obviously so. c.f. isReflexiveCo_maybe
isGReflCo_maybe :: Coercion -> Maybe (Type, Role) Source #
Returns the type coerced if this coercion is a generalized reflexive coercion. Guaranteed to work very quickly.
isReflexiveCo :: Coercion -> Bool Source #
Slowly checks if the coercion is reflexive. Don't call this in a loop, as it walks over the entire coercion.
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role) Source #
Extracts the coerced type from a reflexive coercion. This potentially walks over the entire coercion, so avoid doing this in a loop.
isGReflMCo :: MCoercion -> Bool Source #
Tests if this MCoercion is obviously generalized reflexive Guaranteed to work very quickly.
mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion Source #
mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion Source #
mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion Source #
Like mkCoherenceRightCo
, but with an MCoercion
mkFunResMCo :: Id -> MCoercionR -> MCoercionR Source #
Coercion variables
isCoVar :: Var -> Bool Source #
Is this a coercion variable?
Satisfies
.isId
v ==> isCoVar
v == not (isNonCoVarId
v)
Free variables
tyCoVarsOfCo :: Coercion -> TyCoVarSet Source #
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet Source #
coVarsOfCo :: Coercion -> CoVarSet Source #
tyCoFVsOfCo :: Coercion -> FV Source #
tyCoFVsOfCos :: [Coercion] -> FV Source #
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet Source #
Get a deterministic set of the vars free in a coercion
coercionSize :: Coercion -> Int Source #
Substitution
substCo :: HasDebugCallStack => Subst -> Coercion -> Coercion Source #
Substitute within a Coercion
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
substCos :: HasDebugCallStack => Subst -> [Coercion] -> [Coercion] Source #
Substitute within several Coercion
s
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
substCoWith :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion Source #
Coercion substitution, see zipTvSubst
substCoVarBndr :: HasDebugCallStack => Subst -> CoVar -> (Subst, CoVar) Source #
getCvSubstEnv :: Subst -> CvSubstEnv Source #
Lifting
liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion Source #
liftCoSubst role lc ty
produces a coercion (at role role
)
that coerces between lc_left(ty)
and lc_right(ty)
, where
lc_left
is a substitution mapping type variables to the left-hand
types of the mapped coercions in lc
, and similar for lc_right
.
liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion Source #
liftCoSubstWithEx :: Role -> [TyVar] -> [Coercion] -> [TyCoVar] -> [Type] -> (Type -> Coercion, [Type]) Source #
:: LiftingContext | original LC |
-> TyCoVar | new variable to map... |
-> Coercion | ...to this lifted version |
-> LiftingContext |
Extend a lifting context with a new mapping.
extendLiftingContextAndInScope Source #
:: LiftingContext | Original LC |
-> TyCoVar | new variable to map... |
-> Coercion | to this coercion |
-> LiftingContext |
Extend a lifting context with a new mapping, and extend the in-scope set
liftCoSubstVarBndrUsing Source #
:: (r -> CoercionN) | coercion getter |
-> (LiftingContext -> Type -> r) | callback |
-> LiftingContext | |
-> TyCoVar | |
-> (LiftingContext, TyCoVar, r) |
isMappedByLC :: TyCoVar -> LiftingContext -> Bool Source #
Is a var in the domain of a lifting context?
extendLiftingContextCvSubst :: LiftingContext -> CoVar -> Coercion -> LiftingContext Source #
Extend the substitution component of a lifting context with a new binding for a coercion variable. Used during coercion optimisation.
zapLiftingContext :: LiftingContext -> LiftingContext Source #
Erase the environments in a lifting context
substForAllCoBndrUsingLC :: SwapFlag -> (Coercion -> Coercion) -> LiftingContext -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion) Source #
Like substForAllCoBndr
, but works on a lifting context
lcLookupCoVar :: LiftingContext -> CoVar -> Maybe Coercion Source #
Lookup a CoVar
in the substitution in a LiftingContext
lcInScopeSet :: LiftingContext -> InScopeSet Source #
Get the InScopeSet
from a LiftingContext
data LiftingContext Source #
Instances
Outputable LiftingContext Source # | |
Defined in GHC.Core.Coercion ppr :: LiftingContext -> SDoc Source # |
substRightCo :: LiftingContext -> Coercion -> Coercion Source #
substLeftCo :: LiftingContext -> Coercion -> Coercion Source #
lcSubstLeft :: LiftingContext -> Subst Source #
lcSubstRight :: LiftingContext -> Subst Source #
Comparison
eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool Source #
Compare two Coercion
s, with respect to an RnEnv2
Forcing evaluation of coercions
Pretty-printing
pprParendCo :: Coercion -> SDoc Source #
pprCoAxiom :: forall (br :: BranchFlag). CoAxiom br -> SDoc Source #
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc Source #
pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc Source #
pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc Source #
etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type) Source #
Tidying
tidyCo :: TidyEnv -> Coercion -> Coercion Source #
Tidy a Coercion
See Note [Strictness in tidyType and friends]
Other
promoteCoercion :: HasDebugCallStack => Coercion -> CoercionN Source #
like mkKindCo, but aggressively & recursively optimizes to avoid using a KindCo constructor. The output role is nominal.
buildCoercion :: HasDebugCallStack => Type -> Type -> CoercionN Source #
Assuming that two types are the same, ignoring coercions, find a nominal coercion between the types. This is useful when optimizing transitivity over coercion applications, where splitting two AppCos might yield different kinds. See Note [EtaAppCo] in GHC.Core.Coercion.Opt.
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion Source #
Given a coercion `co :: (t1 :: TYPE r1) ~ (t2 :: TYPE r2)` produce a coercion `rep_co :: r1 ~ r2` But actually it is possible that co :: (t1 :: CONSTRAINT r1) ~ (t2 :: CONSTRAINT r2) or co :: (t1 :: TYPE r1) ~ (t2 :: CONSTRAINT r2) or co :: (t1 :: CONSTRAINT r1) ~ (t2 :: TYPE r2) See Note [mkRuntimeRepCo]
hasCoercionHoleTy :: Type -> Bool Source #
Is there a hetero-kind coercion hole in this type? (That is, a coercion hole with ch_hetero_kind=True.) See wrinkle (EIK2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
hasCoercionHoleCo :: Coercion -> Bool Source #
Is there a hetero-kind coercion hole in this coercion?
hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool Source #
setCoHoleType :: CoercionHole -> Type -> CoercionHole Source #
Set the type of a CoercionHole