Consider this, with `-XPolyKinds`: ``` class C a where data D1 a type F1 a data D2 a type F2 a ``` You'd expect `D1` and `D2` to behave exactly the same; and similarly `F1` and `F2`. But they don't: ``` D1 :: forall k (a:k). k -> * D2 :: * -> * F1 :: forall k (a:k). k -> * F2 :: * -> * ``` This seems odd. Indeed, when I stumbled across it I thought it was a plain bug. But I think there is some justification: - For associated types like `D1`, `F1` we make the class kind-polymorphic by default. And hence the associated types really have to be also. - Should classes be by-default kind-polymorphic? Well, data types are, so probably classes should be too. The types of the methods of the class, or the constructors of the data type, usually give plenty of clues. - For top-level types like `D2`, `F2`, it seems perhaps overkill to make them kind polymorphic by default. The difference is that they have no right hand side to get clues from, so they'll always have kind `k1 -> k2 -> k3` if you go for maximal polymorphism. You can declare the polymorphism with kind signatures. - Why does `F1` return `*`? It could as well be kind-polymorphic in its result. Again I think this is because there cannot be any clue as to its result kind so we default to `*`. Maybe this is all a good choice. The principle seems to be: **if the declaration has a "right hand side", infer kinds from that; if not, default to `*`**. But even if that is the right principle, we should articulate it explicitly, in the user manual and a `Note` somewhere. (I reverse-engineered all this when looking at #9999 again, in the new `Typeable` branch.)