[Haskell] Higher kind type inference paper

[John Meacham]

jhc does it via the simple unification type inference algorithm,
modified to push explicitly given kinds down into terms. so, pretty much
exactly the boxy type inference algorithm, where your kind inference
function looks somewhat like

> data Kind = 
>         Star 
>         | Fun Kind Kind 
>         | Hash
>         | UnboxedTuple  -- (#)
>         | KVar Constraints (IORef (Maybe Kind))

> data Constraints = 
>         AnyKind 
>         | SimpleKind  -- * or simplekind -> simplekind
>         | FunResult   -- ?  * # or (#)
>         | Argument    -- ?? * or #


> tiKind :: Term -> Kind -> Ki ()
> tiKind = ...


constraints are how the simple kind subtyping is done. like the rule for
application would be:

> tiKind (TArrow a b) Star = do
>         va <- newVar FunArg    -- ??
>         vr <- newVar FunResult -- ?
>         tiKind a va
>         tiKind b vr 

note that ?? and ? arn't real kinds, they are just constraints placed on
what valid kinds can be infered in a given spot. whenever a KVar is
filled in, it is first checked against the constraint, whenever two
KVars are unified, the glb of their constraints is used.

then once everything is done. I unify all free kind variables  with *.

The algorithm is heavily influenced by the 'boxy kind inference paper'
of SPJs. 

the code is in FrontEnd.Tc.Kind and FrontEnd.KindInfer, but it is pretty
hairy, due to it evolving incrementally from my previous algorithm which
envolved from the original hatchet code, which is derived from the THIH
paper.

        John


-- 
John Meacham - ⑆repetae.net⑆john⑈