[GHC] #12201: Wrong instance selection with overlapping instance in a superclass

[GHC]

#12201: Wrong instance selection with overlapping instance in a superclass
-------------------------------------+-------------------------------------
        Reporter:  kanetw            |                Owner:
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 This is a delicate point about overlapping instances, which has
 never really been discussed.  Here's what is happening.

 In `test_bar` we get one constraint so solve: `B (Foo s Bool)`.
 And there is an instance declaration that solves
 it
 {{{
 instance B (Foo s a)
 }}}
 So GHC 8 just solves it, and I think it is right to do so.  So we
 get
 {{{
 test_bar :: s -> Int
 }}}

 Why does GHC 7 behave differently?  GHC 7 used a tricky mechanism
 called "silent superclasses" to solve a tricky problem to do with
 recursive instances.  As a result, GHC 7 effectively changed the
 instance for `B (Foo s a)` to
 {{{
 instance A (Foo s a) => B (Foo s a)
 }}}
 Now when solving `B (Foo s Bool)` GHC 7 finds it needs `A (Foo s Bool)`,
 and can't solve that (because of the overlap in A), so it just abstract,
 giving
 {{{
 test_bar :: A (Foo s Bool) => s -> Int
 }}}

 So the mysterious thing is really why GHC 8 accepts the instance
 declaration
 {{{
 instance B (Foo s a)
 }}}
 After all, that instance must also solve `A (Foo s a)`, and that involves
 overlap.  And that behaviour is the result of a second tricky issue.
 Suppose class `A` had a class method, and `Foo` had a data constructor,
 looking like this:
 {{{
 data Foo s a = FNil | FCons a (Foo s a)

 class A a where
   op :: a -> Int

 instance A (Foo s a) where
   op FNil = 0
   op (FCons _ f) = op f   -- Needs A (Foo s a)!

 instance {-# OVERLAPPING #-} A (Foo Int Bool) where
   ...
 }}}

 When typechecking the commented line for `op`, we need to solve `A (Foo s
 a)`.
 And on this occasion it would be Bad to fail to solve it,
 saying "instance overlap".
 See `Note [Subtle interaction of recursion and overlap]` in `TcInstDcls`.
 So there is special magic to allow this to work.  (For the afficionados,
 we use `SkolemTv True` rather than `SkolemTv False` in the
 `TcTyVarDetails`.)

 Alas, this magic also applies to the superclass solving, but I now think
 that it should not do so.  Removing the magic would make the instance
 declaration be rejected; instead you would have to delay the superclass
 choice by writing
 {{{
 instance A (Foo s a) => B (Foo s a)
 }}}
 I think this is probably the right thing to do. Do others agree?

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