Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
GHC.Core.FamInstEnv
Contents
Synopsis
- data FamInst = FamInst {}
- data FamFlavor
- 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)
- type FamInstEnv = UniqDFM TyCon FamilyInstEnv
- emptyFamInstEnv :: FamInstEnv
- emptyFamInstEnvs :: (FamInstEnv, FamInstEnv)
- extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv
- extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv
- famInstEnvElts :: FamInstEnv -> [FamInst]
- famInstEnvSize :: FamInstEnv -> Int
- familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [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 {}
- lookupFamInstEnv :: FamInstEnvs -> TyCon -> [Type] -> [FamInstMatch]
- lookupFamInstEnvConflicts :: FamInstEnvs -> FamInst -> [FamInstMatch]
- lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst]
- isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool
- apartnessCheck :: [Type] -> CoAxBranch -> Bool
- data InjectivityCheckResult
- lookupFamInstEnvInjectivityConflicts :: [Bool] -> FamInstEnvs -> FamInst -> [CoAxBranch]
- injectiveBranches :: [Bool] -> CoAxBranch -> CoAxBranch -> InjectivityCheckResult
- topNormaliseType :: FamInstEnvs -> Type -> Type
- topNormaliseType_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type)
- normaliseType :: FamInstEnvs -> Role -> Type -> (Coercion, Type)
- normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type)
- topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Coercion, Type, MCoercion)
- reduceTyFamApp_maybe :: FamInstEnvs -> Role -> TyCon -> [Type] -> Maybe (Coercion, Type)
Documentation
Constructors
FamInst | |
Instances
NamedThing FamInst # | |
Defined in GHC.Core.FamInstEnv | |
Outputable FamInst # | |
Defined in GHC.Core.FamInstEnv |
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) #
type FamInstEnv = UniqDFM TyCon FamilyInstEnv #
extendFamInstEnv :: FamInstEnv -> FamInst -> FamInstEnv #
extendFamInstEnvList :: FamInstEnv -> [FamInst] -> FamInstEnv #
famInstEnvElts :: FamInstEnv -> [FamInst] #
famInstEnvSize :: FamInstEnv -> Int #
familyInstances :: (FamInstEnv, FamInstEnv) -> TyCon -> [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 #
data FamInstMatch #
Constructors
FamInstMatch | |
Instances
Outputable FamInstMatch # | |
Defined in GHC.Core.FamInstEnv Methods ppr :: FamInstMatch -> SDoc # |
lookupFamInstEnv :: FamInstEnvs -> TyCon -> [Type] -> [FamInstMatch] #
lookupFamInstEnvConflicts :: FamInstEnvs -> FamInst -> [FamInstMatch] #
lookupFamInstEnvByTyCon :: FamInstEnvs -> TyCon -> [FamInst] #
isDominatedBy :: CoAxBranch -> [CoAxBranch] -> Bool #
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 (Coercion, Type) #
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 -> (Coercion, Type) #
normaliseTcApp :: FamInstEnvs -> Role -> TyCon -> [Type] -> (Coercion, Type) #
topReduceTyFamApp_maybe :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Coercion, Type, MCoercion) #
Try to simplify a type-family application, by *one* step If topReduceTyFamApp_maybe env r F tys = Just (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 (Coercion, Type) #