#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.Unl... 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