GHC.Core.Coercion

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.

Main data type

data Coercion

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

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

Outputable Coercion

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: Coercion -> SDoc

Eq (DeBruijn Coercion)

Defined in GHC.Core.Map.Type

Methods

(==) :: DeBruijn Coercion -> DeBruijn Coercion -> Bool

(/=) :: DeBruijn Coercion -> DeBruijn Coercion -> Bool

type CoercionN = Coercion

type CoercionR = Coercion

type CoercionP = Coercion

data MCoercion

A semantically more meaningful type to represent what may or may not be a useful Coercion.

Constructors

MRefl

MCo 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

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

Outputable MCoercion

Defined in GHC.Core.TyCo.Rep

Methods

ppr :: MCoercion -> SDoc

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c UnivCoProvenance

toConstr :: UnivCoProvenance -> Constr

dataTypeOf :: UnivCoProvenance -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c UnivCoProvenance)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UnivCoProvenance)

gmapT :: (forall b. Data b => b -> b) -> UnivCoProvenance -> UnivCoProvenance

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UnivCoProvenance -> r

gmapQ :: (forall d. Data d => d -> u) -> UnivCoProvenance -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> UnivCoProvenance -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> UnivCoProvenance -> m UnivCoProvenance

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]

Constructors

CoercionHole

Fields

• ch_co_var :: CoVar
• ch_ref :: IORef (Maybe Coercion)

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

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

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

Constructors

CLeft

CRight

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LeftOrRight

toConstr :: LeftOrRight -> Constr

dataTypeOf :: LeftOrRight -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LeftOrRight)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LeftOrRight)

gmapT :: (forall b. Data b => b -> b) -> LeftOrRight -> LeftOrRight

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LeftOrRight -> r

gmapQ :: (forall d. Data d => d -> u) -> LeftOrRight -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> LeftOrRight -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LeftOrRight -> m LeftOrRight

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

Methods

(==) :: LeftOrRight -> LeftOrRight -> Bool

(/=) :: LeftOrRight -> LeftOrRight -> Bool

data Var

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Var

toConstr :: Var -> Constr

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

NamedThing Var

Defined in GHC.Types.Var

Methods

getOccName :: Var -> OccName

getName :: Var -> Name

HasOccName Var

Defined in GHC.Types.Var

Methods

occName :: Var -> OccName

Uniquable Var

Defined in GHC.Types.Var

Methods

getUnique :: Var -> Unique

Outputable Var

Defined in GHC.Types.Var

Methods

ppr :: Var -> SDoc

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

Defined in GHC.Types.Var

Methods

(==) :: Var -> Var -> Bool

(/=) :: Var -> Var -> Bool

Ord Var

Defined in GHC.Types.Var

Methods

compare :: Var -> Var -> Ordering

(<) :: Var -> Var -> Bool

(<=) :: Var -> Var -> Bool

(>) :: Var -> Var -> Bool

(>=) :: Var -> Var -> Bool

max :: Var -> Var -> Var

min :: Var -> Var -> Var

Eq (DeBruijn CoreAlt)

Defined in GHC.Core.Map.Expr

Methods

(==) :: DeBruijn CoreAlt -> DeBruijn CoreAlt -> Bool

(/=) :: DeBruijn CoreAlt -> DeBruijn CoreAlt -> Bool

Eq (DeBruijn CoreExpr)

Defined in GHC.Core.Map.Expr

Methods

(==) :: DeBruijn CoreExpr -> DeBruijn CoreExpr -> Bool

(/=) :: DeBruijn CoreExpr -> DeBruijn CoreExpr -> Bool

Eq (DeBruijn Var)

Defined in GHC.Core.Map.Type

Methods

(==) :: DeBruijn Var -> DeBruijn Var -> Bool

(/=) :: DeBruijn Var -> DeBruijn Var -> Bool

OutputableBndr (Id, TagSig)

Defined in GHC.Stg.InferTags.TagSig

Methods

pprBndr :: BindingSite -> (Id, TagSig) -> SDoc

pprPrefixOcc :: (Id, TagSig) -> SDoc

pprInfixOcc :: (Id, TagSig) -> SDoc

bndrIsJoin_maybe :: (Id, TagSig) -> Maybe Int

