
#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