Documentation

The kind expected in a certain context.

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.

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

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

Like checkZonkValidTelescope, but returns the zonked tyvars

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