type Anno Id

Defined in GHC.Hs.Extension

type Anno Id = SrcSpanAnnN

type Anno (LocatedN Id)

Defined in GHC.Hs.Binds

type Anno (LocatedN Id) = SrcSpan

type Anno [LocatedN Id]

Defined in GHC.Hs.Binds

type Anno [LocatedN Id] = SrcSpan

type CoVar = Id

Coercion Variable

type TyCoVar = Id

Type or Coercion Variable

data Role

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

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Role

toConstr :: Role -> Constr

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

Binary Role

Defined in GHC.Core.Coercion.Axiom

Methods

put_ :: BinHandle -> Role -> IO ()

put :: BinHandle -> Role -> IO (Bin Role)

get :: BinHandle -> IO Role

Outputable Role

Defined in GHC.Core.Coercion.Axiom

Methods

ppr :: Role -> SDoc

Eq Role

Defined in GHC.Core.Coercion.Axiom

Methods

(==) :: Role -> Role -> Bool

(/=) :: Role -> Role -> Bool

Ord Role

Defined in GHC.Core.Coercion.Axiom

Methods

compare :: Role -> Role -> Ordering

(<) :: Role -> Role -> Bool

(<=) :: Role -> Role -> Bool

(>) :: Role -> Role -> Bool

(>=) :: Role -> Role -> Bool

max :: Role -> Role -> Role

min :: Role -> Role -> Role

type Anno (Maybe Role)

Defined in GHC.Hs.Decls

type Anno (Maybe Role) = SrcAnn NoEpAnns

type Anno (Maybe Role)

Defined in GHC.Hs.Decls

type Anno (Maybe Role) = SrcAnn NoEpAnns

ltRole :: Role -> Role -> Bool

Functions over coercions

coVarRType :: HasDebugCallStack => CoVar -> Type

coVarLType :: HasDebugCallStack => CoVar -> Type

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

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 Coercions

coercionRole :: Coercion -> Role

Retrieve the role from a coercion.

coercionKindRole :: Coercion -> (Pair Type, Role)

Get a coercion's kind and role.

Constructing coercions

mkGReflCo :: Role -> Type -> MCoercionN -> Coercion

Make a generalized reflexive coercion

mkReflCo :: Role -> Type -> Coercion

Make a reflexive coercion

mkRepReflCo :: Type -> Coercion

Make a representational reflexive coercion

mkNomReflCo :: Type -> Coercion

Make a nominal reflexive 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

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.

mkPiCos :: Role -> [Var] -> Coercion -> Coercion

mkCoCast :: Coercion -> CoercionR -> Coercion

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.

mkTransCo :: Coercion -> Coercion -> Coercion

Create a new Coercion by composing the two given Coercions transitively. (co1 ; co2)

mkNthCo :: HasDebugCallStack => Role -> Int -> Coercion -> Coercion

mkNthCoFunCo

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

mkInstCo :: Coercion -> Coercion -> Coercion

Instantiates a Coercion.

mkAppCo

Arguments

:: Coercion

:: t1 ~r t2

-> Coercion

:: s1 ~N s2, where s1 :: k1, s2 :: k2

-> Coercion

:: t1 s1 ~r t2 s2

Apply a Coercion to another Coercion. The second coercion must be Nominal, unless the first is Phantom. If the first is Phantom, then the second can be either Phantom or Nominal.

mkAppCos :: Coercion -> [Coercion] -> Coercion

Applies multiple Coercions to another Coercion, from left to right. See also mkAppCo.

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.

mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion

Build a function Coercion from two other Coercions. That is, given co1 :: a ~ b and co2 :: x ~ y produce co :: (a -> x) ~ (b -> y).

mkFunResCo :: Role -> Scaled Type -> Coercion -> Coercion

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]

mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion

Make nested ForAllCos

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

mkUnivCo

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

mkProofIrrelCo

Arguments

:: 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

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.

mkKindCo :: Coercion -> Coercion

