Moduleghc-lib-parser-9.14.1.20251220GHC2021

GHC.Core.Coercion.Axiom

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

Synopsis

data BranchFlag
type Branched
type Unbranched
type BranchIndex
newtype Branches
value manyBranches
value unbranched
value fromBranches
value numBranches
value mapAccumBranches
data CoAxiom
data CoAxBranch
value toBranchedAxiom
value toUnbranchedAxiom
value coAxiomName
value coAxiomArity
value coAxiomBranches
value coAxiomTyCon
value isImplicitCoAxiom
value coAxiomNumPats
value coAxiomNthBranch
value coAxiomSingleBranch_maybe
value coAxiomRole
value coAxiomSingleBranch
value coAxBranchTyVars
value coAxBranchCoVars
value coAxBranchRoles
value coAxBranchLHS
value coAxBranchRHS
value coAxBranchSpan
value coAxBranchIncomps
value placeHolderIncomps
data Role
value fsFromRole
data CoAxiomRule
data BuiltInFamRewrite
data BuiltInFamInjectivity
type TypeEqn
value coAxiomRuleArgRoles
value coAxiomRuleRole
value coAxiomRuleBranch_maybe
value isNewtypeAxiomRule_maybe
data BuiltInSynFamily
value trivialBuiltInFamily

Packageghc-lib-parser-9.14.1.20251220
Exports44
LanguageGHC2021
LicenceBSD-3-Clause
SourceAxiom.hs

datadata BranchFlag

typetype Branched = 'Branched

typetype Unbranched = 'Unbranched

typetype BranchIndex = Int

newtypenewtype Branches (br :: BranchFlag)

Constructors

MkBranches
- unMkBranches :: Array BranchIndex CoAxBranch

valuemanyBranches :: [CoAxBranch] -> Branches Branched

valueunbranched :: CoAxBranch -> Branches Unbranched

valuefromBranches :: Branches br -> [CoAxBranch]

valuenumBranches :: Branches br -> Int

valuemapAccumBranches

:: [CoAxBranch] -> CoAxBranch -> CoAxBranch
-> Branches br
-> Branches br

Source#

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

datadata CoAxiom (br :: BranchFlag)

Source#

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

Constructors

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

Instances5Eq, Data, Uniquable, Outputable, NamedThing

Eq (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
Typeable br => Data (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
Uniquable (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
Outputable (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
NamedThing (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom

datadata 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.

Constructors

CoAxBranch
- cab_loc :: SrcSpan
  Location of the defining equation See Note [CoAxiom locations]
- cab_tvs :: [TyVar]
  Bound type variables; not necessarily fresh See Note [CoAxBranch type variables]
- cab_eta_tvs :: [TyVar]
  Eta-reduced tyvars cab_tvs and cab_lhs may be eta-reduced; see Note [Eta reduction for data families]
- cab_cvs :: [CoVar]
  Bound coercion variables Always empty, for now. See Note [Constraints in patterns] in GHC.Tc.TyCl
- cab_roles :: [Role]
  See Note [CoAxBranch roles]
- cab_lhs :: [Type]
  Type patterns to match against
- cab_rhs :: Type
  Right-hand side of the equality See Note [CoAxioms are homogeneous]
- cab_incomps :: [CoAxBranch]
  The previous incompatible branches See Note [Storing compatibility]

Instances2Data, Outputable

Data CoAxBranchDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
Outputable CoAxBranchDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom

valuetoBranchedAxiom :: CoAxiom br -> CoAxiom Branched

valuetoUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched

valuecoAxiomName :: CoAxiom br -> Name

valuecoAxiomArity :: CoAxiom br -> BranchIndex -> Arity

valuecoAxiomBranches :: CoAxiom br -> Branches br

valuecoAxiomTyCon :: CoAxiom br -> TyCon

valueisImplicitCoAxiom :: CoAxiom br -> Bool

valuecoAxiomNumPats :: CoAxiom br -> Int

valuecoAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch

valuecoAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch

valuecoAxiomRole :: CoAxiom br -> Role

valuecoAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch

valuecoAxBranchTyVars :: CoAxBranch -> [TyVar]

valuecoAxBranchCoVars :: CoAxBranch -> [CoVar]

valuecoAxBranchRoles :: CoAxBranch -> [Role]

valuecoAxBranchLHS :: CoAxBranch -> [Type]

valuecoAxBranchRHS :: CoAxBranch -> Type

valuecoAxBranchSpan :: CoAxBranch -> SrcSpan

valuecoAxBranchIncomps :: CoAxBranch -> [CoAxBranch]

valueplaceHolderIncomps :: [CoAxBranch]

datadata Role

Source#

See Note [Roles] in GHC.Core.Coercion

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

Nominal Representational Phantom

Instances7Eq, Data, Ord, NFData, Outputable, Binary, …

Eq RoleDefined in ghc-lib-parser-9.14.1.20251220 · Language.Haskell.Syntax.Basic
Data RoleDefined in ghc-lib-parser-9.14.1.20251220 · Language.Haskell.Syntax.Basic
Ord RoleDefined in ghc-lib-parser-9.14.1.20251220 · Language.Haskell.Syntax.Basic
NFData RoleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom · orphan
Outputable RoleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom · orphan
Binary RoleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom · orphan
type Anno (Maybe Role) = EpAnnCODefined in ghc-lib-parser-9.14.1.20251220 · GHC.Hs.Decls · orphan

valuefsFromRole :: Role -> FastString

datadata CoAxiomRule

Source#

CoAxiomRule describes a built-in axiom, one that we assume to be true See Note [CoAxiomRule]

Constructors

BuiltInFamRew BuiltInFamRewrite
BuiltInFamInj BuiltInFamInjectivity
BranchedAxiom (CoAxiom Branched) BranchIndex
UnbranchedAxiom (CoAxiom Unbranched)

Instances3Eq, Data, Outputable

Eq CoAxiomRuleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
Data CoAxiomRuleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
Outputable CoAxiomRuleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom

datadata BuiltInFamRewrite

Constructors

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

datadata BuiltInFamInjectivity

Constructors

BIF_Interact
- bifinj_name :: FastString
- bifinj_axr :: CoAxiomRule
- bifinj_proves :: TypeEqn -> Maybe TypeEqn
  Always unary: just one TypeEqn argument Returns Nothing when it doesn't like the supplied argument. When this happens in a coercion that means that the coercion is ill-formed, and Core Lint checks for that.

typetype TypeEqn = Pair Type

Source#

A more explicit representation for `t1 ~ t2`.

valuecoAxiomRuleArgRoles :: CoAxiomRule -> [Role]

valuecoAxiomRuleRole :: CoAxiomRule -> Role

valuecoAxiomRuleBranch_maybe :: CoAxiomRule -> Maybe (TyCon, Role, CoAxBranch)

valueisNewtypeAxiomRule_maybe :: CoAxiomRule -> Maybe (TyCon, CoAxBranch)

datadata BuiltInSynFamily

Constructors

BuiltInSynFamily
- sfMatchFam :: [BuiltInFamRewrite]
- sfInteract :: [BuiltInFamInjectivity]

valuetrivialBuiltInFamily :: BuiltInSynFamily

Orphan instances

3 instances