CoAxiom
Fields co_ax_unique :: Unique co_ax_name :: Name co_ax_role :: Role co_ax_tc :: TyCon co_ax_branches :: Branches br co_ax_implicit :: Bool

Instances

Eq (CoAxiom br)
Methods (==) :: CoAxiom br -> CoAxiom br -> Bool (/=) :: CoAxiom br -> CoAxiom br -> Bool
Typeable BranchFlag br => Data (CoAxiom br)
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxiom br -> c (CoAxiom br) Source gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CoAxiom br) Source toConstr :: CoAxiom br -> Constr Source dataTypeOf :: CoAxiom br -> DataType Source dataCast1 :: Typeable (TYPE Lifted -> TYPE Lifted) t => (forall d. Data d => c (t d)) -> Maybe (c (CoAxiom br)) Source dataCast2 :: Typeable (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CoAxiom br)) Source gmapT :: (forall b. Data b => b -> b) -> CoAxiom br -> CoAxiom br Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoAxiom br -> r Source gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoAxiom br -> r Source gmapQ :: (forall d. Data d => d -> u) -> CoAxiom br -> [u] Source gmapQi :: Int -> (forall d. Data d => d -> u) -> CoAxiom br -> u Source gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoAxiom br -> m (CoAxiom br) Source gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoAxiom br -> m (CoAxiom br) Source gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoAxiom br -> m (CoAxiom br) Source
Ord (CoAxiom br)
Methods compare :: CoAxiom br -> CoAxiom br -> Ordering (<) :: CoAxiom br -> CoAxiom br -> Bool (<=) :: CoAxiom br -> CoAxiom br -> Bool (>) :: CoAxiom br -> CoAxiom br -> Bool (>=) :: CoAxiom br -> CoAxiom br -> Bool max :: CoAxiom br -> CoAxiom br -> CoAxiom br min :: CoAxiom br -> CoAxiom br -> CoAxiom br
Outputable (CoAxiom br)
Methods ppr :: CoAxiom br -> SDoc Source pprPrec :: Rational -> CoAxiom br -> SDoc Source
Uniquable (CoAxiom br)
Methods getUnique :: CoAxiom br -> Unique Source
NamedThing (CoAxiom br)
Methods getOccName :: CoAxiom br -> OccName Source getName :: CoAxiom br -> Name Source

data CoAxBranch Source

Constructors

CoAxBranch
Fields cab_loc :: SrcSpan cab_tvs :: [TyVar] cab_cvs :: [CoVar] cab_roles :: [Role] cab_lhs :: [Type] cab_rhs :: Type cab_incomps :: [CoAxBranch]

Instances

