[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 goldfire):

 I'm afraid I mostly disagree with comment:28.

 Your first example is

 {{{#!hs
 -- C :: Type -> Type -> Constraint
 data D k (a :: k) = ... deriving (forall x. C x)
 }}}

 I think we get an instance

 {{{#!hs
 instance forall x k (a :: k). (...) => C x (D k a)
 }}}

 No instantiation is needed to get `D k a` to have kind `Type`. But I'm not
 terribly bothered here -- I don't think the general argument is wrong,
 just the example.

 In the next example (with `C2`), I'm not sure the kind of `C2`. Perhaps
 it's `forall k -> k -> Type -> Constraint`? But even so, we can get

 {{{#!hs
 instance ... => C2 k a (D k a)
 }}}

 without getting hurt.

 Regardless, I don't see how this argument refutes comment:27. The example
 I was considering was

 {{{#!hs
 class C a b
 data D a = D deriving (C (a :: k))
 }}}

 where the `k` in the `deriving` clause is ''not'' mentioned in the data
 declaration. Thus the concerns in comment:28 don't apply. The `a` ''is''
 mentioned, but it needs no unification.

 I do agree that this is hard to nail down. It seems, though, that one way
 forward is to say that any variables explicitly mentioned in the
 `deriving` clause are ''not'' free for unification. Other variables in the
 data decl but ''not'' in the deriving clause can be unified. This is a
 little strange perhaps, but not hard to articulate or understand. I do
 think it's worth asking if anyone ever really needs variables shared
 between the data decl and the `deriving` (Simon's last point in
 comment:28).

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#comment:29>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler