Language.PureScript.TypeChecker.Kinds

This module implements the kind checker

Documentation

kindOf :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> m (SourceType, SourceType)

Infer the kind of a single type

kindOfWithUnknowns :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> m (([(Unknown, SourceType)], SourceType), SourceType)

kindOfWithScopedVars :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> m (([(Text, SourceType)], SourceType), SourceType)

Infer the kind of a single type, returning the kinds of any scoped type variables

kindOfData :: forall m. (MonadError MultipleErrors m, MonadState CheckState m) => ModuleName -> DataDeclarationArgs -> m DataDeclarationResult

kindOfTypeSynonym :: forall m. (MonadError MultipleErrors m, MonadState CheckState m) => ModuleName -> TypeDeclarationArgs -> m TypeDeclarationResult

kindOfClass :: forall m. (MonadError MultipleErrors m, MonadState CheckState m) => ModuleName -> ClassDeclarationArgs -> m ClassDeclarationResult

kindsOfAll :: forall m. (MonadError MultipleErrors m, MonadState CheckState m) => ModuleName -> [TypeDeclarationArgs] -> [DataDeclarationArgs] -> [ClassDeclarationArgs] -> m ([TypeDeclarationResult], [DataDeclarationResult], [ClassDeclarationResult])

unifyKinds :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> SourceType -> m ()

unifyKinds' :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> SourceType -> m ()

Does not attach positions to the error node, instead relies on the | local position context. This is useful when invoking kind unification | outside of kind checker internals.

subsumesKind :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> SourceType -> m ()

instantiateKind :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => (SourceType, SourceType) -> SourceType -> m SourceType

checkKind :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> SourceType -> m SourceType

inferKind :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> m (SourceType, SourceType)

elaborateKind :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> m SourceType

checkConstraint :: forall m. (MonadError MultipleErrors m, MonadState CheckState m) => SourceConstraint -> m SourceConstraint

checkInstanceDeclaration :: forall m. (MonadError MultipleErrors m, MonadState CheckState m) => ModuleName -> InstanceDeclarationArgs -> m InstanceDeclarationResult

checkKindDeclaration :: forall m. (MonadSupply m, MonadError MultipleErrors m, MonadState CheckState m) => ModuleName -> SourceType -> m SourceType

checkTypeKind :: (MonadError MultipleErrors m, MonadState CheckState m, HasCallStack) => SourceType -> SourceType -> m ()

Check the kind of a type, failing if it is not of kind *.

unknownsWithKinds :: forall m. (MonadState CheckState m, MonadError MultipleErrors m, HasCallStack) => [Unknown] -> m [(Unknown, SourceType)]

freshKind :: MonadState CheckState m => SourceSpan -> m SourceType

freshKindWithKind :: MonadState CheckState m => SourceSpan -> SourceType -> m SourceType