GHC.Core.FamInstEnv

Documentation

data FamInst

Constructors

FamInst

Fields

• 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

Instances

NamedThing FamInst

Defined in GHC.Core.FamInstEnv

Methods

getOccName :: FamInst -> OccName

getName :: FamInst -> Name

Outputable FamInst

Defined in GHC.Core.FamInstEnv

Methods

ppr :: FamInst -> SDoc

data FamFlavor

Constructors

SynFamilyInst

DataFamilyInst TyCon

famInstAxiom :: FamInst -> CoAxiom Unbranched

famInstTyCon :: FamInst -> TyCon

famInstRHS :: FamInst -> Type

famInstsRepTyCons :: [FamInst] -> [TyCon]

famInstRepTyCon_maybe :: FamInst -> Maybe TyCon

dataFamInstRepTyCon :: FamInst -> TyCon

pprFamInst :: FamInst -> SDoc

pprFamInsts :: [FamInst] -> SDoc

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

type FamInstEnvs = (FamInstEnv, FamInstEnv)

data FamInstEnv

Instances

Outputable FamInstEnv

Defined in GHC.Core.FamInstEnv

Methods

ppr :: FamInstEnv -> SDoc

emptyFamInstEnv :: FamInstEnv

emptyFamInstEnvs :: (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)

unionFamInstEnv :: FamInstEnv -> FamInstEnv -> FamInstEnv

Makes no particular effort to detect conflicts.

extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv

extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv

famInstEnvElts :: FamInstEnv -> [FamInst]

famInstEnvSize :: FamInstEnv -> Int

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

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

CoAxioms

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

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

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

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

mkNewTypeCoAxiom :: 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.

data FamInstMatch

Constructors

FamInstMatch

Fields

• fim_instance :: FamInst
• fim_tys :: [Type]
• fim_cos :: [Coercion]

Instances

Outputable FamInstMatch

Defined in GHC.Core.FamInstEnv

Methods

ppr :: FamInstMatch -> SDoc

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

lookupFamInstEnvConflicts :: FamInstEnvs -> FamInst -> [FamInst]

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

isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool

apartnessCheck

Arguments

:: [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.

data 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 overlpapped (in which case it is OK if they don't unify). Constructor stores axioms after unification.

lookupFamInstEnvInjectivityConflicts :: [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).

injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult

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

topNormaliseType :: FamInstEnvs -> Type -> Type

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

normaliseType :: FamInstEnvs -> Role -> Type -> Reduction

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

topReduceTyFamApp_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

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