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

 >  So, while Simon's (2) is nice in theory, it wouldn't work until we have
 more dependent types.

 Yes it will -- I just explained it badly.

 In `TcDerivInfer.inferConstaints` we figure out the context of the derived
 instance decl.  To do so we call `TcDerivInfer.simplifyDeriv`, which in
 turn
 calls `TcSimplify.solveWantedsAndDrop`.  It's the latter that will come up
 with that `k~Type` constraint.

 Now if that `k` is a unification variable, `solveWantedsAndDrop` will go
 right ahead and unify it.  Which, you are saying, is precisely what we
 want.  But, unlike the current ad-hoc setup, that will happen though
 constraint solving in general, rather than through a magical
 `Functor`-specific
 wim-wam.

 So, I say, make those unifiable k's into real unification variables, and
 let the constraint solver do its thing.  Then, when the dust settles,
 gather up all the free variables and quantify over them, much as we do
 in any other inferred type.   This does mean we can't fix on the
 quantified
 variables until after `inferConstraints`.  But it's simple and systematic.

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