[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 see what's Simon's getting at with his (2). Let me try to explain by way
 of a much simpler example.

 Suppose the user has written

 {{{#!hs
 f :: _ => a -> a
 f True = False
 f False = True
 }}}

 GHC rejects. But it doesn't have to do so: it could infer `_ := (a ~
 Bool)`, thus giving `f` the type `(a ~ Bool) => a -> a`, a perfectly fine
 type for that definition. Of course, GHC doesn't do this, because it leads
 to a bad user experience.

 It's similar with `deriving` inference: GHC is free to infer whatever
 constraints it wants for the instance. It ''could'' choose to infer a `k ~
 Type` constraint. Currently, it doesn't because that's too like the `a ~
 Bool` constraint above. So Simon is proposing to unrestrict GHC in this
 regard.

 Sadly, however, this doesn't actually work. Again, I'll use a simpler
 example to demonstrate:

 {{{#!hs
 g :: forall k (a :: k). k ~ Type => a -> a
 g x = x
 }}}

 GHC rejects this type signature, saying that `a` has kind `k`. This isn't
 a bug. It was decided en route to `TypeInType` that GHC wouldn't allow
 kind-level equality constraints to be used in the same type that they're
 brought into scope. (Essentially, we don't Pi-quantify constraints.) One
 reason for this is that `~` is lifted and can be forged. (There are some
 disorganized notes about all this
 [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unliftedequality
 here].)

 The `k ~ Type` constraint Simon proposes would suffer from the same non-
 feature. So, even if GHC did infer `k ~ Type`, we couldn't just stuff this
 constraint in the inferred theta and declare victory.

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

 I, too, am against Simon's (1). `stock` deriving is all ad-hoc. I'm not
 bothered by this particular piece of ad-hockery. It should be documented,
 of course, but I think it's OK. I don't think my algorithm should
 accommodate this, though, precisely because it is indeed ad-hoc.

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