Safe Haskell	Safe-Inferred
Language	Haskell2010

GHC.Core.FamInstEnv

Contents

CoAxioms

Synopsis

data FamInst = 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
}
data FamFlavor
- = 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
emptyFamInstEnv :: FamInstEnv
emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
unionFamInstEnv :: FamInstEnv -> FamInstEnv -> FamInstEnv
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
famInstEnvElts :: FamInstEnv -> [FamInst]
famInstEnvSize :: FamInstEnv -> Int
familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [FamInst]
familyNameInstances :: (FamInstEnv, FamInstEnv) -> Name -> [FamInst]
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
data FamInstMatch = FamInstMatch {
- fim_instance :: FamInst
- fim_tys :: [Type]
- fim_cos :: [Coercion]
}
lookupFamInstEnv :: FamInstEnvs -> TyCon -> [Type] -> [FamInstMatch]
lookupFamInstEnvConflicts :: FamInstEnvs -> FamInst -> [FamInst]
lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
apartnessCheck :: [Type] -> CoAxBranch -> Bool
data InjectivityCheckResult
- = InjectivityAccepted
- | InjectivityUnified CoAxBranch CoAxBranch
lookupFamInstEnvInjectivityConflicts :: [Bool] -> FamInstEnvs -> FamInst -> [CoAxBranch]
injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult
topNormaliseType :: FamInstEnvs -> Type -> Type
topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction
normaliseType :: FamInstEnvs -> Role -> Type -> Reduction
normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> Reduction
topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type] -> Maybe HetReduction
reduceTyFamApp_maybe :: FamInstEnvs -> Role -> TyCon -> [Type] -> Maybe Reduction

Documentation

data FamInst Source #

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

Instances details

NamedThing FamInst Source #
Instance details Defined in GHC.Core.FamInstEnv Methods getOccName :: FamInst -> OccName Source # getName :: FamInst -> Name Source #
Outputable FamInst Source #
Instance details Defined in GHC.Core.FamInstEnv Methods ppr :: FamInst -> SDoc Source #

data FamFlavor Source #

Constructors

SynFamilyInst
DataFamilyInst TyCon

famInstAxiom :: FamInst -> CoAxiom Unbranched Source #

famInstTyCon :: FamInst -> TyCon Source #

famInstRHS :: FamInst -> Type Source #

famInstsRepTyCons :: [FamInst] -> [TyCon] Source #

famInstRepTyCon_maybe :: FamInst -> Maybe TyCon Source #

dataFamInstRepTyCon :: FamInst -> TyCon Source #

pprFamInst :: FamInst -> SDoc Source #

pprFamInsts :: [FamInst] -> SDoc Source #

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

type FamInstEnvs = (FamInstEnv, FamInstEnv) Source #

data FamInstEnv Source #

Instances

Instances details

Outputable FamInstEnv Source #
Instance details Defined in GHC.Core.FamInstEnv Methods ppr :: FamInstEnv -> SDoc Source #

emptyFamInstEnv :: FamInstEnv Source #

emptyFamInstEnvs :: (FamInstEnv, FamInstEnv) Source #

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 Source #

Makes no particular effort to detect conflicts.

extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv Source #

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

famInstEnvElts :: FamInstEnv -> [FamInst] Source #

famInstEnvSize :: FamInstEnv -> Int Source #

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

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

CoAxioms

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

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

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

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

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

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 Source #

Constructors

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

Instances

Instances details

Outputable FamInstMatch Source #
Instance details Defined in GHC.Core.FamInstEnv Methods ppr :: FamInstMatch -> SDoc Source #

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

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

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

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

apartnessCheck Source #

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 Source #

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] Source #

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 Source #

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

topNormaliseType :: FamInstEnvs -> Type -> Type Source #

topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe Reduction Source #

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 Source #

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

topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type] -> Maybe HetReduction Source #

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 Source #