Clarification on overlapping instance candidate elimination

Learn
#1

I have a GADT that captures some equality info and a GetFoo class that produces a Foo a b:

data Foo :: Type -> Type -> Type where
  FooNotEq :: Foo a b
  FooEq :: Foo a a
  FooPairEq :: Foo (a, a) (a, a)

type GetFoo :: Type -> Type -> Constraint
class GetFoo a b where
  getFoo :: Foo a b

When writing instances for GetFoo, I can write them in different ways in regards to OVERLAPPABLE/OVERLAPPING pragmas:

instance {-# OVERLAPPABLE #-} GetFoo a b where
  getFoo = FooNotEq

instance {-# OVERLAPPABLE #-} GetFoo a a where
  getFoo = FooEq

instance GetFoo (a, a) (a, a) where
  getFoo = FooPairEq

or

instance GetFoo a b where
  getFoo = FooNotEq

instance {-# OVERLAPPING #-} GetFoo a a where
  getFoo = FooEq

instance {-# OVERLAPPING #-} GetFoo (a, a) (a, a) where
  getFoo = FooPairEq

or even

instance {-# OVERLAPPABLE #-} GetFoo a b where -- OVERLAPPING here is also fine
  getFoo = FooNotEq

instance {-# OVERLAPPING #-} GetFoo a a where
  getFoo = FooEq

instance {-# OVERLAPPING #-} GetFoo (a, a) (a, a) where
  getFoo = FooPairEq

This last chunk of instances confuses me though, according to the verbiage in instance overlap section of the user guide. With getFoo @Int @Int for example, I would expect that the GetFoo a b and GetFoo a a instances would be the “candidates”. The candidate elimination logic is described as follows:

  • Eliminate any candidate 𝐼𝑋 for which there is another candidate 𝐼𝑌 such that both of the following hold:
    • 𝐼𝑌 is strictly more specific than 𝐼𝑋. That is, 𝐼𝑌 is a substitution instance of 𝐼𝑋 but not vice versa.
    • Either 𝐼𝑋 is overlappable, or 𝐼𝑌 is overlapping. (This “either/or” design, rather than a “both/and” design, allow a client to deliberately override an instance from a library, without requiring a change to the library.)

So for condition 1, I would expect GetFoo a a to be more specific than GetFoo a b, so that one holds. For condition 2 though, it would seem that the “either/or” bit isn’t enforced. Assuming IY is GetFoo a a and IX is GetFoo a b, IY is overlapping and IX is overlappable (not either/or) in the above example. I would expect condition 2 to not hold, but from a simple test, GHC is happy (and correctly picks GetFoo a a):

spec :: Spec
spec = do
  describe "getFoo" do
    it "FooEq" do
      getFoo @Int @Int `shouldBe` FooEq

Is there something I’m missing in the overlap docs describing why GHC is happy in this case?

#2

I think the problem is that you are interpreting condition 2 to mean “Either 𝐼𝑋 is overlappable, or 𝐼𝑌 is overlapping, but not both”, but the actual rule is “Either 𝐼𝑋 is overlappable, or 𝐼𝑌 is overlapping, or both are true (both 𝐼𝑋 is overlappable and 𝐼𝑌 is overlapping)”. That is, the condition is OR not XOR.

The comment about choosing an “either/or” design instead of a “both/and” design implies that if you are declaring all the types yourself, you’d probably be fine with the stricter, “AND” version of condition 2 (requiring that both (a) 𝐼𝑋 is overlappable and (b) 𝐼𝑌 is overlapping). So it would make no sense to disallow candidate elimination when both (a) and (b) are true.

1 Like
#3

Ah, that’s very helpful - thanks!

The comment on “either/or” vs. “both/and” in the guide definitely contributed to me interpreting things as xor. Perhaps the user guide could avoid potential future confusion for readers if the “Either” bit was changed, e.g.:

Either 𝐼𝑋 is overlappable, or 𝐼𝑌 is overlapping. (This “either/or” design, rather than a “both/and” design, allow a client to deliberately override an instance from a library, without requiring a change to the library.)

could become

𝐼𝑋 is overlappable or 𝐼𝑌 is overlapping. (This “or” design, rather than an “and” design, allows a client to deliberately override an instance from a library, without requiring a change to the library.)

I’d be happy to PR this.

2 Likes
#4

Please do – thank you!

#5

In general, I prefer to mark the instances that are OVERLAPPABLE, as a visual warning when reading code to keep an eye out for more specific instances.

This is particularly helpful with separate compilation (the deadly ‘orphan instances’), to warn that an OVERLAPPABLE instance in the imported module might get gazumped by a more specific instance in the importing module.

I have the impression (perhaps I’m making this up) that if GHC sees OVERLAPPABLE and the instance is more general than is [W]anted at the usage site, GHC defers selecting that instance in case this module gets imported to somewhere a more specific instance is available(?)

1 Like
#6

For future readers, the user guide verbiage change proposed earlier in the thread has been incorporated here.