| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
TcValidity
- data Rank
- data UserTypeCtxt
- = FunSigCtxt Name Bool
- | InfSigCtxt Name
- | ExprSigCtxt
- | TypeAppCtxt
- | ConArgCtxt Name
- | TySynCtxt Name
- | PatSynBuilderCtxt Name
- | PatSigCtxt
- | RuleSigCtxt Name
- | ResSigCtxt
- | ForSigCtxt Name
- | DefaultDeclCtxt
- | InstDeclCtxt
- | SpecInstCtxt
- | ThBrackCtxt
- | GenSigCtxt
- | GhciCtxt
- | ClassSCCtxt Name
- | SigmaCtxt
- | DataTyCtxt Name
- checkValidType :: UserTypeCtxt -> Type -> TcM ()
- checkValidMonoType :: Type -> TcM ()
- data ContextKind
- expectedKindInCtxt :: UserTypeCtxt -> ContextKind
- checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()
- checkValidFamPats :: Maybe ClsInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> TcM ()
- checkValidInstance :: UserTypeCtxt -> LHsSigType Name -> Type -> TcM ([TyVar], ThetaType, Class, [Type])
- validDerivPred :: TyVarSet -> PredType -> Bool
- checkInstTermination :: [TcType] -> ThetaType -> TcM ()
- type ClsInfo = (Class, VarEnv Type)
- checkValidCoAxiom :: CoAxiom Branched -> TcM ()
- checkValidCoAxBranch :: Maybe ClsInfo -> TyCon -> CoAxBranch -> TcM ()
- checkValidTyFamEqn :: Maybe ClsInfo -> TyCon -> [TyVar] -> [CoVar] -> [Type] -> Type -> SrcSpan -> TcM ()
- arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
- badATErr :: Name -> Name -> SDoc
- checkValidTelescope :: SDoc -> [TyVar] -> SDoc -> TcM ()
- checkZonkValidTelescope :: SDoc -> [TyVar] -> SDoc -> TcM [TyVar]
- checkValidInferredKinds :: [TyVar] -> TyVarSet -> SDoc -> TcM ()
Documentation
data UserTypeCtxt Source #
checkValidType :: UserTypeCtxt -> Type -> TcM () Source #
checkValidMonoType :: Type -> TcM () Source #
data ContextKind Source #
The kind expected in a certain context.
Constructors
| TheKind Kind | a specific kind |
| AnythingKind | any kind will do |
| OpenKind | something of the form |
checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM () Source #
checkValidInstance :: UserTypeCtxt -> LHsSigType Name -> Type -> TcM ([TyVar], ThetaType, Class, [Type]) Source #
type ClsInfo = (Class, VarEnv Type) Source #
Extra information needed when type-checking associated types. The Class is
the enclosing class, and the VarEnv Type maps class variables to their
instance types.
checkValidCoAxBranch :: Maybe ClsInfo -> TyCon -> CoAxBranch -> TcM () Source #
Arguments
| :: Maybe ClsInfo | |
| -> TyCon | of the type family |
| -> [TyVar] | bound tyvars in the equation |
| -> [CoVar] | bound covars in the equation |
| -> [Type] | type patterns |
| -> Type | rhs |
| -> SrcSpan | |
| -> TcM () |
Do validity checks on a type family equation, including consistency with any enclosing class instance head, termination, and lack of polytypes.
checkValidTelescope :: SDoc -> [TyVar] -> SDoc -> TcM () Source #
Check a list of binders to see if they make a valid telescope. The key property we're checking for is scoping. For example: > data SameKind :: k -> k -> * > data X a k (b :: k) (c :: SameKind a b) Kind inference says that a's kind should be k. But that's impossible, because k isn't in scope when a is bound. This check has to come before general validity checking, because once we kind-generalise, this sort of problem is harder to spot (as we'll generalise over the unbound k in a's type.) See also Note [Bad telescopes].
checkZonkValidTelescope :: SDoc -> [TyVar] -> SDoc -> TcM [TyVar] Source #
Like checkZonkValidTelescope, but returns the zonked tyvars
checkValidInferredKinds Source #
Arguments
| :: [TyVar] | vars to check (zonked) |
| -> TyVarSet | vars out of scope |
| -> SDoc | suffix to error message |
| -> TcM () |
After inferring kinds of type variables, check to make sure that the inferred kinds any of the type variables bound in a smaller scope. This is a skolem escape check. See also Note [Bad telescopes].