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

 I've clarified point 3, above.

 Replying to [comment:32 RyanGlScott]:
 >
 > 5. c. I'm not sure I understand this business about `kappa2` (or why
 you'd choose `kappa2 := Type`). Can you give an example of where this
 would arise?

 {{{#!hs
 class C a
 data D a = D deriving C
 }}}

 We see that `C :: forall k. k -> Constraint`. So we have `ki` = `forall k.
 k -> Constraint`. We then instantiate (note new step, above) to get `ki` =
 `kappa3 -> Constraint`, where `kappa3` is a fresh unification variable.
 Unifying with `kappa -> Constraint` simply sets `kappa := kappa3`. So,
 `ki2` is really just `kappa3`. This is the special case in (d).

 What's really going on here is that both the following are well-kinded:

 {{{#!hs
 instance C D
 instance C (D a)
 }}}

 We choose the second -- that's the `kappa2 := Type`. Alternatively, we
 could issue an error here; it's all a free design choice.

 >
 > 5. e. Some more validity checks that would need to be performed for data
 family instances are documented
 [http://git.haskell.org/ghc.git/blob/7ac22b73b38b60bc26ad2508f57732aa17532a80:/compiler/typecheck/TcDeriv.hs#l747
 here].

 I've updated my algorithm. Thanks.

 >
 > 5. h. I was hoping for a little more detail on this skolem business.

 A skolem is a type variable that is held distinct from any other type. For
 example:

 {{{#!hs
 nid :: a -> a
 nid True = False
 }}}

 This fails to type-check because, in the body of `nid`, `a` is a skolem.
 If it were a unification variable, we would just unify `a := Bool`. The
 "Practical Type Inference" paper has a good discussion of skolems.

 In a `deriving` clause, any variable quantified in the clause is
 considered to be a skolem. These skolems are basically unrelated, though,
 to the skolems mentioned in step (i). The skolems in step (i) would come
 from something like this:

 {{{#!hs
 class C (a :: Type)
 data D k (b :: k) = D deriving C
 }}}

 leads to

 {{{#!hs
 instance ... => C (D alpha beta)
 }}}

 where `alpha` and `beta` are unification variables. Because these
 variables are unconstrained, we wish to quantify over them, leading to the
 final instance declaration

 {{{#!hs
 instance forall a (b :: a). ... => C (D a b)
 }}}

 The `a` and `b` here are the fresh skolems of stem (i).

 Your example is

 {{{#!hs
 class C j (a :: j)
 data D = D deriving (forall k. C k)
 }}}

 Here, we learn that `ki2` (of step (c)) is the skolem `k`. (This is a
 skolem because user-written variables are skolems, like in the `nid`
 example.) That is not of the form `... -> Type`, nor is it a unification
 variable. (I just added the key qualifier "unification" to that step.) So
 we reject at this point.

 >
 >       Also, does the skolemicity only kick in if you write an explicit
 `forall`? Or would the `k` in `data D = D deriving (C k)` also get
 skolemized?

 The user-written variables in a `deriving` clause are skolems whether or
 not they are explicitly quantified.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14331#comment:33>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler