Re: [GHC] #14332: Deriving clauses can have forall types

9 Oct 2017

      #14332: Deriving clauses can have forall types
-------------------------------------+-------------------------------------
        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 accepts       |  Unknown/Multiple
  invalid program                    |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 I'm well aware of the fact that `deriv_clause_tys` uses `LHsSigType`. That
 is indeed there for a good reason—`deriving` clauses need to support
 implicit quantification. But just because `LHsSigType` supports explicit
 quantification via `forall`s doesn't mean it's a good idea to actually
 allow them in `deriving` clauses. After all, the fact that we use
 `LHsSigType` in class instances means that it's possible to write
 instances with nested `forall`s, like this:

 {{{#!hs
 instance forall a. forall b. (Show a, Show b) => Show (Either a b)
 }}}

 But despite this, GHC will reject this will `Malformed instance: forall a.
 forall b. Show (Either a b)`. Similarly, we should think carefully about
 whether `deriving (forall <<>>. C c1 ... cn)` well formed or not.

 I thought about this some more last night, and another reason why
 `deriving (forall <<>>. C c1 ... cn)` bothers me is because unlike the
 `forall` in a class instance, this proposed `forall` in a `deriving`
 clause doesn't scope over a "real" type in some ways. That is to say, the
 `C c1 ... cn` in `deriving C c1 ... cn` isn't so much of a type as a "type
 former". There is a rather involved process in taking `C c1 ... cn`,
 applying it to the datatype (possibly after eta reducing some of its type
 variables), and unifying their kinds. In fact, after this kind
 unification, it's possible that some of these type variables will vanish
 completely! Take this example, for instance:

 {{{#!hs
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE TypeInType #-}
 {-# OPTIONS_GHC -ddump-deriv #-}

 class C k (a :: k)

 data D = D deriving (C k)
 }}}

 Here, the actual instance that gets emitted (as shown by `-ddump-deriv`)
 is:

 {{{
 GHCi, version 8.2.1: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/ryanglscott/.ghci
 [1 of 1] Compiling Main             ( Bug.hs, interpreted )

 ==================== Derived instances ====================
 Derived class instances:
   instance Main.C * Main.D where
 }}}

 Notice how the `k` has become `*` due to kind unification! But according
 to this proposal, you could have alternatively written this as:

 {{{#!hs
 data D = D deriving (forall k. C k)
 }}}

 And according to the specification given in comment:3, this should emit an
 instance of the form `forall k. ... => C k D`. But that's clearly not true
 when you inspect `-ddump-deriv`! So this `forall` here is an utter lie.

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