| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
FamInst
Contents
- type FamInstEnvs = (FamInstEnv, FamInstEnv)
- tcGetFamInstEnvs :: TcM FamInstEnvs
- checkFamInstConsistency :: [Module] -> [Module] -> TcM ()
- tcExtendLocalFamInstEnv :: [FamInst] -> TcM a -> TcM a
- tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType] -> (TyCon, [TcType], Coercion)
- tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType] -> Maybe (TyCon, [TcType], Coercion)
- tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion)
- tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs -> GlobalRdrEnv -> Type -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type)
- newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst
- makeInjectivityErrors :: CoAxiom br -> CoAxBranch -> [Bool] -> [CoAxBranch] -> [(SDoc, SrcSpan)]
Documentation
type FamInstEnvs = (FamInstEnv, FamInstEnv) Source #
tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType] -> (TyCon, [TcType], Coercion) Source #
Like tcLookupDataFamInst_maybe, but returns the arguments back if
there is no data family to unwrap.
Returns a Representational coercion
tcLookupDataFamInst_maybe :: FamInstEnvs -> TyCon -> [TcType] -> Maybe (TyCon, [TcType], Coercion) Source #
Converts a data family type (eg F [a]) to its representation type (eg FList a) and returns a coercion between the two: co :: F [a] ~R FList a.
tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion) Source #
If co :: T ts ~ rep_ty then:
instNewTyCon_maybe T ts = Just (rep_ty, co)
Checks for a newtype, and for being saturated Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion
tcTopNormaliseNewTypeTF_maybe :: FamInstEnvs -> GlobalRdrEnv -> Type -> Maybe ((Bag GlobalRdrElt, TcCoercion), Type) Source #
tcTopNormaliseNewTypeTF_maybe gets rid of top-level newtypes,
potentially looking through newtype instances.
It is only used by the type inference engine (specifically, when solving representational equality), and hence it is careful to unwrap only if the relevant data constructor is in scope. That's why it get a GlobalRdrEnv argument.
It is careful not to unwrap data/newtype instances if it can't continue unwrapping. Such care is necessary for proper error messages.
It does not look through type families. It does not normalise arguments to a tycon.
If the result is Just (rep_ty, (co, gres), rep_ty), then co : ty ~R rep_ty gres are the GREs for the data constructors that had to be in scope
newFamInst :: FamFlavor -> CoAxiom Unbranched -> TcRnIf gbl lcl FamInst Source #
Injectivity
makeInjectivityErrors Source #
Arguments
| :: CoAxiom br | Type family for which we generate errors |
| -> CoAxBranch | Currently checked equation (represented by axiom) |
| -> [Bool] | Injectivity annotation |
| -> [CoAxBranch] | List of injectivity conflicts |
| -> [(SDoc, SrcSpan)] |
Build a list of injectivity errors together with their source locations.