[GHC] #12768: 8.0.2 derives invalid code when class method is constrained by itself

[GHC]

#12768: 8.0.2 derives invalid code when class method is constrained by itself
-------------------------------------+-------------------------------------
        Reporter:  jophish           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.0.2
       Component:  Compiler          |              Version:  8.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 There is a real difficulty here, if I'm not mistaken.  Consider
 {{{
 class C a where
   op :: D a => a -> a

 instance C [a] where
   op = opList

 opList :: D [a] => [a] -> [a]
 opList = ...
 }}}
 Now suppose we try GND:
 {{{
 newtype N a = MkN [a] deriving( C )
 }}}
 The GND is expecting to get an implementation of `op` for `N` from that
 for `opList`, something like
 {{{
 instance C [a] => C (N a) where
   op = opN

 opN :: D (N a) => N a -> N a
 opN = ...opList...   -- Uses coerce
 }}}
 But the call to `opList` in the definition of `opN` needs `(D [a])`
 whereas what we
 are given is `D (N a)`.  **And these are not inter-coercible**.  For
 example we
 might have manually written instances
 {{{
 instance D [a] where ...
 instance D (N a) where ...
 }}}
 and there is no relation between them.  So in this case, the code for
 `opN` is **not** representationally the same as the code for `opList`, so
 GND (which is all about representational equivalence) doesn't really
 apply.

 In the actual example, `D` is just `C` again, but I don't think we should
 treat it any differently.

 The actual error is generated by an attempt to coerce
 {{{
 coerce @(C m => m ()) @(C (N m) => N m ())
 }}}
 which rightly fails.

 So I think GND just doesn't work here.

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