Data CoAxBranch
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch Source gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoAxBranch Source toConstr :: CoAxBranch -> Constr Source dataTypeOf :: CoAxBranch -> DataType Source dataCast1 :: Typeable (TYPE Lifted -> TYPE Lifted) t => (forall d. Data d => c (t d)) -> Maybe (c CoAxBranch) Source dataCast2 :: Typeable (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch) Source gmapT :: (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r Source gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r Source gmapQ :: (forall d. Data d => d -> u) -> CoAxBranch -> [u] Source gmapQi :: Int -> (forall d. Data d => d -> u) -> CoAxBranch -> u Source gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch Source gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch Source gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch Source
Outputable CoAxBranch
Methods ppr :: CoAxBranch -> SDoc Source pprPrec :: Rational -> CoAxBranch -> SDoc Source

toBranchedAxiom :: CoAxiom br -> CoAxiom Branched Source

toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched Source

coAxiomName :: CoAxiom br -> Name Source

coAxiomArity :: CoAxiom br -> BranchIndex -> Arity Source

coAxiomBranches :: CoAxiom br -> Branches br Source

coAxiomTyCon :: CoAxiom br -> TyCon Source

isImplicitCoAxiom :: CoAxiom br -> Bool Source

coAxiomNumPats :: CoAxiom br -> Int Source

coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch Source

coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch Source

coAxiomRole :: CoAxiom br -> Role Source

coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch Source

coAxBranchTyVars :: CoAxBranch -> [TyVar] Source

coAxBranchCoVars :: CoAxBranch -> [CoVar] Source

coAxBranchRoles :: CoAxBranch -> [Role] Source

coAxBranchLHS :: CoAxBranch -> [Type] Source

coAxBranchRHS :: CoAxBranch -> Type Source

coAxBranchSpan :: CoAxBranch -> SrcSpan Source

coAxBranchIncomps :: CoAxBranch -> [CoAxBranch] Source

placeHolderIncomps :: [CoAxBranch] Source

data Role Source

Constructors

Nominal
Representational
Phantom

Instances

Eq Role
Methods (==) :: Role -> Role -> Bool (/=) :: Role -> Role -> Bool
Data Role
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 (TYPE Lifted -> TYPE Lifted) t => (forall d. Data d => c (t d)) -> Maybe (c Role) Source dataCast2 :: Typeable (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) 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 :: (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
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
Methods ppr :: Role -> SDoc Source pprPrec :: Rational -> Role -> SDoc Source
Binary Role
Methods put_ :: BinHandle -> Role -> IO () Source put :: BinHandle -> Role -> IO (Bin Role) Source get :: BinHandle -> IO Role Source

fsFromRole :: Role -> FastString Source

data CoAxiomRule Source

For now, we work only with nominal equality.

Constructors

CoAxiomRule
Fields coaxrName :: FastString coaxrAsmpRoles :: [Role] coaxrRole :: Role coaxrProves :: [Eqn] -> Maybe Eqn coaxrProves returns `Nothing` when it doesn't like the supplied arguments. When this happens in a coercion that means that the coercion is ill-formed, and Core Lint checks for that.

Instances

Eq CoAxiomRule
Methods (==) :: CoAxiomRule -> CoAxiomRule -> Bool (/=) :: CoAxiomRule -> CoAxiomRule -> Bool
Data CoAxiomRule
Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CoAxiomRule -> c CoAxiomRule Source gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CoAxiomRule Source toConstr :: CoAxiomRule -> Constr Source dataTypeOf :: CoAxiomRule -> DataType Source dataCast1 :: Typeable (TYPE Lifted -> TYPE Lifted) t => (forall d. Data d => c (t d)) -> Maybe (c CoAxiomRule) Source dataCast2 :: Typeable (TYPE Lifted -> TYPE Lifted -> TYPE Lifted) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxiomRule) Source gmapT :: (forall b. Data b => b -> b) -> CoAxiomRule -> CoAxiomRule Source gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CoAxiomRule -> r Source gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CoAxiomRule -> r Source gmapQ :: (forall d. Data d => d -> u) -> CoAxiomRule -> [u] Source gmapQi :: Int -> (forall d. Data d => d -> u) -> CoAxiomRule -> u Source gmapM :: Monad m => (forall d. Data d => d -> m d) -> CoAxiomRule -> m CoAxiomRule Source gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CoAxiomRule -> m CoAxiomRule Source gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CoAxiomRule -> m CoAxiomRule Source
Ord CoAxiomRule
Methods compare :: CoAxiomRule -> CoAxiomRule -> Ordering (<) :: CoAxiomRule -> CoAxiomRule -> Bool (<=) :: CoAxiomRule -> CoAxiomRule -> Bool (>) :: CoAxiomRule -> CoAxiomRule -> Bool (>=) :: CoAxiomRule -> CoAxiomRule -> Bool max :: CoAxiomRule -> CoAxiomRule -> CoAxiomRule min :: CoAxiomRule -> CoAxiomRule -> CoAxiomRule
Outputable CoAxiomRule
Methods ppr :: CoAxiomRule -> SDoc Source pprPrec :: Rational -> CoAxiomRule -> SDoc Source
Uniquable CoAxiomRule
Methods getUnique :: CoAxiomRule -> Unique Source

type Eqn = Pair Type Source

A more explicit representation for `t1 ~ t2`.

data BuiltInSynFamily Source

Constructors

BuiltInSynFamily
Fields sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type) sfInteractTop :: [Type] -> Type -> [Eqn] sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [Eqn]

trivialBuiltInFamily :: BuiltInSynFamily Source