#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): Simon and I debated this all at some length this morning. We basically settled on agreeing to my paragraph at the end of comment:29. Spelling this out: 1. The variables introduces in the `data` declaration head scope over the `deriving` clause. (Throughout this comment, `newtype` is treated identically to `data`.) This is true even for GADT-syntax declarations where any variables in the head typically have no scope. 2. Any type variables mentioned in a `deriving` clause but not already in scope are brought into scope locally in that `deriving` clause. Independent comma-separated clauses are separate and quantify separately. 3. The user may write an explicit `forall` in a `deriving` clause scoped over only one clause. This is understood as a scoping construct, not quite as a full-blooded `forall`. 4. Process a `data` declaration on its own, without further regard to any `deriving` clauses. 5. For each `deriving` clause: a. Let the kind of the head of the clause (the part without the `forall`) be `ki` and the set of variables locally quantified be `bs`. Let the head of the clause be `drv`. b. Unify `ki` with `kappa -> Constraint`, getting a substitution for `kappa`; let the result of this substitution be `ki2`. (Issue an error if unification fails.) c. It is required that `ki2` have the form `... -> Type` or `kappa2` for some variable `kappa2`. If `ki2` is `kappa2`, then choose `kappa2 := Type`. Now, we have something of the form `... -> Type`. Let the number of arguments in the `...` be `n`. d. Let the set of variables mentioned in the `deriving` clause but not locally scoped (that is, they are also mentioned in the `data` declaration head) be `as`. e. It is an error if any variable in `as` is mentioned in any of the last `n` arguments in the `data` declaration head. f. Drop the last `n` arguments (whether visible or invisible) to the datatype. Call the result `ty`. g. Replace any type variables in `ty` but '''not''' mentioned in the `deriving` clause with fresh unification variables. h. Unify the kind of `ty` with `ki2`, issuing an error if unification fails. Zonk `ty`, replacing any unfilled unification variable with fresh skolems. Call the set of these skolems `sks`. i. Produce `instance forall {bs sks as}. ... => drv ty`, where the braces around the variables is meant to imply that order does not matter; GHC will do a topological sort to get these variables in the right order. j. Solve for the unknown context `...` and insert that into the declaration. k. Declare victory. I think that does it. Simon had wanted a much more declarative specification (and I agree), but I'm stuck on how to write one at the moment. Let's perhaps agree on this algorithmic specification and then see if there are ways to clean it up. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14331#comment:31 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler