[GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

[GHC]

#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