Copyright	(c) Edward Kmett 2011-2012
License	BSD3
Maintainer	Edward Kmett <ekmett@gmail.com>
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Ermine.Inference.Kind

Description

Synopsis

Documentation

inferKind :: MonadMeta s m => Type (MetaK s) (KindM s) -> m (KindM s) Source

Infer a kind for a given type.

inferAnnotKind :: MonadMeta s m => Annot (KindM s) -> m (KindM s) Source

checkKind :: MonadMeta s m => Type (MetaK s) (KindM s) -> KindM s -> m () Source

Check that the Kind of a given Type can unify with the specified kind.

checkDataTypeKinds :: [DataType () Text] -> M s [DataType Void Void] Source

Checks a list of data types for well-kindedness. The unit in the kind variables is interpreted as an unknown, which must be determined by the algorithm. The string variables may refer to other data types in the group. During the process, all unknowns will be solved or generalized, and all type variables will be replaced by the respective constructor with the appropriate schematic type. These are returned from the procedure.

TODO: Currently, the following example fails with a skolem escape:

  data Foo (a : k) = Foo (Bar a)
  data Bar a = Bar (Foo a)

This is because Foo and Bar must be checked as a group, k is skolemized for the checking of Foo, but its type leaks to Bar's unknown kind. Resolving this may be complicated, as it requires a similar explicit/implicit divide as checking lets, but partial annotations are possible. One solution may be to infer first and then check against annotations. Kind checking is Hindley-Milner, so this is viable.

checkDataTypeGroup :: [DataType () Text] -> M s [DataType Void Void] Source

checkDataTypeKind :: Map Text (DataType (MetaK s) a) -> DataType (MetaK s) Text -> M s ([MetaK s], Schema v) Source

Checks that the types in a data declaration have sensible kinds.

checkConstructorKind :: Constructor (MetaK s) (KindM s) -> M s () Source

Checks that the types in a data constructor have sensible kinds.