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

 Thanks Richard, this looks wonderful. I have some questions/comments about
 your algorithm:

 3. What happens if the user writes an explicit `forall` in a `deriving`
 clause but leaves out a variable, such as in `data Foo a = ... deriving
 (forall b. C b c)`?

    Also, in what sense is this not a "full-blooded `forall`"?

 5. c. I'm not sure I understand this business about `kappa2` (or why you'd
 choose `kappa2 := Type`). Can you give an example of where this would
 arise?

 5. e. Some more validity checks that would need to be performed for data
 family instances are documented
 [http://git.haskell.org/ghc.git/blob/7ac22b73b38b60bc26ad2508f57732aa17532a80:/compiler/typecheck/TcDeriv.hs#l747
 here].

 5. h. I was hoping for a little more detail on this skolem business. For
 instance, we'd want to reject `data D = D deriving (forall k. C k)` (where
 we have `class C k (a :: k)`) since the `k` is skolem, yes? (Disclaimer:
 due to my lack of experience with typechecker terminology, I'm guessing
 that "skolem" is a fancy way of saying "can't unify with other types".
 Please correct me if I'm off-track here.) Currently, this just says
 "replacing any unfilled unification variable with fresh skolems", which
 doesn't give me a sense of //where// the skolems are coming from.

       Also, does the skolemicity only kick in if you write an explicit
 `forall`? Or would the `k` in `data D = D deriving (C k)` also get
 skolemized?

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