3 | | This page summarises several alternative designs, which are debated on #9200. (See also #9201.) |
4 | | |
5 | | == Baseline strategy (BASELINE) == |
6 | | |
7 | | This plan, originally due to Mark Jones, is the strategy that GHC 7.8 follows for ordinary, recursive term-level functions, and for recursive data types. I'll describe it for data types, with this example: |
| 3 | This page summarises several alternative designs for doing kind inference for |
| 4 | types and classes, under `-XPolyKinds`. See the extensive discussion on #9200. (See also #9201.) |
| 5 | |
| 6 | == Current strategy (GHC 7.8) == |
| 7 | |
| 8 | Running example: |
| 9 | {{{ |
| 10 | data T a f = T1 Int (T a f) | T2 (f a) |
| 11 | |
| 12 | data S a f = S1 (S Maybe (S Int)) |
| 13 | }}} |
| 14 | |
| 15 | Here is GHC 7.8's strategy: |
| 16 | |
| 17 | 1. Sort data/type/class declarations into strongly connected components. In our example, there are two recursive SCCs, one for `T` and one for `S`. |
| 18 | |
| 19 | 2. Then, for each SCC in turn: |
| 20 | |
| 21 | * Bind the type constructor to a fresh meta-kind variable: |
| 22 | {{{ |
| 23 | T :: kappa0 |
| 24 | }}} |
| 25 | * Kind-check all the declarations of the SCC in this environment. This will generate some unifications, so in the end we get |
| 26 | {{{ |
| 27 | kappa0 ~ kappa1 -> (kappa1 -> *) -> * |
| 28 | }}} |
| 29 | * Generalise. So we get |
| 30 | {{{ |
| 31 | T :: forall k. k -> (k -> *) -> * |
| 32 | }}} |
| 33 | Following the same three steps for `S` fails, because we need polymorphic recursion. Srarting with `S :: kappa0`, we get |
| 34 | {{{ |
| 35 | kappa0 ~ kappa1 -> kappa2 -> * -- S has two arguments |
| 36 | kappa1 ~ *->* -- From (S Maybe) |
| 37 | kappa1 ~ * -- From (S Int) |
| 38 | ...and some more... |
| 39 | }}} |
| 40 | So in GHC 7.8 you can supply a "complete user kind signature" (CUSK) for `S`, thus: |
| 41 | {{{ |
| 42 | data S (a :: k) (f :: k -> *) where |
| 43 | S1 :: S Maybe (S Int) -> S a f |
| 44 | }}} |
| 45 | The real step 2 works thus: |
| 46 | * Bind the each non-CUSK type constructor to a fresh meta-kind variable, and each CUSK type constructor to its polymorphic kind. |
| 47 | {{{ |
| 48 | S :: forall k. k -> (k->*) -> * |
| 49 | }}} |
| 50 | * Kind-check all the declarations of the SCC in this environment. With this new kind for `S`, kind checking succeeds. |
| 51 | |
| 52 | * Generalise any non-CUSK type constructors. |
| 53 | |
| 54 | == Proposed new strategy == |
| 55 | |
| 56 | The main proposed change is to the definition of a "complete user kind signature" (CUSK). The current story is in [http://www.haskell.org/ghc/docs/latest/html/users_guide/kind-polymorphism.html#complete-kind-signatures Section 7.8.3 of the user manual]. Alas, it does not allow CUSKs for class declarations. |
| 57 | The new proposal is this: |
| 58 | * A class or datatype is said to have a CUSK if and only if all of its type variables are annotated. |
| 59 | This is somewhat simpler, it covers classes. See comment:19:ticket:9200 for more exposition. |
| 60 | This change alone is enough to satisfy #9200. |
| 61 | |
| 62 | '''Simon''' What about type synonym declarations. Don't we need a kind signature on the RHS? |
| 63 | |
| 64 | == A possible variation == |
| 65 | |
| 66 | This algorithm is not quite as expressive as it could be. Consider |
13 | | 1. Identify which type constructors have Complete User Type Signatures (CUSK). In this example, `TT` does. Extend the environment with these, fixed, kinds: |
| 72 | Here `TT` has a CUSK, but `SS` does not. Hence in step 1 we'd bind `SS :: kappa0`. But in the RHS of `TT` we use `SS` at two different kinds, so infernece will fail. We could solve this by giving a CUSK to `SS` as well. |
| 73 | |
| 74 | However, we can ''also'' solve it using a plan due to Mark Jones, and one that GHC 7.8 already follows for ordinary, recursive term-level functions. As usual, divide the declarations into SCCs, and then for each SCC do the following: |
| 75 | |
| 76 | * Identify which type constructors have Complete User Type Signatures (CUSK). In this example, `TT` does. Extend the environment with these, fixed, kinds: |
37 | | Note that for a ''non-recursive'' type or class declaration, (BASELINE) always works fine. |
38 | | |
39 | | === Refine the definition of CUSK (BASELINE/NEWCUSK) === |
40 | | |
41 | | GHC's current definition of a complete user-supplied kind signature is [http://www.haskell.org/ghc/docs/latest/html/users_guide/kind-polymorphism.html#complete-kind-signatures here in the user manual]. A big disadvantage is that classes can't have a CUSK under that definition. |
42 | | |
43 | | A somewhat simpler, but more permissive definition, and one that covers classes, is this: |
44 | | * A class or datatype is said to have a CUSK if and only if all of its type variables are annotated. |
45 | | |
46 | | See comment:19:ticket:9200 for more exposition. |
47 | | |
48 | | === Typing rule for (BASELINE/NEWCUSK) === |
49 | | |
| 100 | This strategy is more complicated than the initial proposal, but allows fewer annotations. It's not clear whether it is wroth the bother. |
| 101 | |
| 102 | === Typing rule for the new proposal === |
| 103 | |
| 104 | An algorithm is all very well, but what about the typing judgements? |