Opened 3 years ago

Closed 3 years ago

Last modified 15 months ago

#12201 closed bug (invalid)

Wrong instance selection with overlapping instance in a superclass

Reported by: kanetw Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: Instances Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description (last modified by kanetw)

test_foo and test_bar should have the same type, but it seems like the non-{#- OVERLAPPING #-} instance is chosen prematurely.

{-# LANGUAGE NoMonomorphismRestriction, FlexibleContexts, FlexibleInstances #-}
module Bug where

class A a where
class A a => B a where

data Foo s a
instance {-# OVERLAPPING #-} A (Foo Int Bool)
instance A (Foo s a)
instance B (Foo s a)

helper :: Foo s Bool -> s -> Int
helper = undefined

foo :: (A a, B a) => a
foo = undefined

bar :: B a => a
bar = undefined

{-
  *Bug> :t test_foo 
  test_foo :: A (Foo s Bool) => s -> Int
-}
test_foo = helper foo

{-
  *Bug> :t test_bar
  test_bar :: s -> Int
-}
test_bar = helper bar

Compare with 7.10.3:

*Bug> :t test_foo
test_foo :: A (Foo s Bool) => s -> Int
*Bug> :t test_bar
test_bar :: A (Foo s Bool) => s -> Int

Change History (8)

comment:1 Changed 3 years ago by kanetw

Description: modified (diff)

comment:2 Changed 3 years ago by kanetw

Still present on latest HEAD:

GHCi, version 8.1.20160616: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Bug              ( /home/kane/ghc8-instance-bug/Bug.hs, interpreted )

/home/kane/ghc8-instance-bug/Bug.hs:22:1: warning: [-Wsimplifiable-class-constraints]
    The constraint ‘A (Foo s Bool)’ matches an instance declaration
    instance A (Foo s a)
      -- Defined at /home/kane/ghc8-instance-bug/Bug.hs:9:10
    This makes type inference very fragile;
      try simplifying it using the instance
Ok, modules loaded: Bug.
*Bug> :t test
test :: A (Foo s Bool) => s -> Int
*Bug> :t test2
test2 :: s -> Int

comment:3 Changed 3 years ago by kanetw

GHC doesn't seem to check superclass constraints for overlap before solving.

{-# LANGUAGE NoMonomorphismRestriction, FlexibleContexts, FlexibleInstances #-}
module Bug where

class A a where
class A a => B a where

data Foo s a
instance {-# OVERLAPPING #-} A (Foo Int Bool)
instance A (Foo s a)
instance B (Foo s a)

helper :: Foo s Bool -> s -> Int
helper = undefined

foo :: (A a, B a) => a
foo = undefined

bar :: B a => a
bar = undefined

{-
  *Bug> :t test_foo 
  test_foo :: A (Foo s Bool) => s -> Int
-}
test_foo = helper foo

{-
  *Bug> :t test_bar
  test_bar :: s -> Int
-}
test_bar = helper bar

GHC7 works as expected. I suspect the recent superclass solver changes caused this.

comment:4 Changed 3 years ago by kanetw

Description: modified (diff)
Summary: Wrong instance selection with overlapping instances and local bindingsWrong instance selection with overlapping instance in a superclass

comment:5 Changed 3 years ago 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?

comment:6 Changed 3 years ago by kanetw

That sounds like the right thing to do. It feels a bit unpleasant from an aesthetics perspective, but I can't really think of a better solution.

comment:7 Changed 3 years ago by bgamari

Resolution: invalid
Status: newclosed

Closing since there appears to be no better ideas on the table. Feel free to re-open if you have a better alternative.

comment:8 Changed 15 months ago by simonpj

Keywords: Instances added
Note: See TracTickets for help on using tickets.