#10132: Inconsistent kind polymorphism for top-level and associated type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Description changed by simonpj: Old description:

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

New description: 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.) -- -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10132#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#10132: Inconsistent kind polymorphism for top-level and associated type families -------------------------------------+------------------------------------- Reporter: simonpj | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.4 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Type of failure: None/Unknown | Unknown/Multiple Blocked By: | Test Case: Related Tickets: | Blocking: | Differential Revisions: -------------------------------------+------------------------------------- Comment (by Simon Peyton Jones ): In [changeset:"b833bc2767d7a8c42093cf2994453f70df206c8d/ghc"]: {{{ #!CommitTicketReference repository="ghc" revision="b833bc2767d7a8c42093cf2994453f70df206c8d" User manual section to document the principles of kind inference This just documents the conclusions of Trac #10132 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/10132#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler