#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