Opened 2 years ago

Closed 2 years ago

Last modified 15 months ago

#10132 closed bug (fixed)

Inconsistent kind polymorphism for top-level and associated type families

Reported by: simonpj Owned by:
Priority: normal Milestone: 8.0.1
Component: Compiler Version: 7.8.4
Keywords: Cc: diatchki, dimitris, goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by simonpj)

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

Change History (5)

comment:1 Changed 2 years ago by simonpj

Description: modified (diff)

comment:2 Changed 2 years ago by goldfire

I concur with everything above. Indeed, I believe the statement in bold has been the guiding principle all along, but perhaps not well articulated.

comment:3 Changed 2 years ago by Simon Peyton Jones <simonpj@…>

In b833bc2767d7a8c42093cf2994453f70df206c8d/ghc:

User manual section to document the principles of kind inference

This just documents the conclusions of Trac #10132

comment:4 Changed 2 years ago by simonpj

Resolution: fixed
Status: newclosed

comment:5 Changed 15 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.