Draft: Kinded Structures

Motivation

Many type systems are equipped with kinding systems. Mostly notably (and relevant to OCaml) are the various kinding systems associated with rows. This MR aims to implement a generic kinding framework in Inferno.

This MR is used as the basis of my implementation of polymorphic variants which I will soon push and begin upstreaming.

Description

The changes in this MR introduce a notion of a 'kinded structure':

• an abstract type kind;
• a kind_of function for structures that implements the kinding system on structures:

type kind

exception IllKinded
val kind_of : ('a -> kind) -> 'a structure -> kind

Kinds are equipped with a partial order k1 <= k2 defined using subkind : kind -> kind -> bool.

The MR also refactors structural conjunction to be parameterised over a generic 'first-order unification problem' U:

 U ::= t = t | exists 'a :: k. U | U && U

This is expressed as:

• kind_of for checking kinds during conjunction
• var to introduce existentially bound variables in the unification problem
• free to wrap structures into terms
• equate to emit equality constraints between terms

The Option structure is refactored into FirstOrder structure where variables now contain kinds represented as Var k instead of None. The conjunction of first-order variables relies on a partial least upper bound operator between kinds (kind_lub).