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 kindk1 -> 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.)