Moduleghc-9.10.3GHC2021

GHC.Core.FamInstEnv

6 types
39 values

Packageghc-9.10.3
Exports45
LanguageGHC2021
LicenceBSD-3-Clause
SourceFamInstEnv.hs

datadata FamInst

Constructors

FamInst
- fi_axiom :: CoAxiom Unbranched
- fi_flavor :: FamFlavor
- fi_fam :: Name
- fi_tcs :: [RoughMatchTc]
- fi_tvs :: [TyVar]
- fi_cvs :: [CoVar]
- fi_tys :: [Type]
- fi_rhs :: Type
- fi_orphan :: IsOrphan

Instances2NamedThing, Outputable

NamedThing FamInstDefined in ghc-9.10.3 · GHC.Core.FamInstEnv
Outputable FamInstDefined in ghc-9.10.3 · GHC.Core.FamInstEnv

datadata FamFlavor

Constructors

SynFamilyInst
DataFamilyInst TyCon

valuefamInstAxiom :: FamInst -> CoAxiom Unbranched

valuefamInstTyCon :: FamInst -> TyCon

valuefamInstRHS :: FamInst -> Type

valuefamInstsRepTyCons :: [FamInst] -> [TyCon]

valuefamInstRepTyCon_maybe :: FamInst -> Maybe TyCon

valuedataFamInstRepTyCon :: FamInst -> TyCon

valuepprFamInst :: FamInst -> SDoc

valuepprFamInsts :: [FamInst] -> SDoc

valueorphNamesOfFamInst :: FamInst -> NameSet

valuemkImportedFamInst

:: Name
-> [RoughMatchTc]
-> CoAxiom Unbranched
-> IsOrphan
-> FamInst

valuemkLocalFamInst

:: FamFlavor
-> CoAxiom Unbranched
-> [TyVar]
-> [CoVar]
-> [Type]
-> Type
-> FamInst

typetype FamInstEnvs = (FamInstEnv, FamInstEnv)

datadata FamInstEnv

Instances1Outputable

Outputable FamInstEnvDefined in ghc-9.10.3 · GHC.Core.FamInstEnv

valueemptyFamInstEnv :: FamInstEnv

valueemptyFamInstEnvs :: (FamInstEnv, FamInstEnv)

Create a FamInstEnv from Name indices. INVARIANTS: * The fs_tvs are distinct in each FamInst of a range value of the map (so we can safely unify them)

valueunionFamInstEnv :: FamInstEnv -> FamInstEnv -> FamInstEnv

Makes no particular effort to detect conflicts.

valueextendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv

valueextendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv

valuefamInstEnvElts :: FamInstEnv -> [FamInst]

valuefamInstEnvSize :: FamInstEnv -> Int

valuefamilyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]

valuefamilyNameInstances :: (FamInstEnv, FamInstEnv) -> Name -> [FamInst]

CoAxioms

21 declarations

valuemkCoAxBranch

:: [TyVar]
-> [TyVar]
-> [CoVar]
-> [Type]
-> Type
-> [Role]
-> SrcSpan
-> CoAxBranch

valuemkBranchedCoAxiom :: Name -> TyCon -> [CoAxBranch] -> CoAxiom Branched

valuemkUnbranchedCoAxiom :: Name -> TyCon -> CoAxBranch -> CoAxiom Unbranched

valuemkSingleCoAxiom

:: Role
-> Name
-> [TyVar]
-> [TyVar]
-> [CoVar]
-> TyCon
-> [Type]
-> Type
-> CoAxiom Unbranched

valuemkNewTypeCoAxiom

:: Name
-> TyCon
-> [TyVar]
-> [Role]
-> Type
-> CoAxiom Unbranched

Create a coercion constructor (axiom) suitable for the given newtype TyCon. The Name should be that of a new coercion CoAxiom, the TyVars the arguments expected by the newtype and the type the appropriate right hand side of the newtype, with the free variables a subset of those TyVars.

datadata FamInstMatch

Constructors

FamInstMatch
- fim_instance :: FamInst
- fim_tys :: [Type]
- fim_cos :: [Coercion]

Instances1Outputable

Outputable FamInstMatchDefined in ghc-9.10.3 · GHC.Core.FamInstEnv

valuelookupFamInstEnv :: FamInstEnvs -> TyCon -> [Type] -> [FamInstMatch]

valuelookupFamInstEnvConflicts :: FamInstEnvs -> FamInst -> [FamInst]

valuelookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]

valueisDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool

valueapartnessCheck

:: [Type]
flattened target arguments. Make sure they're flattened! See Note [Flattening type-family applications when matching instances] in GHC.Core.Unify.
-> CoAxBranch
the candidate equation we wish to use Precondition: this matches the target
-> Bool
True = equation can fire

Do an apartness check, as described in the "Closed Type Families" paper (POPL '14). This should be used when determining if an equation (CoAxBranch) of a closed type family can be used to reduce a certain target type family application.

valuecompatibleBranches :: CoAxBranch -> CoAxBranch -> Bool

datadata InjectivityCheckResult

Result of testing two type family equations for injectiviy.

Constructors

InjectivityAccepted
Either RHSs are distinct or unification of RHSs leads to unification of LHSs
InjectivityUnified CoAxBranch CoAxBranch
RHSs unify but LHSs don't unify under that substitution. Relevant for closed type families where equation after unification might be overlapped (in which case it is OK if they don't unify). Constructor stores axioms after unification.

valuelookupFamInstEnvInjectivityConflicts

:: [Bool]
-> FamInstEnvs
-> FamInst
-> [CoAxBranch]

Check whether an open type family equation can be added to already existing instance environment without causing conflicts with supplied injectivity annotations. Returns list of conflicting axioms (type instance declarations).

valueinjectiveBranches

Check whether two type family axioms don't violate injectivity annotation.

valuetopNormaliseType :: FamInstEnvs -> Type -> Type

valuetopNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction

Get rid of *outermost* (or toplevel) * type function redex * data family redex * newtypes returning an appropriate Representational coercion. Specifically, if topNormaliseType_maybe env ty = Just (co, ty') then (a) co :: ty ~R ty' (b) ty' is not a newtype, and is not a type-family or data-family redex

However, ty' can be something like (Maybe (F ty)), where (F ty) is a redex.

Always operates homogeneously: the returned type has the same kind as the original type, and the returned coercion is always homogeneous.

valuenormaliseType :: FamInstEnvs -> Role -> Type -> Reduction

valuenormaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> Reduction

valuetopReduceTyFamApp_maybe

:: FamInstEnvs
-> TyCon
-> [Type]
-> Maybe HetReduction

Try to simplify a type-family application, by *one* step If topReduceTyFamApp_maybe env r F tys = Just (HetReduction (Reduction co rhs) res_co) then co :: F tys ~R# rhs res_co :: typeKind(F tys) ~ typeKind(rhs) Type families and data families; always Representational role

valuereduceTyFamApp_maybe

:: FamInstEnvs
-> Role
-> TyCon
-> [Type]
-> Maybe Reduction