#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