[GHC] #13446: Deferred type error sneaks in with -fno-defer-type-errors enabled

[GHC]

#13446: Deferred type error sneaks in with -fno-defer-type-errors enabled
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.2
  checker)                           |
      Resolution:                    |             Keywords:
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):

 Total shot in the dark: perhaps the reason that this is typechecking is
 that, post-03541cbae50f0d1cdf99120ab88698f29a278159, GHC treats all cases
 with insoluble given constraints as inaccessible. In the case of `lifting
 = Sub 'a'`, you have the given constraint `Coercible a (J (JTy a))`, and
 since GHC can't reduce the type family `JTy a` any, it deems `Coercible a
 (J (JTy a))` insoluble, causing it to typecheck.

 However, if you actually use `lifting` and instantiate the type variable
 `a` with `JObject`, then `JTy JObject` //does// reduce, and now the given
 constraint is `Coercible JObject (J ('Class "java.lang.Object"))`, or
 equivalently, `Coercible (J ('Class "java.lang.Object")) (J ('Class
 "java.lang.Object"))`, which //is// soluble!

 Perhaps this is revealing a typechecker implementation detail that
 inaccessible cases become deferred type errors if they are actually
 accessed?

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