TcValidity

Documentation

data Rank

Instances

Outputable Rank

Defined in TcValidity

Methods

ppr :: Rank -> SDoc

pprPrec :: Rational -> Rank -> SDoc

data UserTypeCtxt

Constructors

FunSigCtxt Name Bool

InfSigCtxt Name

ExprSigCtxt

KindSigCtxt

TypeAppCtxt

ConArgCtxt Name

TySynCtxt Name

PatSynCtxt Name

PatSigCtxt

RuleSigCtxt Name

ResSigCtxt

ForSigCtxt Name

DefaultDeclCtxt

InstDeclCtxt Bool

SpecInstCtxt

ThBrackCtxt

GenSigCtxt

GhciCtxt Bool

ClassSCCtxt Name

SigmaCtxt

DataTyCtxt Name

DerivClauseCtxt

TyVarBndrKindCtxt Name

DataKindCtxt Name

TySynKindCtxt Name

TyFamResKindCtxt Name

checkValidType :: UserTypeCtxt -> Type -> TcM ()

checkValidMonoType :: Type -> TcM ()

checkValidTheta :: UserTypeCtxt -> ThetaType -> TcM ()

checkValidInstance :: UserTypeCtxt -> LHsSigType GhcRn -> Type -> TcM ()

checkValidInstHead :: UserTypeCtxt -> Class -> [Type] -> TcM ()

validDerivPred :: TyVarSet -> PredType -> Bool

checkTySynRhs :: UserTypeCtxt -> TcType -> TcM ()

checkValidCoAxiom :: CoAxiom Branched -> TcM ()

checkValidCoAxBranch :: TyCon -> CoAxBranch -> TcM ()

checkValidTyFamEqn

Arguments

:: TyCon

of the type family

-> [Var]

Bound variables in the equation

-> [Type]

Type patterns

-> Type

Rhs

-> TcM ()

Do validity checks on a type family equation, including consistency with any enclosing class instance head, termination, and lack of polytypes.

checkConsistentFamInst

Arguments

:: AssocInstInfo

-> TyCon

Family tycon

-> CoAxBranch

-> TcM ()

badATErr :: Name -> Name -> SDoc

arityErr :: Outputable a => SDoc -> a -> Int -> Int -> SDoc

checkValidTelescope :: TyCon -> TcM ()

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 Note [Generalisation for type constructors] in TcTyClsDecls for data type declarations and Note [Keeping scoped variables in order: Explicit] in TcHsType for foralls

allDistinctTyVars :: TyVarSet -> [KindOrType] -> Bool