ghc-8.2.1: The GHC API

Safe HaskellNone
LanguageHaskell2010

TcValidity

Synopsis

Documentation

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 TYPE _

type ClsInstInfo = (Class, [TyVar], VarEnv Type) Source #

Extra information about the parent instance declaration, needed when type-checking associated types. The Class is the enclosing class, the [TyVar] are the type variable of the instance decl, and and the VarEnv Type maps class variables to their instance types.

checkValidTyFamEqn Source #

Arguments

:: Maybe ClsInstInfo 
-> 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.

arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc Source #

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].