Safe Haskell | None |
---|---|
Language | GHC2021 |
Module for coercion axioms, used to represent type family instances and newtypes
Synopsis
- data BranchFlag
- type Branched = 'Branched
- type Unbranched = 'Unbranched
- type BranchIndex = Int
- newtype Branches (br :: BranchFlag) = MkBranches {}
- manyBranches :: [CoAxBranch] -> Branches Branched
- unbranched :: CoAxBranch -> Branches Unbranched
- fromBranches :: forall (br :: BranchFlag). Branches br -> [CoAxBranch]
- numBranches :: forall (br :: BranchFlag). Branches br -> Int
- mapAccumBranches :: forall (br :: BranchFlag). ([CoAxBranch] -> CoAxBranch -> CoAxBranch) -> Branches br -> Branches br
- data CoAxiom (br :: BranchFlag) = CoAxiom {
- 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
- data CoAxBranch = CoAxBranch {}
- toBranchedAxiom :: forall (br :: BranchFlag). CoAxiom br -> CoAxiom Branched
- toUnbranchedAxiom :: forall (br :: BranchFlag). CoAxiom br -> CoAxiom Unbranched
- coAxiomName :: forall (br :: BranchFlag). CoAxiom br -> Name
- coAxiomArity :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> Arity
- coAxiomBranches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
- coAxiomTyCon :: forall (br :: BranchFlag). CoAxiom br -> TyCon
- isImplicitCoAxiom :: forall (br :: BranchFlag). CoAxiom br -> Bool
- coAxiomNumPats :: forall (br :: BranchFlag). CoAxiom br -> Int
- coAxiomNthBranch :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
- coAxiomSingleBranch_maybe :: forall (br :: BranchFlag). CoAxiom br -> Maybe CoAxBranch
- coAxiomRole :: forall (br :: BranchFlag). CoAxiom br -> Role
- coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
- coAxBranchTyVars :: CoAxBranch -> [TyVar]
- coAxBranchCoVars :: CoAxBranch -> [CoVar]
- coAxBranchRoles :: CoAxBranch -> [Role]
- coAxBranchLHS :: CoAxBranch -> [Type]
- coAxBranchRHS :: CoAxBranch -> Type
- coAxBranchSpan :: CoAxBranch -> SrcSpan
- coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
- placeHolderIncomps :: [CoAxBranch]
- data Role
- fsFromRole :: Role -> FastString
- data CoAxiomRule
- data BuiltInFamRewrite = BIF_Rewrite {
- bifrw_name :: FastString
- bifrw_axr :: CoAxiomRule
- bifrw_fam_tc :: TyCon
- bifrw_arity :: Arity
- bifrw_match :: [Type] -> Maybe ([Type], Type)
- bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
- data BuiltInFamInjectivity = BIF_Interact {}
- type TypeEqn = Pair Type
- coAxiomRuleArgRoles :: CoAxiomRule -> [Role]
- coAxiomRuleRole :: CoAxiomRule -> Role
- coAxiomRuleBranch_maybe :: CoAxiomRule -> Maybe (TyCon, Role, CoAxBranch)
- isNewtypeAxiomRule_maybe :: CoAxiomRule -> Maybe (TyCon, CoAxBranch)
- data BuiltInSynFamily = BuiltInSynFamily {}
- trivialBuiltInFamily :: BuiltInSynFamily
Documentation
data BranchFlag Source #
type Unbranched = 'Unbranched Source #
type BranchIndex = Int Source #
newtype Branches (br :: BranchFlag) Source #
manyBranches :: [CoAxBranch] -> Branches Branched Source #
fromBranches :: forall (br :: BranchFlag). Branches br -> [CoAxBranch] Source #
numBranches :: forall (br :: BranchFlag). Branches br -> Int Source #
mapAccumBranches :: forall (br :: BranchFlag). ([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 :: BranchFlag) Source #
A CoAxiom
is a "coercion constructor", i.e. a named equality axiom.
CoAxiom | |
|
Instances
NamedThing (CoAxiom br) Source # | |
Uniquable (CoAxiom br) Source # | |
Outputable (CoAxiom br) Source # | |
Typeable br => Data (CoAxiom br) Source # | |
Defined in GHC.Core.Coercion.Axiom 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) # | |
Eq (CoAxiom br) Source # | |
data CoAxBranch Source #
A branch of a coercion axiom, which provides the evidence for unwrapping a newtype or a type-family reduction step using a single equation.
CoAxBranch | |
|
Instances
Outputable CoAxBranch Source # | |
Defined in GHC.Core.Coercion.Axiom ppr :: CoAxBranch -> SDoc Source # | |
Data CoAxBranch Source # | |
Defined in GHC.Core.Coercion.Axiom 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 # |
toBranchedAxiom :: forall (br :: BranchFlag). CoAxiom br -> CoAxiom Branched Source #
toUnbranchedAxiom :: forall (br :: BranchFlag). CoAxiom br -> CoAxiom Unbranched Source #
coAxiomName :: forall (br :: BranchFlag). CoAxiom br -> Name Source #
coAxiomArity :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> Arity Source #
coAxiomBranches :: forall (br :: BranchFlag). CoAxiom br -> Branches br Source #
coAxiomTyCon :: forall (br :: BranchFlag). CoAxiom br -> TyCon Source #
isImplicitCoAxiom :: forall (br :: BranchFlag). CoAxiom br -> Bool Source #
coAxiomNumPats :: forall (br :: BranchFlag). CoAxiom br -> Int Source #
coAxiomNthBranch :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch Source #
coAxiomSingleBranch_maybe :: forall (br :: BranchFlag). CoAxiom br -> Maybe CoAxBranch Source #
coAxiomRole :: forall (br :: BranchFlag). CoAxiom br -> Role 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 #
See Note [Roles] in GHC.Core.Coercion
Order of constructors matters: the Ord instance coincides with the *super*typing relation on roles.
Instances
Binary Role Source # | |
Outputable Role Source # | |
Data Role Source # | |
Defined in Language.Haskell.Syntax.Basic 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 # 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 # | |
Eq Role Source # | |
Ord Role Source # | |
type Anno (Maybe Role) Source # | |
Defined in GHC.Hs.Decls |
fsFromRole :: Role -> FastString Source #
data CoAxiomRule Source #
CoAxiomRule describes a built-in axiom, one that we assume to be true See Note [CoAxiomRule]
BuiltInFamRew BuiltInFamRewrite | |
BuiltInFamInj BuiltInFamInjectivity | |
BranchedAxiom (CoAxiom Branched) BranchIndex | |
UnbranchedAxiom (CoAxiom Unbranched) |
Instances
Outputable CoAxiomRule Source # | |
Defined in GHC.Core.Coercion.Axiom ppr :: CoAxiomRule -> SDoc Source # | |
Data CoAxiomRule Source # | |
Defined in GHC.Core.Coercion.Axiom 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 # | |
Eq CoAxiomRule Source # | |
Defined in GHC.Core.Coercion.Axiom (==) :: CoAxiomRule -> CoAxiomRule -> Bool # (/=) :: CoAxiomRule -> CoAxiomRule -> Bool # |
data BuiltInFamRewrite Source #
BIF_Rewrite | |
|
data BuiltInFamInjectivity Source #
BIF_Interact | |
|
coAxiomRuleArgRoles :: CoAxiomRule -> [Role] Source #
coAxiomRuleRole :: CoAxiomRule -> Role Source #
coAxiomRuleBranch_maybe :: CoAxiomRule -> Maybe (TyCon, Role, CoAxBranch) Source #
data BuiltInSynFamily Source #