Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
GHC.Core.Coercion
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.
Synopsis
- data Coercion
- type CoercionN = Coercion
- type CoercionR = Coercion
- type CoercionP = Coercion
- data MCoercion
- type MCoercionN = MCoercion
- type MCoercionR = MCoercion
- 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
- coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
- coVarKind :: CoVar -> Type
- coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role)
- coVarRole :: CoVar -> Role
- coercionType :: Coercion -> Type
- mkCoercionType :: Role -> Type -> Type -> Type
- coercionKind :: Coercion -> Pair Type
- coercionLKind :: Coercion -> Type
- coercionRKind :: Coercion -> Type
- coercionKinds :: [Coercion] -> Pair [Type]
- coercionRole :: Coercion -> Role
- coercionKindRole :: Coercion -> (Pair Type, Role)
- mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
- mkReflCo :: Role -> Type -> Coercion
- mkRepReflCo :: Type -> Coercion
- mkNomReflCo :: Type -> Coercion
- mkCoVarCo :: CoVar -> Coercion
- mkCoVarCos :: [CoVar] -> [Coercion]
- mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Coercion
- mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
- mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
- mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
- mkAxInstLHS :: 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 :: Coercion -> Coercion -> Coercion
- mkNthCo :: HasDebugCallStack => Role -> Int -> Coercion -> Coercion
- mkNthCoFunCo :: Int -> CoercionN -> Coercion -> Coercion -> Coercion
- nthCoRole :: Int -> Coercion -> Role
- mkLRCo :: LeftOrRight -> Coercion -> Coercion
- mkInstCo :: Coercion -> Coercion -> Coercion
- mkAppCo :: Coercion -> Coercion -> Coercion
- mkAppCos :: Coercion -> [Coercion] -> Coercion
- mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
- mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion
- mkFunResCo :: Role -> Scaled Type -> Coercion -> Coercion
- mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
- mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
- mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
- mkPhantomCo :: Coercion -> Type -> Type -> Coercion
- mkHoleCo :: CoercionHole -> Coercion
- mkUnivCo :: UnivCoProvenance -> Role -> Type -> Type -> Coercion
- mkSubCo :: HasDebugCallStack => Coercion -> Coercion
- mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
- mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
- downgradeRole :: Role -> Role -> Coercion -> Coercion
- mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
- mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
- mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
- mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
- mkCoherenceRightCo :: 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
- mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN
- mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
- mkPrimEqPred :: Type -> Type -> Type
- mkReprPrimEqPred :: Type -> Type -> Type
- mkPrimEqPredRole :: Role -> Type -> Type -> PredType
- mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
- mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
- 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
- mapStepResult :: (ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
- unwrapNewTypeStepper :: NormaliseStepper Coercion
- topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
- topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
- decomposeCo :: Arity -> Coercion -> [Role] -> [Coercion]
- decomposeFunCo :: HasDebugCallStack => Role -> Coercion -> (CoercionN, Coercion, Coercion)
- decomposePiCos :: HasDebugCallStack => CoercionN -> Pair Type -> [Type] -> ([CoercionN], CoercionN)
- getCoVar_maybe :: Coercion -> Maybe CoVar
- splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
- splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
- splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
- splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
- splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
- splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
- nthRole :: Role -> TyCon -> Int -> Role
- tyConRolesX :: Role -> TyCon -> [Role]
- tyConRolesRepresentational :: TyCon -> [Role]
- setNominalRole_maybe :: Role -> Coercion -> Maybe Coercion
- 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
- mkHomoForAllMCo :: TyCoVar -> MCoercion -> MCoercion
- mkFunResMCo :: Scaled Type -> MCoercionR -> MCoercionR
- mkPiMCos :: [Var] -> MCoercion -> MCoercion
- checkReflexiveMCo :: MCoercion -> MCoercion
- isReflMCo :: MCoercion -> Bool
- mkCoVar :: Name -> Type -> CoVar
- isCoVar :: Var -> Bool
- coVarName :: CoVar -> Name
- setCoVarName :: CoVar -> Name -> CoVar
- setCoVarUnique :: CoVar -> Unique -> CoVar
- isCoVar_maybe :: Coercion -> Maybe 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 :: TCvSubst -> Var -> Maybe Coercion
- substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion
- substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion]
- substCoVar :: TCvSubst -> CoVar -> Coercion
- substCoVars :: TCvSubst -> [CoVar] -> [Coercion]
- substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion
- substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar)
- extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst
- getCvSubstEnv :: TCvSubst -> 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 :: (LiftingContext -> Type -> (CoercionN, a)) -> LiftingContext -> TyCoVar -> (LiftingContext, TyCoVar, CoercionN, a)
- isMappedByLC :: TyCoVar -> LiftingContext -> Bool
- mkSubstLiftingContext :: TCvSubst -> LiftingContext
- zapLiftingContext :: LiftingContext -> LiftingContext
- substForAllCoBndrUsingLC :: Bool -> (Coercion -> Coercion) -> LiftingContext -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
- lcTCvSubst :: LiftingContext -> TCvSubst
- lcInScopeSet :: LiftingContext -> InScopeSet
- type LiftCoEnv = VarEnv Coercion
- data LiftingContext = LC TCvSubst LiftCoEnv
- liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst
- liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst
- substRightCo :: LiftingContext -> Coercion -> Coercion
- substLeftCo :: LiftingContext -> Coercion -> Coercion
- swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
- lcSubstLeft :: LiftingContext -> TCvSubst
- lcSubstRight :: LiftingContext -> TCvSubst
- eqCoercion :: Coercion -> Coercion -> Bool
- eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
- seqCo :: Coercion -> ()
- pprCo :: Coercion -> SDoc
- pprParendCo :: Coercion -> SDoc
- pprCoAxiom :: 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 :: Coercion -> CoercionN
- buildCoercion :: Type -> Type -> CoercionN
- multToCo :: Mult -> Coercion
- simplifyArgsWorker :: [TyCoBinder] -> Kind -> TyCoVarSet -> [Role] -> [(Type, Coercion)] -> ([Type], [Coercion], MCoercionN)
- hasCoercionHoleTy :: Type -> Bool
- hasCoercionHoleCo :: Coercion -> Bool
- type HoleSet = UniqSet CoercionHole
- coercionHolesOfType :: Type -> UniqSet CoercionHole
- coercionHolesOfCo :: Coercion -> UniqSet CoercionHole
Main data type
A Coercion
is concrete evidence of the equality/convertibility
of two types.
Instances
Data Coercion # | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Coercion -> c Coercion Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Coercion Source # toConstr :: Coercion -> Constr Source # dataTypeOf :: Coercion -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Coercion) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Coercion) Source # gmapT :: (forall b. Data b => b -> b) -> Coercion -> Coercion Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Coercion -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Coercion -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Coercion -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Coercion -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Coercion -> m Coercion Source # | |
Outputable Coercion # | |
Defined in GHC.Core.TyCo.Rep | |
Eq (DeBruijn Coercion) # | |
A semantically more meaningful type to represent what may or may not be a
useful Coercion
.
Instances
Data MCoercion # | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> MCoercion -> c MCoercion Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c MCoercion Source # toConstr :: MCoercion -> Constr Source # dataTypeOf :: MCoercion -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c MCoercion) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c MCoercion) Source # gmapT :: (forall b. Data b => b -> b) -> MCoercion -> MCoercion Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> MCoercion -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> MCoercion -> r Source # gmapQ :: (forall d. Data d => d -> u) -> MCoercion -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> MCoercion -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> MCoercion -> m MCoercion Source # | |
Outputable MCoercion # | |
Defined in GHC.Core.TyCo.Rep |
type MCoercionN = MCoercion #
type MCoercionR = MCoercion #
data UnivCoProvenance #
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 UnivCoProvenance # | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> UnivCoProvenance -> c UnivCoProvenance Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnivCoProvenance Source # toConstr :: UnivCoProvenance -> Constr Source # dataTypeOf :: UnivCoProvenance -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnivCoProvenance) Source # gmapT :: (forall b. Data b => b -> b) -> UnivCoProvenance -> UnivCoProvenance Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r Source # gmapQ :: (forall d. Data d => d -> u) -> UnivCoProvenance -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance Source # | |
Outputable UnivCoProvenance # | |
Defined in GHC.Core.TyCo.Rep Methods ppr :: UnivCoProvenance -> SDoc # |
data CoercionHole #
A coercion to be filled in by the type-checker. See Note [Coercion holes]
Instances
Data CoercionHole # | |
Defined in GHC.Core.TyCo.Rep Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoercionHole -> c CoercionHole Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoercionHole Source # toConstr :: CoercionHole -> Constr Source # dataTypeOf :: CoercionHole -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CoercionHole) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoercionHole) Source # gmapT :: (forall b. Data b => b -> b) -> CoercionHole -> CoercionHole Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoercionHole -> r Source # gmapQ :: (forall d. Data d => d -> u) -> CoercionHole -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> CoercionHole -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoercionHole -> m CoercionHole Source # | |
Uniquable CoercionHole # | |
Defined in GHC.Core.TyCo.Rep Methods getUnique :: CoercionHole -> Unique # | |
Outputable CoercionHole # | |
Defined in GHC.Core.TyCo.Rep Methods ppr :: CoercionHole -> SDoc # |
coHoleCoVar :: CoercionHole -> CoVar #
setCoHoleCoVar :: CoercionHole -> CoVar -> CoercionHole #
data LeftOrRight #
Instances
Data LeftOrRight # | |
Defined in GHC.Types.Basic Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LeftOrRight -> c LeftOrRight Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LeftOrRight Source # toConstr :: LeftOrRight -> Constr Source # dataTypeOf :: LeftOrRight -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LeftOrRight) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LeftOrRight) Source # gmapT :: (forall b. Data b => b -> b) -> LeftOrRight -> LeftOrRight Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r Source # gmapQ :: (forall d. Data d => d -> u) -> LeftOrRight -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> LeftOrRight -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight Source # | |
Binary LeftOrRight # | |
Defined in GHC.Types.Basic Methods put_ :: BinHandle -> LeftOrRight -> IO () # put :: BinHandle -> LeftOrRight -> IO (Bin LeftOrRight) # get :: BinHandle -> IO LeftOrRight # | |
Outputable LeftOrRight # | |
Defined in GHC.Types.Basic Methods ppr :: LeftOrRight -> SDoc # | |
Eq LeftOrRight # | |
Defined in GHC.Types.Basic |
Variable
Essentially a typed Name
, that may also contain some additional information
about the Var
and its use sites.
Instances
Data Var # | |
Defined in GHC.Types.Var Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Var -> c Var Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Var Source # toConstr :: Var -> Constr Source # dataTypeOf :: Var -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Var) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Var) Source # gmapT :: (forall b. Data b => b -> b) -> Var -> Var Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Var -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Var -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var -> m Var Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var -> m Var Source # | |
NamedThing Var # | |
Defined in GHC.Types.Var | |
HasOccName Var # | |
Defined in GHC.Types.Var | |
Uniquable Var # | |
Defined in GHC.Types.Var | |
Outputable Var # | |
Defined in GHC.Types.Var | |
OutputableBndr Var # | |
Defined in GHC.Core.Ppr Methods pprBndr :: BindingSite -> Var -> SDoc # pprPrefixOcc :: Var -> SDoc # pprInfixOcc :: Var -> SDoc # bndrIsJoin_maybe :: Var -> Maybe Int # | |
Eq Var # | |
Ord Var # | |
Eq (DeBruijn CoreAlt) # | |
Eq (DeBruijn CoreExpr) # | |
type Anno Id # | |
Defined in GHC.Hs.Extension | |
type Anno (LocatedN Id) # | |
Defined in GHC.Hs.Binds | |
type Anno [LocatedN Id] # | |
Defined in GHC.Hs.Binds |
Constructors
Nominal | |
Representational | |
Phantom |
Instances
Data Role # | |
Defined in GHC.Core.Coercion.Axiom Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Role -> c Role Source # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role Source # toConstr :: Role -> Constr Source # dataTypeOf :: Role -> DataType Source # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Role) Source # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Role) Source # gmapT :: (forall b. Data b => b -> b) -> Role -> Role Source # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r Source # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Role -> r Source # gmapQ :: (forall d. Data d => d -> u) -> Role -> [u] Source # gmapQi :: Int -> (forall d. Data d => d -> u) -> Role -> u Source # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Role -> m Role Source # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role Source # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Role -> m Role Source # | |
Binary Role # | |
Outputable Role # | |
Defined in GHC.Core.Coercion.Axiom | |
Eq Role # | |
Ord Role # | |
type Anno (Maybe Role) # | |
Defined in GHC.Hs.Decls | |
type Anno (Maybe Role) # | |
Defined in GHC.Hs.Decls |
Functions over coercions
coVarTypes :: HasDebugCallStack => CoVar -> Pair Type #
coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind, Kind, Type, Type, Role) #
coercionType :: Coercion -> Type #
mkCoercionType :: Role -> Type -> Type -> Type #
Makes a coercion type from two types: the types whose equality
is proven by the relevant Coercion
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
.
coercionLKind :: Coercion -> Type #
coercionRKind :: Coercion -> Type #
coercionKinds :: [Coercion] -> Pair [Type] #
Apply coercionKind
to multiple Coercion
s
coercionRole :: Coercion -> Role #
Retrieve the role from a coercion.
Constructing coercions
mkRepReflCo :: Type -> Coercion #
Make a representational reflexive coercion
mkNomReflCo :: Type -> Coercion #
Make a nominal reflexive coercion
mkCoVarCos :: [CoVar] -> [Coercion] #
mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Coercion #
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion #
mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type #
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type #
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type #
Return the left-hand type of the axiom, when the axiom is instantiated at the types given.
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type #
Instantiate the left-hand side of an unbranched axiom
mkPiCo :: Role -> Var -> Coercion -> Coercion #
Make a forall Coercion
, where both types related by the coercion
are quantified over the same variable.
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
.
Arguments
:: Int | "n" |
-> CoercionN | multiplicity coercion |
-> Coercion | argument coercion |
-> Coercion | result coercion |
-> Coercion | nth coercion from a FunCo See Note [Function coercions] If FunCo _ mult arg_co res_co :: (s1:TYPE sk1 :mult-> s2:TYPE sk2) ~ (t1:TYPE tk1 :mult-> t2:TYPE tk2) Then we want to behave as if co was TyConAppCo mult argk_co resk_co arg_co res_co where argk_co :: sk1 ~ tk1 = mkNthCo 0 (mkKindCo arg_co) resk_co :: sk2 ~ tk2 = mkNthCo 0 (mkKindCo res_co) i.e. mkRuntimeRepCo |
Extract the nth field of a FunCo
nthCoRole :: Int -> Coercion -> Role #
If you're about to call mkNthCo r n co
, then r
should be
whatever nthCoRole n co
returns.
mkLRCo :: LeftOrRight -> Coercion -> Coercion #
mkTyConAppCo :: HasDebugCallStack => 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 :: TyCoVar -> CoercionN -> Coercion -> Coercion #
Make a Coercion from a tycovar, a kind coercion, and a body coercion. The kind of the tycovar should be the left-hand kind of the kind coercion. See Note [Unused coercion variable in ForAllCo]
mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion #
Make a Coercion quantified over a type/coercion variable; the variable has the same type in both sides of the coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion #
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 #
Make a coercion from a coercion hole
Arguments
:: UnivCoProvenance | |
-> 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.
mkSubCo :: HasDebugCallStack => Coercion -> Coercion #
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion #
Arguments
:: Role | role of the created coercion, "r" |
-> Coercion | :: phi1 ~N phi2 |
-> Coercion | g1 :: phi1 |
-> Coercion | g2 :: phi2 |
-> Coercion | :: g1 ~r g2 |
Make a "coercion between coercions".
downgradeRole :: Role -> Role -> Coercion -> Coercion #
Like downgradeRole_maybe
, but panics if the change isn't a downgrade.
See Note [Role twiddling functions]
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion #
mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion #
Given ty :: k1
, co :: k1 ~ k2
,
produces co' :: ty ~r (ty |> co)
mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion #
Given ty :: k1
, co :: k1 ~ k2
,
produces co' :: (ty |> co) ~r ty
mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion #
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 :: Role -> Type -> CoercionN -> Coercion -> Coercion #
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 #
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 #
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 #
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.
mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN #
Given a family instance TyCon
and its arg Coercion
s, return the
corresponding family Coercion
. E.g:
data family T a data instance T (Maybe b) = MkT b
Where the instance TyCon
is :RTL, so:
mkFamilyTyConAppCo :RTL (co :: a ~# Int) = T (Maybe a) ~# T (Maybe Int)
cf. mkFamilyTyConApp
mkPrimEqPred :: Type -> Type -> Type #
Creates a primitive type equality predicate. Invariant: the types are not Coercions
mkReprPrimEqPred :: Type -> Type -> Type #
mkPrimEqPredRole :: Role -> Type -> Type -> PredType #
Makes a lifted equality predicate at the given role
mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type #
Creates a primitive type equality predicate with explicit kinds
mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type #
Creates a primitive representational type equality predicate with explicit kinds
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 ev = RecTcChecker -> TyCon -> [Type] -> NormaliseStepResult ev #
A function to check if we can reduce a type by one step. Used
with topNormaliseTypeX
.
data NormaliseStepResult ev #
The result of stepping in a normalisation function.
See topNormaliseTypeX
.
Constructors
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
Outputable ev => Outputable (NormaliseStepResult ev) # | |
Defined in GHC.Core.Coercion Methods ppr :: NormaliseStepResult ev -> SDoc # |
composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev #
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
mapStepResult :: (ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2 #
unwrapNewTypeStepper :: NormaliseStepper Coercion #
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
. Specifically, here's the invariant:
topNormaliseNewType_maybe rec_nts ty = Just (co, ty')
then (a) co : ty ~ 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) #
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 => Role -> Coercion -> (CoercionN, Coercion, Coercion) #
decomposePiCos :: HasDebugCallStack => CoercionN -> Pair Type -> [Type] -> ([CoercionN], CoercionN) #
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_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion) #
Like splitForAllCo_maybe
, but only returns Just for tyvar binder
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion) #
Like splitForAllCo_maybe
, but only returns Just for covar binder
tyConRolesX :: Role -> TyCon -> [Role] #
tyConRolesRepresentational :: TyCon -> [Role] #
setNominalRole_maybe :: Role -> Coercion -> Maybe Coercion #
Converts a coercion to be nominal, if possible. See Note [Role twiddling functions]
pickLR :: LeftOrRight -> (a, a) -> a #
isGReflCo :: Coercion -> Bool #
Tests if this coercion is obviously a generalized reflexive coercion. Guaranteed to work very quickly.
isReflCo :: Coercion -> Bool #
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) #
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) #
Returns the type coerced if this coercion is a generalized reflexive coercion. Guaranteed to work very quickly.
isReflexiveCo :: Coercion -> Bool #
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) #
Extracts the coerced type from a reflexive coercion. This potentially walks over the entire coercion, so avoid doing this in a loop.
isReflCoVar_maybe :: Var -> Maybe Coercion #
isGReflMCo :: MCoercion -> Bool #
Tests if this MCoercion is obviously generalized reflexive Guaranteed to work very quickly.
mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion #
mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion #
mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion #
Like mkCoherenceRightCo
, but with an MCoercion
mkTransMCo :: MCoercion -> MCoercion -> MCoercion #
Compose two MCoercions via transitivity
mkTransMCoL :: MCoercion -> Coercion -> MCoercion #
mkTransMCoR :: Coercion -> MCoercion -> MCoercion #
mkHomoForAllMCo :: TyCoVar -> MCoercion -> MCoercion #
mkFunResMCo :: Scaled Type -> MCoercionR -> MCoercionR #
checkReflexiveMCo :: MCoercion -> MCoercion #
Coercion variables
Is this a coercion variable?
Satisfies
.isId
v ==> isCoVar
v == not (isNonCoVarId
v)
setCoVarName :: CoVar -> Name -> CoVar #
setCoVarUnique :: CoVar -> Unique -> CoVar #
isCoVar_maybe :: Coercion -> Maybe CoVar #
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.)
Free variables
tyCoVarsOfCo :: Coercion -> TyCoVarSet #
tyCoVarsOfCos :: [Coercion] -> TyCoVarSet #
coVarsOfCo :: Coercion -> CoVarSet #
tyCoFVsOfCo :: Coercion -> FV #
tyCoFVsOfCos :: [Coercion] -> FV #
tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet #
Get a deterministic set of the vars free in a coercion
coercionSize :: Coercion -> Int #
Substitution
substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion #
Substitute within a Coercion
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion] #
Substitute within several Coercion
s
The substitution has to satisfy the invariants described in
Note [The substitution invariant].
substCoVar :: TCvSubst -> CoVar -> Coercion #
substCoVars :: TCvSubst -> [CoVar] -> [Coercion] #
substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion #
Coercion substitution, see zipTvSubst
substCoVarBndr :: HasCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar) #
getCvSubstEnv :: TCvSubst -> CvSubstEnv #
Lifting
liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion #
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 #
liftCoSubstWithEx :: Role -> [TyVar] -> [Coercion] -> [TyCoVar] -> [Type] -> (Type -> Coercion, [Type]) #
Arguments
:: LiftingContext | original LC |
-> TyCoVar | new variable to map... |
-> Coercion | ...to this lifted version |
-> LiftingContext |
Extend a lifting context with a new mapping.
extendLiftingContextAndInScope #
Arguments
:: 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 :: (LiftingContext -> Type -> (CoercionN, a)) -> LiftingContext -> TyCoVar -> (LiftingContext, TyCoVar, CoercionN, a) #
isMappedByLC :: TyCoVar -> LiftingContext -> Bool #
Is a var in the domain of a lifting context?
zapLiftingContext :: LiftingContext -> LiftingContext #
Erase the environments in a lifting context
substForAllCoBndrUsingLC :: Bool -> (Coercion -> Coercion) -> LiftingContext -> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion) #
Like substForAllCoBndr
, but works on a lifting context
lcTCvSubst :: LiftingContext -> TCvSubst #
Extract the underlying substitution from the LiftingContext
lcInScopeSet :: LiftingContext -> InScopeSet #
Get the InScopeSet
from a LiftingContext
data LiftingContext #
Instances
Outputable LiftingContext # | |
Defined in GHC.Core.Coercion Methods ppr :: LiftingContext -> SDoc # |
liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst #
liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst #
substRightCo :: LiftingContext -> Coercion -> Coercion #
substLeftCo :: LiftingContext -> Coercion -> Coercion #
swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv #
Apply "sym" to all coercions in a LiftCoEnv
lcSubstLeft :: LiftingContext -> TCvSubst #
lcSubstRight :: LiftingContext -> TCvSubst #
Comparison
eqCoercion :: Coercion -> Coercion -> Bool #
Syntactic equality of coercions
eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool #
Compare two Coercion
s, with respect to an RnEnv2
Forcing evaluation of coercions
Pretty-printing
pprParendCo :: Coercion -> SDoc #
pprCoAxiom :: CoAxiom br -> SDoc #
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc #
pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc #
pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc #
etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type) #
Tidying
tidyCo :: TidyEnv -> Coercion -> Coercion #
Tidy a Coercion
See Note [Strictness in tidyType and friends]
Other
promoteCoercion :: Coercion -> CoercionN #
like mkKindCo, but aggressively & recursively optimizes to avoid using a KindCo constructor. The output role is nominal.
buildCoercion :: Type -> Type -> CoercionN #
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.
simplifyArgsWorker :: [TyCoBinder] -> Kind -> TyCoVarSet -> [Role] -> [(Type, Coercion)] -> ([Type], [Coercion], MCoercionN) #
hasCoercionHoleTy :: Type -> Bool #
Is there a coercion hole in this type?
hasCoercionHoleCo :: Coercion -> Bool #
Is there a coercion hole in this coercion?
type HoleSet = UniqSet CoercionHole #
A set of CoercionHole
s
coercionHolesOfType :: Type -> UniqSet CoercionHole #
Extract out all the coercion holes from a given type