Inconsistent kind polymorphism for top-level and associated type families

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 (closed) again, in the new Typeable branch.)