[GHC] #7296: ghc-7 assumes incoherent instances without requiring language `IncoherentInstances`

[GHC]

#7296: ghc-7 assumes incoherent instances without requiring language
`IncoherentInstances`
---------------------------------+------------------------------------------
    Reporter:  maeder            |       Owner:                             
        Type:  bug               |      Status:  new                        
    Priority:  normal            |   Milestone:                             
   Component:  Compiler          |     Version:  7.6.1                      
    Keywords:                    |          Os:  Unknown/Multiple           
Architecture:  Unknown/Multiple  |     Failure:  GHC accepts invalid program
  Difficulty:  Unknown           |    Testcase:                             
   Blockedby:                    |    Blocking:                             
     Related:                    |  
---------------------------------+------------------------------------------
Changes (by simonpj):

  * difficulty:  => Unknown


Comment:

 You are right, and this is tricky. The real error is that in the recursive
 call to `test` on line 16 of `Splittable.hs`, rather than rejecting the
 code (which is arguably right) GHC picks the `Test a Spec2` instance on
 line 20.

 But that's actually deliberate.  Here the note from `TcInstDcls`:
 {{{
 Note [Subtle interaction of recursion and overlap]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider this
   class C a where { op1,op2 :: a -> a }
   instance C a => C [a] where
     op1 x = op2 x ++ op2 x
     op2 x = ...
   instance C [Int] where
     ...

 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 excecuting 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.
 }}}
 But your example points out that my reasoning is flawed. I'm not sure
 exactly what to do, and I'm too swamped to think about it right now.  I
 hope it's not a show stopper for you.

 You can work around thus:
 {{{
 instance Test a Spec2 => Test a Spec1 where
  test a (MkSpec1 b) = map MkSpec1 $ test a b
 }}}
 which defers the choice to later, which is what we want.  Then you get
 `[]` for both tests.  Sadly you need `FlexibleContexts` and
 `UndecidableInstances` to persuade GHC to accept this instance.


 Simon

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