| 24 | |

| 25 | This section deals with a proposal to collapse kinds and sorts into a single system |

| 26 | so as to allow Generalised Algebraic DataKinds (GADKs). The sort `BOX` should |

| 27 | become a kind, whose ''kind'' is again `BOX`. Kinds would no longer be classified by sorts; |

| 28 | they would be classified by kinds. |

| 29 | |

| 30 | (As an aside, sets containing themselves result in an inconsistent system; see, for instance, |

| 31 | [http://www.cs.nott.ac.uk/~txa/g53cfr/l20.agda this example]. This is not of practical |

| 32 | concern for Haskell.) |

| 33 | |

| 34 | Collapsing kinds and sorts would allow some form of indexing on kinds. Consider the |

| 35 | following two types, currently not promotable in FC-pro: |

| 36 | {{{ |

| 37 | data Proxy a = Proxy |

| 38 | |

| 39 | data Ind (n :: Nat) :: * where ... |

| 40 | }}} |

| 41 | In `Proxy`, `a` has kind `forall k. k`. This type is not promotable because |

| 42 | `a` does not have kind `*`. This is unfortunate, since a new feature (kind |

| 43 | polymorphism) is getting on the way of another new feature (promoting |

| 44 | datatypes). As for `Ind`, it takes an argument of kind (promoted) `Nat`, |

| 45 | which renders it non-promotable. Why is this? Well, promoted `Proxy` and `Ind` |

| 46 | would have sorts: |

| 47 | {{{ |

| 48 | Proxy :: forall s. s -> BOX |

| 49 | |

| 50 | Ind :: 'Nat -> BOX |

| 51 | }}} |

| 52 | But `s` is a sort variable, and `'Nat` is the sort arising from promoting |

| 53 | the kind `Nat` (which itself arose from promoting a datatype). FC-pro has |

| 54 | neither sort variables nor promoted sorts. However, if there are no sorts, and |

| 55 | `BOX` is the '''kind''' of all kinds, the "sorts" ("kinds", now) of promoted `Proxy` |

| 56 | and `Ind` become: |

| 57 | {{{ |

| 58 | Proxy :: forall k. k -> BOX |

| 59 | |

| 60 | Ind :: Nat -> BOX |

| 61 | }}} |

| 62 | Now instead of sort variables we have kind variables, and we do not need to promote |

| 63 | `Nat` again. |

| 64 | |

| 65 | Kind indexing alone should not require kind equality constraints; we always |

| 66 | require type/kind signatures for kind polymorphic stuff, so then |

| 67 | [http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/gadt-rigid-contexts.pdf wobbly types] |

| 68 | can be used to type check generalised algebraic kinds, avoiding the need for |

| 69 | coercions. While this would still require some implementation effort, it |

| 70 | should be "doable". |