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

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

 To my knowledge, there's no formalism that states what the static
 semantics of `deriving` clauses are, so saying what should or shouldn't be
 allowed leaves a lot up to personal interpretation. But I can at least
 give my interpretation: whenever something of the form:

 {{{#!hs
 data D d1 ... dn = ... deriving (C c1 ... cm)
 }}}

 is encountered, then an instance of the form:

 {{{#!hs
 instance ... => C c1 ... cm (D d1 ... dn)
 }}}

 is emitted. To put it less formally, one takes the derived type and plops
 the datatype to the right of it, forming the instance.

 Having established this, let me turn the tables on you and ask: what do
 //you// think should happen if something of this form is encountered?

 {{{#!hs
 data D d1 ... dn = ... deriving (forall <...>. C c1 ... cm)
 }}}

 I for one can't come up with a consistent semantics for this. Do you emit
 this?

 {{{#!hs
 instance ... => (forall <...>. C c1 ... cm) (D d1 ... dn)
 }}}

 Clearly not, since instances have to be headed by an actual type class
 constructor. So do you attempt to beta-reduce the `forall`'d type? What
 happens if there is more than one `forall`'d type variable?

 In my view, trying to make sense of this is opening up a giant can of
 worms. I'm open to being proved wrong though—is there an interpretation of
 this which makes sense, and has a consistent semantics?

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