Re: [GHC] #14331: Overzealous free-floating kind check causes deriving clause to be rejected

13 Oct 2017

      #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 think you don't understand correctly. (Perhaps because I've communicated
 poorly.)

 The user writes

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

 There is implicit lexical quantification in the `deriving` clause.
 ("Lexical" because it's all just based on reading the code -- no type-
 checking yet!) So, these declarations are understood to mean

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

 We don't have to write `forall` for the class or data declarations,
 because the type variables there are understood to mean quantification.
 Note that I'm ''not'' quantifying over `c` in the `deriving` clause,
 because it's already in scope.

 The initial declarations are processed without regard to the `deriving`
 clause, producing

 {{{#!hs
 class C {k1} {k2} (a :: k1) (b :: k2)
 data D {k3} (c :: k3) = D
 }}}

 Now, we type-check

 {{{#!hs
 instance forall {c k}. C (c :: k) (D c)
 }}}

 where the `C (c :: k)` is taken from the `deriving` clause, and the
 quantified variables are not yet ordered. After type-checking, we get

 {{{#!hs
 instance forall (k :: Type) (c :: k). C {k} {Type} c (D {k} c)
 }}}

 as desired.

 Note that the use of `c` in the `deriving` clause did not lead to
 unification. Instead, the fact that we know more about its kind does.

 However, in writing this up, I discovered a new problem. When I write

 {{{#!hs
 class C2 a
 data D b = D deriving C2
 }}}

 do I mean

 {{{#!hs
 instance C2 {k -> Type} D
 }}}

 or

 {{{#!hs
 instance C2 {Type} (D b)
 }}}

 ? Both are well-kinded and sensible. Right now, we always choose the
 latter, but I'm not sure why.

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