Inconsistent kind polymorphism for top-level and associated type families
|Reported by:||simonpj||Owned by:|
|Keywords:||Cc:||diatchki, dimitris, goldfire|
|Type of failure:||None/Unknown||Test Case:|
|Related Tickets:||Differential Rev(s):|
Description (last modified by )
Consider this, with
class C a where data D1 a type F1 a data D2 a type F2 a
D2 to behave exactly the same; and similarly
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
F1we 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
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 -> k3if you go for maximal polymorphism. You can declare the polymorphism with kind signatures.
- Why does
*? 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
(I reverse-engineered all this when looking at #9999 again, in the new