#14331: Overzealous free-floating kind check causes deriving clause to be rejected -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.2.1 checker) | Resolution: | Keywords: deriving Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Replying to [comment:6 goldfire]:
But I see `instance C (a :: k) D` as fully equivalent to `instance forall k (a :: k). C a D`. They just make different things explicit, but both declarations have the same static and dynamic semantics.
Yes, agreed.
And, I don't quite agree that clauses in a `deriving` are macro-like. They are types of kind `... -> Type -> Constraint`, where the `...` may be empty.
Surely you mean kind `k -> Constraint`? You certainly can't say `deriving Z`, where `class Z a b`, for instance. To elaborate what I mean by "macro" here: yes, the `C c1 ... cn` in `deriving (C c1 ... cn)` is a type, and one that is thrust into the typechecker at one point as a sanity-check to make sure you aren't writing utter garbage. But it's not like other types in that `C c1 ... cn` doesn't appear on its own in the emitted code—it only makes sense to talk about `C c1 ... cn` in the final program //after it has been combined// with its corresponding data type. Trying to stick `forall`s on just `C c1 ... cn` feels nonsensical, because the scoping needs to happen for the whole derived instance, not just `C c1 ... cn`, which happens to be one part of the recipe.
I believe that you are genuinely confused here. But I'm afraid I'm equally confused as to why you're confused.
The thing that I am confused on above all else is this business on skolems you mention in https://ghc.haskell.org/trac/ghc/ticket/14332#comment:9, and why the user-written kinds of a data type's type variables don't fall under the same scrutiny. I can't even begin to understand how this would work without an explanation of what is motivating this design choice. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14331#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler