ghc-lib-parser-9.6.6.20240701: The GHC API, decoupled from GHC versions
Safe HaskellIgnore
LanguageHaskell2010

GHC.Core.Coercion.Axiom

Description

Module for coercion axioms, used to represent type family instances and newtypes

Synopsis

Documentation

type Branched = 'Branched Source #

type Unbranched = 'Unbranched Source #

newtype Branches (br :: BranchFlag) Source #

Constructors

MkBranches 

mapAccumBranches :: ([CoAxBranch] -> CoAxBranch -> CoAxBranch) -> Branches br -> Branches br Source #

The [CoAxBranch] passed into the mapping function is a list of all previous branches, reversed

data CoAxiom br Source #

A CoAxiom is a "coercion constructor", i.e. a named equality axiom.

Instances

Instances details
Typeable br => Data (CoAxiom br) Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxiom br -> c (CoAxiom br)

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

toConstr :: CoAxiom br -> Constr

dataTypeOf :: CoAxiom br -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> CoAxiom br -> CoAxiom br

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

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

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

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

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

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

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

NamedThing (CoAxiom br) Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Uniquable (CoAxiom br) Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

getUnique :: CoAxiom br -> Unique Source #

Outputable (CoAxiom br) Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

ppr :: CoAxiom br -> SDoc Source #

Eq (CoAxiom br) Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

(==) :: CoAxiom br -> CoAxiom br -> Bool #

(/=) :: CoAxiom br -> CoAxiom br -> Bool #

data CoAxBranch Source #

Constructors

CoAxBranch 

Instances

Instances details
Data CoAxBranch Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch

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

toConstr :: CoAxBranch -> Constr

dataTypeOf :: CoAxBranch -> DataType

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

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

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

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

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

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

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

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

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

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

Outputable CoAxBranch Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

ppr :: CoAxBranch -> SDoc Source #

data Role Source #

See Note [Roles] in GHC.Core.Coercion

Order of constructors matters: the Ord instance coincides with the *super*typing relation on roles.

Instances

Instances details
Data Role Source # 
Instance details

Defined in Language.Haskell.Syntax.Basic

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

Defined in GHC.Core.Coercion.Axiom

Outputable Role Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

ppr :: Role -> SDoc Source #

Eq Role Source # 
Instance details

Defined in Language.Haskell.Syntax.Basic

Methods

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

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

Ord Role Source # 
Instance details

Defined in Language.Haskell.Syntax.Basic

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

Defined in GHC.Hs.Decls

type Anno (Maybe Role) Source # 
Instance details

Defined in GHC.Hs.Decls

data CoAxiomRule Source #

For now, we work only with nominal equality.

Constructors

CoAxiomRule 

Fields

Instances

Instances details
Data CoAxiomRule Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxiomRule -> c CoAxiomRule

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

toConstr :: CoAxiomRule -> Constr

dataTypeOf :: CoAxiomRule -> DataType

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

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

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

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

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

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

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

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

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

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

Uniquable CoAxiomRule Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Outputable CoAxiomRule Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Methods

ppr :: CoAxiomRule -> SDoc Source #

Eq CoAxiomRule Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

Ord CoAxiomRule Source # 
Instance details

Defined in GHC.Core.Coercion.Axiom

type TypeEqn = Pair Type Source #

A more explicit representation for `t1 ~ t2`.

Orphan instances

Binary Role Source # 
Instance details

Outputable Role Source # 
Instance details

Methods

ppr :: Role -> SDoc Source #