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

 I think there is morally a difference between

 {{{#!hs
 class Foo a where
    foo :: (a ~ Int => a) -> a -> a
 }}}

 and your example which is more like

 {{{#!hs
 class Foo a where
    foo :: (a ~ Int) => a -> a -> a
 }}}

 in terms of if we should reject things once we know `a ~ Char`, and that
 hence `a ~ Int` can never happen.

 In the former you're given two arguments, one of which requires you to
 provide something impossible to use, and so simply cant be used, while in
 the latter you're required to implement a contradiction when you go to
 write `instance Foo Char`.

 Notice the polarity of the equality constraint. In the former it is in
 positive position. In the latter it is in negative position as usual.
 Finding a contradiction in negative position fits with Richard's intuition
 about if we should complain, but in positive position it simply means that
 argument is inaccessible, which is perfectly okay.

 Someone might pass it in in a more polymorphic setting where they don't
 know if the constraint could be satisfied or not, until the instance for
 Foo is selected, which is what is happening here.

 Today I usually hack around the latter by passing an explicit Dict for the
 constraint, so that I have the option to bring it into scope or not, and
 can carefully avoid GHC prematurely detonating upon discovering the
 contradiction

 {{{#!hs
 class Foo a where
    foo :: Dict (a ~ Int) -> a -> a -> a
 }}}

 but until now I haven't had to hack around it for the former -- and the
 explicit Dict-based solutions are much clunkier to both write, and for
 users to use in practice. (We used to use this approach to implement ex
 falso quodlibet in the `constraints` package, but now we just use `Any`
 directly as an uninhabitable initial `Constraint`.)

 > Currently

 {{{#!hs
 foo :: (Char ~ Int => Int) -> a -> a
 foo _ a2 = a2
 }}}

 > gives a similar message. Is that reasonable? The argument to foo can't
 be called.

 I'd personally think that that should be allowed, as silly as it looks in
 this very concrete case. `foo` itself doesn't care about the argument at
 all. The burden of complaining about the impossibility of what we can see
 locally would be `Int ~ Char` should fall on type checking the argument
 passed to `foo` at the call site, not to `foo`, and at that call site it
 may or may not be impossible as it may not know the `Int` part of the
 equation there.

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