ghc-8.6.4: 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 _

checkValidFamPats Source #

Arguments

:: Maybe ClsInstInfo 
-> TyCon 
-> [TyVar] 
-> [CoVar] 
-> [Type]

patterns the user wrote

-> [Type]

"extra" patterns from a data instance kind sig

-> SDoc

pretty-printed user-written instance head

-> TcM () 

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

-> SDoc

user-written LHS

-> 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 => SDoc -> a -> Int -> Int -> SDoc Source #

checkValidTelescope :: [TyConBinder] -> SDoc -> 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].