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

3 Nov 2016

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

 Well I guess that

 * if we are doing GND for `(C (N a))`, where `N` is a newtype
 * then `(C a)` is representationally equal to `(C (N a))`

 and that's just what we need here.  But I don't see an easy way to
 incorporate that knowledge in the solver.

 And this is very much a weird case: the `(C m)` constraint is entirely
 redundant.

 I worked out how GHC 8.0 is working.  We generate this:
 {{{
 instance C m => C (N m) where
   foo = coerce (foo :: m ()) :: N (m ())
 }}}
 From this instance decl we generate
 {{{
 dfCN :: C m => C (N m)
 dfCN d = MkC ($cfooN d)

 $cfooN :: C m => C (N m) => N m ()
 $cfooN d _ = foo d d |> (a coercion)
 }}}
 Notice that in `$cfooN` we don't need the second dictionary argument
 (corresponding to the `C m` constrain in `foo`'s signature in the class
 decl).  It just so happens that the instance context can satisfy it.

 But exploiting this fluke involves instantiating the call to `foo`, which
 is what I am now not doing.

 In comment:4, the fluke would require that from `C a` (the context of the
 instance decl) we could prove `D a` (the requirement of the call in the
 method body), again ignoring the supplied `(D (N a))`.

 I think the 8.0 behaviour is actually INCORRECT (it misbehaves in examples
 like comment:4), so I think we should indeed adopt the change for the 8.0
 branch.

 Do we have any actual user complaints?

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