Given co :: (a :: k) ~ (b :: k') produce co' :: k ~ k'.

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 Coercions, 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

mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type

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 `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

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

decomposeCo :: Arity -> Coercion -> [Role] -> [Coercion]

This breaks a Coercion with type T A B C ~ T D E F into a list of Coercions of kinds A ~ D, B ~ E and E ~ F. Hence:

decomposeCo 3 c [r1, r2, r3] = [nth r1 0 c, nth r2 1 c, nth r3 2 c]

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.

splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)

splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)

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

nthRole :: Role -> TyCon -> Int -> Role

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

coToMCo :: Coercion -> MCoercion

mkTransMCo :: MCoercion -> MCoercion -> MCoercion

Compose two MCoercions via transitivity

mkTransMCoL :: MCoercion -> Coercion -> MCoercion

mkTransMCoR :: Coercion -> MCoercion -> MCoercion

mkCastTyMCo :: Type -> MCoercion -> Type

Cast a type by an MCoercion

mkSymMCo :: MCoercion -> MCoercion

Get the reverse of an MCoercion

mkHomoForAllMCo :: TyCoVar -> MCoercion -> MCoercion

mkFunResMCo :: Scaled Type -> MCoercionR -> MCoercionR

mkPiMCos :: [Var] -> MCoercion -> MCoercion

isReflMCo :: MCoercion -> Bool

checkReflexiveMCo :: MCoercion -> MCoercion

Coercion variables

mkCoVar :: Name -> Type -> CoVar

isCoVar :: Var -> Bool

Is this a coercion variable? Satisfies isId v ==> isCoVar v == not (isNonCoVarId v).

coVarName :: CoVar -> Name

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

anyFreeVarsOfCo :: (TyCoVar -> Bool) -> Coercion -> Bool

Substitution

type CvSubstEnv = CoVarEnv Coercion

A substitution of Coercions for CoVars

emptyCvSubstEnv :: CvSubstEnv

lookupCoVar :: TCvSubst -> Var -> Maybe Coercion

substCo :: HasDebugCallStack => TCvSubst -> Coercion -> Coercion

Substitute within a Coercion The substitution has to satisfy the invariants described in Note [The substitution invariant].

substCos :: HasDebugCallStack => TCvSubst -> [Coercion] -> [Coercion]

Substitute within several Coercions The substitution has to satisfy the invariants described in Note [The substitution invariant].

substCoVar :: TCvSubst -> CoVar -> Coercion

substCoVars :: TCvSubst -> [CoVar] -> [Coercion]

substCoWith :: HasDebugCallStack => [TyVar] -> [Type] -> Coercion -> Coercion

Coercion substitution, see zipTvSubst

substCoVarBndr :: HasDebugCallStack => TCvSubst -> CoVar -> (TCvSubst, CoVar)

extendTvSubstAndInScope :: TCvSubst -> TyVar -> Type -> TCvSubst

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

liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion

liftCoSubstWithEx :: Role -> [TyVar] -> [Coercion] -> [TyCoVar] -> [Type] -> (Type -> Coercion, [Type])

emptyLiftingContext :: InScopeSet -> LiftingContext

extendLiftingContext

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

Arguments

:: (r -> CoercionN)

coercion getter

-> (LiftingContext -> Type -> r)

callback

-> LiftingContext

-> TyCoVar

-> (LiftingContext, TyCoVar, r)

isMappedByLC :: TyCoVar -> LiftingContext -> Bool

Is a var in the domain of a lifting context?

mkSubstLiftingContext :: TCvSubst -> LiftingContext

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

type LiftCoEnv = VarEnv Coercion

data LiftingContext

Constructors

LC TCvSubst LiftCoEnv

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 Coercions, with respect to an RnEnv2

Forcing evaluation of coercions

seqCo :: Coercion -> ()

Pretty-printing

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)

Tidying

tidyCo :: TidyEnv -> Coercion -> Coercion

Tidy a Coercion

See Note [Strictness in tidyType and friends]

tidyCos :: TidyEnv -> [Coercion] -> [Coercion]

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.

multToCo :: Mult -> Coercion

hasCoercionHoleTy :: Type -> Bool

Is there a coercion hole in this type?

hasCoercionHoleCo :: Coercion -> Bool

Is there a coercion hole in this coercion?

hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool

setCoHoleType :: CoercionHole -> Type -> CoercionHole

Set the type of a CoercionHole