133 | | GADT constructors must only accept arguments of kind {{{*}}} (as per the restrictions on (->) described below), but may also collect constraints for the kind inference system. |

134 | | |

135 | | === Ambiguous cases === |

136 | | |

137 | | TODO: are there real ambiguous cases? _Assuming_ data types have their kind signatures inferred before functions are type checked and must be monomorphic in their kinds, I don't see how there could be unless a variable is totally unconstrained (i.e. not mentioned) |

138 | | |

139 | | {{{ |

140 | | foo :: forall a . Int |

141 | | }}} |

142 | | |

143 | | However this is accepted (6.8.3), although ghci drops the 'a'. Even if it was used in a scoped setting (TODO example of where that makes sense without a type class grounding it), the moment it is used it'll get a kind constraint. Do PolymorphicKinds break this assumption? |

| 133 | GADT constructors must only accept arguments of kind {{{*}}} (as per the restrictions on (->) described above), but may also collect constraints for the kind inference system. |

| 134 | |

| 135 | === Kind inference === |

| 136 | |

| 137 | Kind inference figures out the kind of each type variable. There are often ambiguous cases: |

| 138 | {{{ |

| 139 | data T a b = MkT (a b) |

| 140 | }}} |

| 141 | These are resolved by Haskell 98 with `(a :: *->*)` and `(b :: *)`. We propose no change. |

| 142 | But see kind polymorphism below. |