Moduleghc-9.10.3GHC2021
GHC.Core.Coercion.Axiom
Module for coercion axioms, used to represent type family instances and newtypes
- 11 types
- 27 values
- Packageghc-9.10.3
- Exports38
- 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, NamedThing, Outputable, Uniquable
Eq (CoAxiom br)Defined in ghc-9.10.3 · GHC.Core.Coercion.AxiomTypeable br => Data (CoAxiom br)Defined in ghc-9.10.3 · GHC.Core.Coercion.AxiomNamedThing (CoAxiom br)Defined in ghc-9.10.3 · GHC.Core.Coercion.AxiomOutputable (CoAxiom br)Defined in ghc-9.10.3 · GHC.Core.Coercion.AxiomUniquable (CoAxiom br)Defined in ghc-9.10.3 · 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-9.10.3 · GHC.Core.Coercion.AxiomOutputable CoAxBranchDefined in ghc-9.10.3 · 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, Outputable, Binary, Anno, …
Eq RoleDefined in ghc-9.10.3 · Language.Haskell.Syntax.BasicData RoleDefined in ghc-9.10.3 · Language.Haskell.Syntax.BasicOrd RoleDefined in ghc-9.10.3 · Language.Haskell.Syntax.BasicOutputable RoleDefined in ghc-9.10.3 · GHC.Core.Coercion.Axiom · orphanBinary RoleDefined in ghc-9.10.3 · GHC.Core.Coercion.Axiom · orphantype Anno (Maybe Role) = EpAnnCODefined in ghc-9.10.3 · GHC.Hs.Decls · orphantype Anno (Maybe Role) = EpAnnCODefined in ghc-9.10.3 · GHC.Hs.Decls · orphan
For now, we work only with nominal equality.
Constructors
CoAxiomRulecoaxrName :: FastStringcoaxrAsmpRoles :: [Role]coaxrRole :: RolecoaxrProves :: [TypeEqn] -> Maybe TypeEqncoaxrProves returns
Nothingwhen 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.
Instances5Eq, Data, Ord, Outputable, Uniquable
Eq CoAxiomRuleDefined in ghc-9.10.3 · GHC.Core.Coercion.AxiomData CoAxiomRuleDefined in ghc-9.10.3 · GHC.Core.Coercion.AxiomOrd CoAxiomRuleDefined in ghc-9.10.3 · GHC.Core.Coercion.AxiomOutputable CoAxiomRuleDefined in ghc-9.10.3 · GHC.Core.Coercion.AxiomUniquable CoAxiomRuleDefined in ghc-9.10.3 · GHC.Core.Coercion.Axiom
A more explicit representation for `t1 ~ t2`.
Constructors
BuiltInSynFamilysfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)sfInteractTop :: [Type] -> Type -> [TypeEqn]sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]