ghc-8.8.1: The GHC API
Safe HaskellNone
LanguageHaskell2010

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

Main data type

data Coercion Source #

A Coercion is concrete evidence of the equality/convertibility of two types.

Instances

Instances details
Data Coercion # 
Instance details

Defined in TyCoRep

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 # 
Instance details

Defined in TyCoRep

data MCoercion Source #

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

Constructors

MRefl 
MCo Coercion 

Instances

Instances details
Data MCoercion # 
Instance details

Defined in TyCoRep

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 # 
Instance details

Defined in TyCoRep

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

Instances details
Data UnivCoProvenance # 
Instance details

Defined in TyCoRep

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 # 
Instance details

Defined in TyCoRep

data CoercionHole Source #

A coercion to be filled in by the type-checker. See Note [Coercion holes]

Constructors

CoercionHole 

Instances

Instances details
Data CoercionHole # 
Instance details

Defined in TyCoRep

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 #

Outputable CoercionHole # 
Instance details

Defined in TyCoRep

data LeftOrRight Source #

Constructors

CLeft 
CRight 

Instances

Instances details
Eq LeftOrRight # 
Instance details

Defined in BasicTypes

Data LeftOrRight # 
Instance details

Defined in BasicTypes

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 #

Outputable LeftOrRight # 
Instance details

Defined in BasicTypes

Binary LeftOrRight # 
Instance details

Defined in Binary

data Var Source #

Variable

Essentially a typed Name, that may also contain some additional information about the Var and its use sites.

Instances

Instances details
Eq Var # 
Instance details

Defined in Var

Methods

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

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

Data Var # 
Instance details

Defined in 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 #

Ord Var # 
Instance details

Defined in 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 #

OutputableBndr Var # 
Instance details

Defined in PprCore

Outputable Var # 
Instance details

Defined in Var

Methods

ppr :: Var -> SDoc Source #

pprPrec :: Rational -> Var -> SDoc Source #

Uniquable Var # 
Instance details

Defined in Var

Methods

getUnique :: Var -> Unique Source #

HasOccName Var # 
Instance details

Defined in Var

Methods

occName :: Var -> OccName Source #

NamedThing Var # 
Instance details

Defined in Var

type CoVar = Id Source #

Coercion Variable

type TyCoVar = Id Source #

Type or Coercion Variable

data Role Source #

Instances

Instances details
Eq Role # 
Instance details

Defined in CoAxiom

Methods

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

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

Data Role # 
Instance details

Defined in CoAxiom

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 #

Ord Role # 
Instance details

Defined in CoAxiom

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 #

Outputable Role # 
Instance details

Defined in CoAxiom

Binary Role # 
Instance details

Defined in CoAxiom

Functions over coercions

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

mkCoercionType :: Role -> Type -> Type -> Type Source #

Makes a coercion type from two types: the types whose equality is proven by the relevant Coercion

coercionRole :: Coercion -> Role Source #

Retrieve the role from a coercion.

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

Get a coercion's kind and role.

Constructing coercions

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

Make a generalized reflexive coercion

mkReflCo :: Role -> Type -> Coercion Source #

Make a reflexive coercion

mkRepReflCo :: Type -> Coercion Source #

Make a representational reflexive coercion

mkNomReflCo :: Type -> Coercion Source #

Make a nominal reflexive coercion

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

mkTransCo :: Coercion -> Coercion -> Coercion Source #

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

mkTransMCo :: MCoercion -> MCoercion -> MCoercion Source #

Compose two MCoercions via transitivity

nthCoRole :: Int -> Coercion -> Role Source #

If you're about to call mkNthCo r n co, then r should be whatever nthCoRole n co returns.

mkAppCo Source #

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 Source #

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

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.

mkFunCo :: Role -> Coercion -> Coercion -> Coercion Source #

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

mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion Source #

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 Source #

Make nested ForAllCos

mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion Source #

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 Source #

Make a phantom coercion between two types. The coercion passed in must be a nominal coercion between the kinds of the types.

mkUnsafeCo :: Role -> Type -> Type -> Coercion Source #

Manufacture an unsafe coercion from thin air. Currently (May 14) this is used only to implement the unsafeCoerce# primitive. Optimise by pushing down through type constructors.

