ghc-8.2.2: The GHC API

TcValidity

Synopsis

# Documentation

data Rank #

data ContextKind #

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) #

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.

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 #

checkValidTelescope :: SDoc -> [TyVar] -> SDoc -> 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 also Note [Bad telescopes].

checkZonkValidTelescope :: SDoc -> [TyVar] -> SDoc -> TcM [TyVar] #

Like checkZonkValidTelescope, but returns the zonked tyvars

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