[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):

 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