Swarm.Language.Kindcheck

Kind checking for the Swarm language.

Documentation

data KindError

Kind checking errors that can occur.

Constructors

ArityMismatch TyCon Int [Type]

A type constructor expects n arguments, but was given these arguments instead.

UndefinedTyCon TyCon Type

An undefined type constructor was encountered in the given type.

TrivialRecTy Var Type

A trivial recursive type (one that does not use its bound variable) was encountered.

VacuousRecTy Var Type

A vacuous recursive type (one that expands immediately to itself) was encountered.

Instances

Show KindError

Defined in Swarm.Language.Kindcheck

Methods

showsPrec :: Int -> KindError -> ShowS

show :: KindError -> String

showList :: [KindError] -> ShowS

Eq KindError

Defined in Swarm.Language.Kindcheck

Methods

(==) :: KindError -> KindError -> Bool

(/=) :: KindError -> KindError -> Bool

PrettyPrec KindError

Defined in Swarm.Language.Pretty

Methods

prettyPrec :: Int -> KindError -> Doc ann

checkPolytypeKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Polytype -> m TydefInfo

Check that a polytype is well-kinded.

checkKind :: (Has (Reader TDCtx) sig m, Has (Throw KindError) sig m) => Type -> m ()

Check that a type is well-kinded. For now, we don't allow higher-kinded types, *i.e.* all kinds will be of the form Type -> Type -> ... -> Type which can be represented by a number (the arity); every type constructor must also be fully applied. So, we only have to check that each type constructor is applied to the correct number of type arguments. In the future, we might very well want to generalize to arbitrary higher kinds (e.g. (Type -> Type) -> Type etc.) which would require generalizing this checking code a bit.

Here we also check that any recursive types are non-vacuous, i.e. not of the form rec t. t, and non-trivial, i.e. the variable bound by the rec actually occurs somewhere in the body.