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

 Alright, that sounds reasonable enough.

 After thinking about this some more, though, I realized that there's
 another incongruity with your proposal and how `TcDeriv` currently
 operates. In particular, there can be //more// unification after part (i)
 if you are deriving `Functor`, `Foldable`, or `Traversable`. Here is an
 example of such a situation (taken from Trac #10561):

 {{{#!hs
 newtype Compose (f :: k2 -> Type) (g :: k1 -> k2) (x :: k1) =
     Compose (f (g a))
   deriving stock Functor
 }}}

 In part (i), we would unify `Type -> Type` (the kind of the argument to
 `Functor`) with `k1 -> Type` (the kind of `Compose f g`, giving us:

 {{{#!hs
 instance forall {k2 (f :: k2 -> Type) (g :: Type -> k2)}.
          (Functor f, Functor g) => Functor (Compose f g)
 }}}

 But note that this won't kind-check yet, since the kinds of `f` and `g`
 are still too general. This is where
 [http://git.haskell.org/ghc.git/blob/e375bd350bc9e719b757f4dc8c907c330b26ef6e:/compiler/typecheck/TcDerivInfer.hs#l179
 this code] in `TcDerivInfer` kicks in: it takes every type on the RHS of
 the datatype that accepts one argument (in the example above, that would
 be `f` and `g`), unifies their kinds with `Type -> Type`, and applies the
 resulting substitution to the type variables. In the example above, this
 substitution would be `[k2 |-> Type]`, so applying that would yield the
 instance:

 {{{#!hs
 instance forall {(f :: Type -> Type) (g :: Type -> Type)}.
          (Functor f, Functor g) => Functor (Compose f g)
 }}}

 And now it kind-checks, so we can feed the instance context into the
 simplifier (part (k)).

 My question is: where does this extra unification for deriving `Functor`,
 `Foldable`, or `Traversable` fall into your algorithm? In part (j) you
 write `instance forall {bs sks as}. ... => drv ty`, which seems to suggest
 that the type variables shouldn't be unified any more after that step, but
 that's not true in this particular example.

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