[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.2.1
       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 RyanGlScott):

 OK, I think I've got a hunch why this code is failing all of a sudden
 starting with GHC HEAD. As I mentioned earlier, this code was typechecking
 just fine up until d2958bd08a049b61941f078e51809c7e63bc3354. You can see
 what code ghc is filling in with `-ddump-deriv`:

 {{{
 $ /opt/ghc/head/bin/ghc Bug.hs -ddump-deriv
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 ==================== Filling in method body ====================
 Bug.Foo [GHC.Types.Char]
   Bug.foo = Bug.$dmfoo @GHC.Types.Char
 }}}

 If I try to implement something like `$dmfoo` manually, I can get the same
 error:

 {{{#!hs
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 module Bug where

 class Foo a where
   foo :: (a ~ Int => Int) -> a -> a
   foo = fooDefault

 fooDefault :: (a ~ Int => Int) -> a -> a
 fooDefault _ a2 = a2

 instance Foo Char where
   foo = fooDefault @Char
 }}}

 {{{
 $ /opt/ghc/head/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:14:9: error:
     • Couldn't match type ‘Char’ with ‘Int’
       Inaccessible code in
         a type expected by the context:
           Char ~ Int => Int
     • In the expression: fooDefault @Char
       In an equation for ‘foo’: foo = fooDefault @Char
       In the instance declaration for ‘Foo Char’
 }}}

 So it's apparent that this behavior is different from before.
 Unfortunately, `-ddump-deriv` doesn't output this defaulting information
 on GHC 8.0.1 and earlier, so all we have to work with is `-ddump-simpl`.
 Compiling the original program with `-ddump-simpl` on GHC 8.0.1 yields:

 {{{
 -- RHS size: {terms: 3, types: 7, coercions: 0}
 $cfoo_rCm :: ((Char :: *) ~ (Int :: *) => Int) -> Char -> Char
 [GblId, Arity=2, Caf=NoCafRefs, Str=DmdType]
 $cfoo_rCm = \ _ [Occ=Dead] (a2_aBf :: Char) -> a2_aBf

 -- RHS size: {terms: 1, types: 0, coercions: 3}
 Bug.$fFooChar [InlPrag=INLINE (sat-args=0)] :: Foo Char
 [GblId[DFunId(nt)], Arity=2, Caf=NoCafRefs, Str=DmdType]
 Bug.$fFooChar =
   $cfoo_rCm
   `cast` (Sym (Bug.N:Foo[0] <Char>_N)
           :: ((((Char :: *) ~ (Int :: *) => Int) -> Char -> Char) :: *)
              ~R#
              (Foo Char :: Constraint))
 }}}

 I'm not sure if I'm reading that correctly, but I //think// that instead
 of defining `$cfoo_rCm` in terms of `$dmfoo`, GHC is inlining the
 definition of `$dmfoo` directly into `$cfoo` (which has so far accounted
 for the difference between a succesfully typechecked program and one that
 fails).

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