#14331: Overzealous free-floating kind check causes deriving clause to be rejected -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: merge Priority: normal | Milestone: 8.2.2 Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | deriving/should_compile/T14331 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj):
the logic in comment:26 also means that `data Proxy a = P deriving Functor` should fail
Not at all! After elaborating the data type decl we have {{{ data P {k} (a::k) = P deriving( Functor ) }}} Now we create an instance declaration in which we are free to instantiate `k` (and indeed `a`) as much as we plase: {{{ instance Functor (P (*->*)) where ... }}} The quantified variables of the data type decl can freely be instantiated in the (derived) instance. We want the most general such instantiation so that the derived instance is applicable as much as poss; hence unification. I have belatedly realised that the real stumbling block here is when the same variable appears ''both'' in the data type decl ''and'' in the `deriving` clause. For example here {{{ -- C :: * -> * -> Constraint data D k (a::k) = ... deriving( forall x. C x ) }}} is fine: we get an instance looking like {{{ instance forall x (b::*). (...) => C x (D * b) where ... }}} The `x` from the `deriving` is universally quantified in the instance; the `k` and `a` are instantiated to `*` and `b` respectively; then we quantify over `b`. But the nasty case is this: {{{ data D k (a::k) = ... deriving( C2 k a ) }}} The `k` and `a` belong both to the data decl (hence it's in the "freely instantiate" camp) but also belong somehow in the instance. Can I freely instantiate the `k` in the instance? And the `k`? It'd be very odd if I got an instance like {{{ instance ... => C2 * a (D * a) where ... }}} because the `deriving` part explicitly said `k` not `*`. This seems very hard to specify. It's much easier to think of the data type decl and the instance entirely separately. Do we need the same variable to appear in both places? That is, what if we said that the type variables from the data type don't scope over the 'deriving' clause? Then {{{ data D k (a::k) = ... deriving( C2 k a ) }}} would mean {{{ data D k (a::k) = ... deriving( forall kk aa. C2 kk aa ) }}} where I've alpha-renamed to make it clear. What would go wrong if we did that? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14331#comment:28 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler