Moduleghc-lib-parser-9.14.1.20251220GHC2021
GHC.Core.Coercion.Axiom
Module for coercion axioms, used to represent type family instances and newtypes
- 13 types
- 31 values
- Packageghc-lib-parser-9.14.1.20251220
- Exports44
- LanguageGHC2021
- LicenceBSD-3-Clause
- SourceAxiom.hs
Constructors
The [CoAxBranch] passed into the mapping function is a list of
all previous branches, reversed
A CoAxiom is a "coercion constructor", i.e. a named equality axiom.
Constructors
CoAxiomco_ax_unique :: Uniqueco_ax_name :: Nameco_ax_role :: Roleco_ax_tc :: TyConco_ax_branches :: Branches brco_ax_implicit :: Bool
Instances5Eq, Data, Uniquable, Outputable, NamedThing
Eq (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.AxiomTypeable br => Data (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.AxiomUniquable (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.AxiomOutputable (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.AxiomNamedThing (CoAxiom br)Defined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
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
CoAxBranchcab_loc :: SrcSpanLocation 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 :: TypeRight-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.AxiomOutputable CoAxBranchDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
See Note [Roles] in GHC.Core.Coercion
Order of constructors matters: the Ord instance coincides with the *super*typing relation on roles.
Instances7Eq, Data, Ord, NFData, Outputable, Binary, …
Eq RoleDefined in ghc-lib-parser-9.14.1.20251220 · Language.Haskell.Syntax.BasicData RoleDefined in ghc-lib-parser-9.14.1.20251220 · Language.Haskell.Syntax.BasicOrd RoleDefined in ghc-lib-parser-9.14.1.20251220 · Language.Haskell.Syntax.BasicNFData RoleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom · orphanOutputable RoleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom · orphanBinary RoleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom · orphantype Anno (Maybe Role) = EpAnnCODefined in ghc-lib-parser-9.14.1.20251220 · GHC.Hs.Decls · orphan
CoAxiomRule describes a built-in axiom, one that we assume to be true See Note [CoAxiomRule]
Instances3Eq, Data, Outputable
Eq CoAxiomRuleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.AxiomData CoAxiomRuleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.AxiomOutputable CoAxiomRuleDefined in ghc-lib-parser-9.14.1.20251220 · GHC.Core.Coercion.Axiom
Constructors
BIF_Rewritebifrw_name :: FastStringbifrw_axr :: CoAxiomRulebifrw_fam_tc :: TyConbifrw_arity :: Aritybifrw_match :: [Type] -> Maybe ([Type], Type)bifrw_proves :: [TypeEqn] -> Maybe TypeEqn
Constructors
BIF_Interactbifinj_name :: FastStringbifinj_axr :: CoAxiomRulebifinj_proves :: TypeEqn -> Maybe TypeEqnAlways unary: just one TypeEqn argument Returns
Nothingwhen 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.
A more explicit representation for `t1 ~ t2`.