Opened 2 years ago

Last modified 2 months ago

#7296 new bug

ghc-7 assumes incoherent instances without requiring language `IncoherentInstances`

Reported by: maeder Owned by: simonpj
Priority: normal Milestone: 7.12.1
Component: Compiler (Type checker) Version: 7.6.1
Keywords: Cc: sternkinder@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC accepts invalid program Test Case:
Blocked By: Blocking:
Related Tickets: #9820 Differential Revisions:

Description

the attached examples works with ghc-7 and returns

    *Main> a
    [Spec1 Spec2]
    *Main> b
    []

(One may wish that b also returned [Spec1 Spec2])

ghc-6 complains with

Splittable.hs:16:36:
    Overlapping instances for Test a Spec2
      arising from a use of `test' at Splittable.hs:16:36-43
    Matching instances:
      instance [overlap ok] Test a Spec2
        -- Defined at Splittable.hs:20:13-24
      instance [overlap ok] Test Bool Spec2
        -- Defined at Splittable.hs:25:13-27
    (The choice depends on the instantiation of `a'
     To pick the first instance above, use -XIncoherentInstances
     when compiling the other instance declarations)
    In the second argument of `($)', namely `test a b'
    In the expression: map Spec1 $ test a b
    In the definition of `test':
        test a (Spec1 b) = map Spec1 $ test a b
Failed, modules loaded: none.

After adding IncoherentInstances the file also goes through ghc-6 with the same results.

Attachments (1)

Splittable.hs (500 bytes) - added by maeder 2 years ago.

Download all attachments as: .zip

Change History (9)

Changed 2 years ago by maeder

comment:1 Changed 2 years ago by maeder

I meant, one may wish that a and b returned equal results, namely that a returned "[]" by using the more special instance of Spec2 in the instance definition of Spec1.

comment:2 Changed 2 years ago by simonpj

  • difficulty set to Unknown

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

comment:3 Changed 2 years ago by maeder

Thanks for this analysis, it is no show stopper for us.

comment:4 Changed 23 months ago by igloo

  • Component changed from Compiler to Compiler (Type checker)
  • Milestone set to 7.8.1
  • Owner set to simonpj

comment:5 Changed 10 months ago by thoughtpolice

  • Milestone changed from 7.8.3 to 7.10.1

Moving to 7.10.1

comment:6 Changed 3 months ago by thomie

comment:7 Changed 3 months ago by goldfire

See #9820 for another example of how this might happen. (I don't believe #8338 is related to this ticket.)

comment:8 Changed 2 months ago by thoughtpolice

  • Milestone changed from 7.10.1 to 7.12.1

Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

Note: See TracTickets for help on using tickets.