How are these two instances overlapping (involving out-of-scope types)

Question

I couple of days ago I asked a question about injecting functors in the context of free-monads. The solution suggested there, based on Data Types à la Carte uses a class that represents a sort of containment relationship between functors.

-- | Class that represents the relationship between a functor 'sup' containing
-- a functor 'sub'.
class (Functor sub, Functor sup) => sub :-<: sup where
    inj :: sub a -> sup a

-- | A functor contains itself.
instance Functor f => f :-<: f where
    inj = id

-- | A functor is contained in the sum of that functor with another.
instance (Functor f, Functor g) => f :-<: (Sum f g) where
    inj = InL

-- | If a functor 'f' is contained in a functor 'g', then f is contained in the
-- sum of a third functor, say 'h', with 'g'.
instance (Functor f, Functor g, Functor h, f :-<: g) => f :-<: (Sum h g) where
    inj = InR . inj

Now consider the following data types:

type WeatherData = String

data WeatherServiceF a = Fetch (WeatherData -> a) deriving (Functor)

data StorageF a = Store WeatherData a deriving (Functor)

And a function with the following type

fetch :: (WeatherServiceF :-<: g) => Free g WeatherData

Where Free comes from the Control.Monad.Free module.

Then if I try to use this function as follows:

reportWeather :: Free (Sum WeatherServiceF StorageF) ()
reportWeather = do
    _ <- fetch
    return ()

I get an overlapping-instances error, saying:

• Overlapping instances for WeatherServiceF
                            :-<: Sum WeatherServiceF StorageF
    arising from a use of ‘fetch’
  Matching instances:
    two instances involving out-of-scope types
      instance (Functor f, Functor g) => f :-<: Sum f g

      instance (Functor f, Functor g, Functor h, f :-<: g) =>
               f :-<: Sum h g

Now, I understand that the first is a valid instance, but why the second is considered a valid instance as well? If I instantiate the variables in the second case I would get

instance ( Functor WeatherServiceF
         , Functor StorageF
         , Functor WeatherServiceF
         , WeatherServiceF :-<: StorageF
         ) => WeatherServiceF :-<: Sum WeatherServiceF g

Which should not be an instance since it is not true that WeatherServiceF :-<: StorageF. Why is GHC inferring such an instance?

I have the following instances enabled:

{-# LANGUAGE DeriveFunctor         #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators         #-}

Ben Ben · Accepted Answer · 2017-11-22T10:20:37

The compiler has to be able to select instances by considering only the "head" of the instance, without looking at the constraints. The constraints are only considered once the applicable instance has been chosen. If it cannot decide between two instances looking only at the head, then they overlap.

The reason is that there is no guarantee that all of the instances used in the final complete program will be imported into this module. If the compiler ever committed to choosing an instance based on not being able to see an instance fulfilling a constraint of another instance, then different modules could make different choices about which of the two overlapping instances to use for the same type, based on the different set of instances available in each.

The overlap check is intended to stop that happening. So the only way it can do that is if GHC treats all constraints as at least potentially satisfiable when it's seeing which instances might apply in a given situation. When that leaves exactly one candidate, that candidate will remain regardless of what other instances are added or removed elsewhere in the program. It can then check that the necessary instances are available in this module to satisfy the constraints.

How are these two instances overlapping (involving out-of-scope types)

1 Answers