Implement proper row kinds

[dhil]

For row variables we have kind Row. A row variable ranges over a cofinite set, however, we do not keep track of its finite complement, which means when a row variable appears as an argument in a type application, we miss out on valuable information about the variable.

[jamescheney]

I don't see any particular obstacle to implementing this as described above / in ATTAPL, perhaps by defining a "restriction" on row kinds. However, we are fairly seriously considering extending the typechecker to allow some other forms of constraints, which would allow handling (or generalizing) various forms of "restrictions" that are currently present in the kind system: base types, monomorphic types, possibly linearity following Garrett's ICFP 16 paper.

I'm therefore wondering whether "proper row kinds" (annotated with a list of fields that must not be defined in the row) also amount to a form of constraint, a.k.a. the "lacks" constraint found in Gaster and Jones style rows. Thus instead of saying forall r::Row{L}. t we would say something like forall r::Row. (r lacks l1,...,r lacks ln) => t where L = {l1,...,ln}.

This is not a suggestion to delay dealing with this issue until we add constraints to Links type inference, just a remark that once we do, the Row{L} kinds might be refactored into plain row kinds plus constraints - perhaps via desugaring after source typechecking or IR translation while keeping the kinds+restrictions in the source language. (On the other hand, I now wonder whether there is some reason why they used Row{L} kinds for this rather than constraints in the HM(X) chapter. So maybe we should work out whether that makes sense on paper first.)