[GHC] #12466: Typechecker regression: Inaccessible code in a type expected by the context

[GHC]

#12466: Typechecker regression: Inaccessible code in a type expected by the context
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:  8.0.2
       Component:  Compiler (Type    |              Version:  8.1
  checker)                           |
      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 ekmett):

 So am I correct in guessing that this causes us to fail for the
 `Conjoined` class in `lens`?

 I've stripped it down removing the superclasses here:

 {{{#!hs
 class Conjoined p where
   conjoined :: ((p ~ (->)) => q (a -> b) r) -> q (p a b) r -> q (p a b) r
   conjoined _ r = r
 }}}

 (This is just a noisier version of `Foo`.)

 This is a rather big huge of the optimization story in `lens`, as we use
 it to avoid fiddling around with updating indices when the user isn't
 using them. This can make a 100x difference in performance for user code,
 so it isn't a trivial thing to throw away. If this suddenly isn't legal
 any more I'm really not sure what the heck we're going to do.

 That said, I don't see how that statement is illegal. `conjoined` takes
 two argument, one says _if_ you can tell me that p is (->) i'll give you a
 thing. The other is unconditionally usable.

 Once you learn p isn't `(->)` you simply can't use the first argument, as
 you could never satisfy its precondition. It isn't an error on the behalf
 of the signature of `conjoined`. It seems something is hinky in the way
 we're judging who has incurred an obligation here and when.

 We seem to be being far too eager to discharge an obligation we have no
 reason to even look at. Until something tries to use the first argument,
 why are we even doing anything with its constraints at all? The constraint
 being unsatisfiable in this limited situation is very much the point of
 the expression in the first place.

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