[GHC] #12832: GHC infers too simplified contexts

[GHC]

#12832: GHC infers too simplified contexts
-------------------------------------+-------------------------------------
        Reporter:  danilo2           |                Owner:
            Type:  bug               |               Status:  new
        Priority:  high              |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
 Type of failure:  Incorrect         |  Unknown/Multiple
  error/warning at compile-time      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 There is a reason for this behaviour.  I won't say that it is a ''good''
 reason, but it's not an accident.  See this note in `TcInstDcls`:
 {{{
 Note [Subtle interaction of recursion and overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this
   class C a where { op1,op2 :: a -> a }
   instance {-# OVERLAPPING #-} C [Int] where
     ...
   instance {-# OVERLAPPABLE #-} C a => C [a] where
     op1 x = op2 x ++ op2 x
     op2 x = ...
     ...

 When type-checking the C [a] instance, we need a C [a] dictionary (for
 the call of op2).  If we look up in the instance environment, we find
 an overlap.  And in *general* the right thing is to complain (see Note
 [Overlapping instances] in InstEnv).  But in *this* case it's wrong to
 complain, because we just want to delegate to the op2 of this same
 instance.

 Why is this justified?  Because we generate a (C [a]) constraint in
 a context in which 'a' cannot be instantiated to anything that matches
 other overlapping instances, or else we would not be executing this
 version of op1 in the first place.

 It might even be a bit disguised:

   nullFail :: C [a] => [a] -> [a]
   nullFail x = op2 x ++ op2 x

   instance C a => C [a] where
     op1 x = nullFail x

 Precisely this is used in package 'regex-base', module Context.hs.
 See the overlapping instances for RegexContext, and the fact that they
 call 'nullFail' just like the example above.  The DoCon package also
 does the same thing; it shows up in module Fraction.hs.

 Conclusion: when typechecking the methods in a C [a] instance, we want to
 treat the 'a' as an *existential* type variable, in the sense described
 by Note [Binding when looking up instances].  That is why
 isOverlappableTyVar
 responds True to an InstSkol, which is the kind of skolem we use in
 tcInstDecl2.
 }}}
 In your example, from
 {{{
 instance Run m Int where
   run = test
 }}}
 we get a Wanted `[W] Test m Int` constraint.  Because it's in an instance
 decl, the `m` type variable has the above magic overlap property, we
 apply the instance declaration to get `[W] (Foo m, Bar m, Baz m)`.

 I don't say this is great, but I'm not sure what else to do.

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