Issue with overlapping instances

Learn
1

I’m playing a bit with MonadTrans and MFunctor from mmorph.

I defined a class Embeds and I’m trying to define the following instances

instance {-# OVERLAPPABLE #-} (Monad m, MonadTrans t, Embeds n m) => Embeds n (t m)

instance {-# OVERLAPPING #-} (Monad n, MFunctor t, Embeds n m) => Embeds (t n) (t m)

When I try to use those instances, I get the following error

      Overlapping instances for Embeds
                                  (StateT Int Identity) (StateT Int IO)
        arising from a use of ‘embed’
      Matching instances:
        instance [overlapping] forall k (n :: * -> *)
                                      (t :: (* -> *) -> k -> *) (m :: * -> *).
                               (Monad n, MFunctor t, Embeds n m) =>
                               Embeds (t n) (t m)
          -- Defined at Main.hs:30:30
        instance [overlappable] (Monad m, MonadTrans t, Embeds n m) =>
                                Embeds n (t m)
          -- Defined at Main.hs:25:31
      An overlapping instance can only be chosen when it is strictly more specific.
      The first instance that follows overlaps the second, but is not more specific than it:
        instance [overlapping] forall k (n :: * -> *)
                                      (t :: (* -> *) -> k -> *) (m :: * -> *).
                               (Monad n, MFunctor t, Embeds n m) =>
                               Embeds (t n) (t m)
        instance [overlappable] (Monad m, MonadTrans t, Embeds n m) =>
                                Embeds n (t m)

I would say that Embeds (t n) (t m) is strictly more specific than Embeds n (t m). Are also constraints considered when checking if a type is stricter than another?

Is there a way to say that I always want to use the second instance when both are available?

As a related question… if I use {-# INCOHERENT #-} for both instances, the code compiles correctly. Is that a safe/wise thing to do?

You can find the complete code here

2

The issue is that there are some hidden kind variables in play. You can fix it by giving Embeds an explicit kind signature:

import Data.Kind

type Embeds :: (Type -> Type) -> (Type -> Type) -> Constraint
class Embeds m n where
-- ...

Or alternatively, give the type variable a an explicit type:

class Embeds m n where
  embed :: forall (a :: Type). m a -> n a

(Or alternatively, alternatively, you could use NoPolyKinds)

I discovered this by trying to minimize your reproducer, but next time you can try adding -fprint-explicit-kinds. Then the error message becomes as follows:

Main.hs:46:3: error: [GHC-43085]
    • Overlapping instances for Embeds
                                  @{*} (StateT Int Identity) (StateT Int IO)
        arising from a use of ‘embed’
      Matching instances:
        instance [overlapping] forall k (n :: * -> *)
                                      (t :: (* -> *) -> k -> *) (m :: * -> *).
                               (Monad n, MFunctor @{k} t, Embeds @{*} n m) =>
                               Embeds @{k} (t n) (t m)
          -- Defined at Main.hs:33:30
        instance [overlappable] (Monad m, MonadTrans t, Embeds @{*} n m) =>
                                Embeds @{*} n (t m)
          -- Defined at Main.hs:28:31
      An overlapping instance can only be chosen when it is strictly more specific.
      The first instance that follows overlaps the second, but is not more specific than it:
        instance [overlapping] forall k (n :: * -> *)
                                      (t :: (* -> *) -> k -> *) (m :: * -> *).
                               (Monad n, MFunctor @{k} t, Embeds @{*} n m) =>
                               Embeds @{k} (t n) (t m)
        instance [overlappable] (Monad m, MonadTrans t, Embeds @{*} n m) =>
                                Embeds @{*} n (t m)
   |
46 |   embed statefulOperation
   |   ^^^^^

As you can see, while the t n is more specific than n, the kind k is actually more general than *.

3

Thanks a lot for the solution and the explanation!