Unexpected Overlapping instances error

Question

I have the following code. Class1 instances say what the direct superclass is of a class, SuperClass1 automatically traverses Class1 to find all superclasses. (I have omitted the actual methods of these classes because they are not relevant for my issue.)

{-# LANGUAGE PolyKinds, RankNTypes, ConstraintKinds, FlexibleInstances, UndecidableInstances, MultiParamTypeClasses, FunctionalDependencies #-}

class Class1 b h | h -> b
instance Class1 Functor Applicative
instance Class1 Applicative Monad

class SuperClass1 b h
instance {-# OVERLAPPING #-} SuperClass1 b b
instance {-# OVERLAPPABLE #-} (SuperClass1 b c, Class1 c h) => SuperClass1 b h

This works great! Now I want to use it like this:

newtype HFree c f a = HFree { runHFree :: forall g. c g => (forall b. f b -> g b) -> g a }

instance SuperClass1 Functor c => Functor (HFree c f)
instance SuperClass1 Applicative c => Applicative (HFree c f)
instance SuperClass1 Monad c => Monad (HFree c f)

test :: (a -> b) -> HFree Monad f a -> HFree Monad f b
test = fmap

(I.e. I can give an instance of Functor for Hfree c f whenever Functor is a superclass of c.)

And this gives this error in the Applicative instance (and similar for the Monad instance):

• Overlapping instances for SuperClass1 Functor c1
    arising from the superclasses of an instance declaration
  Matching instances:
    instance [overlappable] forall k k k (b :: k) (c :: k) (h :: k).
                            (SuperClass1 b c, Class1 c h) =>
                            SuperClass1 b h
      -- Defined at superclass.hs:17:31
    instance [overlapping] forall k (b :: k). SuperClass1 b b
      -- Defined at superclass.hs:16:30
  (The choice depends on the instantiation of ‘c1, k1’
   To pick the first instance above, use IncoherentInstances
   when compiling the other instance declarations)
• In the instance declaration for ‘Applicative (HFree c f)’

As far as I understand, what happens is that an Applicative instance requires a Functor instance, so the Applicative instance also needs the SuperClass1 Functor c constraint from Functor. And indeed if I add this, the error goes away. (This is what I currently have: http://hackage.haskell.org/package/free-functors-0.7/docs/Data-Functor-HFree.html)

But somehow GHC is smart enough to understand that SuperClass1 Applicative c implies SuperClass1 Functor c, because it doesn't complain about a missing constraint. Instead it gets stuck on an overlapping instances error. It would be great if there's a way to fix the error, but I can't figure out how!

Answer 1

But somehow GHC is smart enough to understand that SuperClass1 Applicative c implies SuperClass1 Functor c, because it doesn't complain about a missing constraint.

I fear you are being too hopeful - GHC is probably working its way from the other end and giving up immediately: it sees fmap and tries to check that HFree is a Functor. It has only one instance to pick from: SuperClass1 Functor c => Functor (HFree c f). Then, it starts trying to satisfy the constraint on that instance (SuperClass1 Functor c) and suddenly realizes it doesn't know what to do - there are two instances it could pick:

• SuperClass1 b b
• SuperClass1 b h

Notice that I left out the constraints on these instances - that's because GHC needs to commit to an instance before even looking at the constraints on the left hand side. With that said, @user2407038's comment is quite true: your instances overlap pretty badly - GHC doesn't know a priori if it should try to unify b ~ Functor and b ~ c or b ~ Functor and h ~ c. Both could work.

If it was the case that picking either would work, you should turn on IncoherentInstances. This is, unfortunately, not the case here. You know that you want the second instance picked, but GHC doesn't.

---

I've recently been toying around with a similar sort of problem but in relation to subtyping but no matter how you go about it, instance resolution is really hard. My advice to you is to use type families when you can.

EDIT

Here is a solution to get your code to compile, except relying on type families instead of type-classes. The setup machinery is

{-# LANGUAGE PolyKinds, ConstraintKinds, TypeFamilies, UndecidableInstances, DataKinds, TypeOperators #-}

import Data.Kind (Constraint)

-- Find transitively all the superclasses of a constraint (including itself)
type family SuperClasses (x :: k -> Constraint) :: [k -> Constraint]
type instance SuperClasses Functor = '[Functor]
type instance SuperClasses Applicative = Applicative ': SuperClasses Functor
type instance SuperClasses Monad = Monad ': SuperClasses Applicative

-- Type level version of `elem` which is a Constraint
type family Elem (x :: k) (xs :: [k]) :: Constraint where
  Elem a (a ': bs) = ()
  Elem a (b ': bs) = Elem a bs

-- Type level version of checking the first list is a subset of the second
type family Subset (xs :: [k]) (ys :: [k]) :: Constraint where
  Subset '[] bs = ()
  Subset (a ': as) bs = (Elem a bs, Subset as bs)

-- Tell us whether the constraint x is a sub-constraint (thereby implied by) y
type x <: y = SuperClasses x `Subset` SuperClasses y

Then, applied to Functor, Applicative, and Monad, we need

-- I've cropped the body of HFree since it is of no interest here
data HFree c f a

instance Functor     <: c => Functor     (HFree c f)
instance Applicative <: c => Applicative (HFree c f)
instance Monad       <: c  => Monad      (HFree c f)

And here are some tests

-- Compiles
test1 :: (a -> b) -> HFree Monad f a -> HFree Monad f b
test1 = fmap

-- Compiles
test2 :: a -> HFree Monad f a
test2 = pure

-- Doesn't compile
test3 :: a -> HFree Functor f a
test3 = pure