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⑈