Kind inference for datatypes

This technical supplement to Kind Inference for Datatypes serves to expand upon the text in the main paper. It contains detailed typing rules, proofs, and connections to the Glasgow Haskell Compiler (GHC). Sections in this document are meant to connect to sections in the main paper. There are many hyperlinks throughout, especially those highlighting the connections to GHC; you may wish to read on a computer instead of on paper.

This section accompanies Section 8 of the main paper, including discussion about more related language extensions. These extensions affect kind inference, but not in a fundamental way.

Besides specified type variables for which users can optionally provide type arguments, Haskell also incorporates visible dependent quantification (VDQ) 1 , e.g., type T :: ∀(k :: ⋆) → k → ⋆, with which users are forced to provide type arguments to T . That is, one would use T with, e.g., T ⋆ Int and T (⋆ → ⋆) Maybe, never just T Int. Visible dependent quantification is Haskell's equivalent to routine dependent quantification in dependently typed languages.

To support VDQ, rule dt-tt needs to be extended, as VDQ brings variables into scope for later reference. For example, given type T :: ∀(k :: ⋆) → k → ⋆ data T k a = MkT We should get a context k :: ⋆, a :: k when checking MkT .

VDQ opens an interesting design choice: should unannotated type variables be able to introduce VDQ? For example, in the definition of P below, we use f and a as the arguments to T . To make it type-check, we need to infer P :: ∀(f :: ⋆) → f → ⋆.