mkHoleCo :: CoercionHole -> Coercion Source #

Make a coercion from a coercion hole

mkUnivCo Source #

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.

mkProofIrrelCo Source #

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 Source #

Like downgradeRole_maybe, but panics if the change isn't a downgrade. See Note [Role twiddling functions]

maybeSubCo :: EqRel -> Coercion -> Coercion Source #

If the EqRel is ReprEq, makes a SubCo; otherwise, does nothing. Note that the input coercion should always be nominal.

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 ty :: k1, co :: k1 ~ 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 :: 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.

mkKindCo :: Coercion -> Coercion Source #

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

castCoercionKind :: Coercion -> Role -> Type -> Type -> CoercionN -> CoercionN -> Coercion Source #

Creates a new coercion with both of its types casted by different casts castCoercionKind g r t1 t2 h1 h2, where g :: t1 ~r t2, has type (t1 |> h1) ~r (t2 |> h2). h1 and h2 must be nominal.

castCoercionKindI :: 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 castCoercionKind instead if t1, t2, and r are known beforehand.

Decomposition

instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion) Source #

If co :: T ts ~ rep_ty then:

instNewTyCon_maybe T ts = Just (rep_ty, co)

Checks for a newtype, and for being saturated

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.

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

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 : ty0 ~ ty'. (b) ty' is not a newtype.

The function returns Nothing for non-newtypes, or unsaturated applications

This function does *not* look through type families, because it has no access to the type family environment. If you do have that at hand, consider to use topNormaliseType_maybe, which should be a drop-in replacement for topNormaliseNewType_maybe 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

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

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]

getCoVar_maybe :: Coercion -> Maybe CoVar Source #

Attempts to obtain the type variable underlying a Coercion

splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion]) Source #

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) Source #

Attempt to take a coercion application apart.

splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion) Source #

Like splitForAllCo_maybe, but only returns Just for tyvar binder

splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion) Source #

Like splitForAllCo_maybe, but only returns Just for covar binder

setNominalRole_maybe :: Role -> Coercion -> Maybe Coercion Source #

Converts a coercion to be nominal, if possible. See Note [Role twiddling functions]

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.

Coercion variables

isCoVar_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.)

Free variables

tyCoVarsOfCoDSet :: Coercion -> DTyCoVarSet Source #

Get a deterministic set of the vars free in a coercion

Substitution

type CvSubstEnv = CoVarEnv Coercion Source #

A substitution of Coercions for CoVars

substCo :: HasCallStack => TCvSubst -> Coercion -> Coercion Source #

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

substCos :: HasCallStack => TCvSubst -> [Coercion] -> [Coercion] Source #

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

substCoWith :: HasCallStack => [TyVar] -> [Type] -> Coercion -> Coercion Source #

Coercion substitution, see zipTvSubst

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.

extendLiftingContext Source #

Arguments

:: LiftingContext

original LC

-> TyCoVar

new variable to map...

-> Coercion

...to this lifted version

-> LiftingContext 

Extend a lifting context with a new mapping.

extendLiftingContextAndInScope Source #

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

isMappedByLC :: TyCoVar -> LiftingContext -> Bool Source #

Is a var in the domain of a lifting context?

zapLiftingContext :: LiftingContext -> LiftingContext Source #

Erase the environments in a lifting context

lcTCvSubst :: LiftingContext -> TCvSubst Source #

Extract the underlying substitution from the LiftingContext

data LiftingContext Source #

Constructors

LC TCvSubst LiftCoEnv 

Instances

Instances details
Outputable LiftingContext # 
Instance details

Defined in Coercion

swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv Source #

Apply "sym" to all coercions in a LiftCoEnv

Comparison

eqCoercion :: Coercion -> Coercion -> Bool Source #

Syntactic equality of coercions

eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool Source #

Compare two Coercions, with respect to an RnEnv2

Forcing evaluation of coercions

Pretty-printing

Tidying

Other

promoteCoercion :: Coercion -> CoercionN Source #

like mkKindCo, but aggressively & recursively optimizes to avoid using a KindCo constructor. The output role is nominal.

buildCoercion :: 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 OptCoercion.