ghc-8.4.3: The GHC API

Safe HaskellNone
LanguageHaskell2010

FamInstEnv

Contents

Synopsis

Documentation

data FamInst Source #

Constructors

FamInst 
Instances
Outputable FamInst Source # 
Instance details

Defined in FamInstEnv

NamedThing FamInst Source # 
Instance details

Defined in FamInstEnv

type FamInstEnv = UniqDFM FamilyInstEnv Source #

CoAxioms

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 
Instances
Outputable FamInstMatch Source # 
Instance details

Defined in FamInstEnv

apartnessCheck Source #

Arguments

:: [Type]

flattened target arguments. Make sure they're flattened! See Note [Flattening]. (NB: This "flat" is a different "flat" than is used in TcFlatten.)

-> 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_maybe :: FamInstEnvs -> Type -> Maybe (Coercion, Type) 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.

normaliseTcArgs Source #

Arguments

:: FamInstEnvs

env't with family instances

-> Role

desired role of output coercion

-> TyCon

tc

-> [Type]

tys

-> (Coercion, [Type])

co :: tc tys ~ tc new_tys

Normalise arguments to a tycon