#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): It will lead to an accepting definition, yes, but I don't think it's the definition you'd want (or at least, it seems to differ from the proposal I put forth in comment:14). If I understand your argument correctly, you want all type variables in a `deriving` clause's type to be scoped differently from the data type, and expect unification to save you in the end? That is, this: {{{#!hs data D a = D deriving (C (a :: k)) }}} Would be treated like this? {{{#!hs data D {k1} (a1 :: k1) = D deriving (forall {j} k (a :: k). C @k @j a) }}} If so, we have a problem—the //only// kinds we'd unify are the `j` in `C a :: j -> Constraint` and `Type` (the kind of `D a`), so the instance we'd get in the end is: {{{#!hs instance forall {k1} k {a1 :: k1} (a :: k). C @k @Type a (D @k1 a1) where ... }}} Which is not what I'd expect, since `a` and `a1` are distinct. The only way to ensure that they're the same is to interpret the scope like this: {{{#!hs data D {k} (a :: k) = D deriving (forall {j}. C @k @j a) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14331#comment:19 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler