| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Unison.KindInference
Description
Kind inference for Unison
Unison has Type, ->, and Ability kinds
An algorithm sketch: First break all decls into strongly connected
components in reverse topological order. Then, for each component,
generate kind constraints that arise from the constructors in the
decl to discover constraints on the decl vars. These constraints
are then given to a constraint solver that determines a unique kind
for each type variable. Unconstrained variables are defaulted to
kind Type (just like Haskell 98). This is done by inferDecls.
Afterwards, the SolveState holds the kinds of all decls and we
can check that type annotations in terms that may mention the
decls are well-kinded with kindCheckAnnotations.
Synopsis
- inferDecls :: forall v loc. (Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Map Reference (Decl v loc) -> Either (NonEmpty (KindError v loc)) (SolveState v loc)
- kindCheckAnnotations :: forall v loc. (Var v, Ord loc, Show loc, BuiltinAnnotation loc) => PrettyPrintEnv -> SolveState v loc -> Term v loc -> Either (NonEmpty (KindError v loc)) ()
- data KindError v loc
Documentation
inferDecls :: forall v loc. (Var v, BuiltinAnnotation loc, Ord loc, Show loc) => PrettyPrintEnv -> Map Reference (Decl v loc) -> Either (NonEmpty (KindError v loc)) (SolveState v loc) Source #
Infer the kinds of all decl vars
kindCheckAnnotations :: forall v loc. (Var v, Ord loc, Show loc, BuiltinAnnotation loc) => PrettyPrintEnv -> SolveState v loc -> Term v loc -> Either (NonEmpty (KindError v loc)) () Source #
Check that all annotations in a term are well-kinded