Why can't Haskell unify my types when using a constraint as class parameter?

Question

I am trying to split my code into nice modules. However, while doing this, one of the classes I have in the imported module (Outer in Module 1 below) needs a constraint that is only known in the importing module (Inner in Module 1). I tried to solve this by giving the class Outer this constraint as variable c, which seems to work.

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Main where

-- Module 1
data A = A
data B = B
data C = C

class Runners c where
        runA :: (forall w. (c w) => w a) -> A
        runB :: (forall w. (c w) => w a) -> B
        runC :: (forall w. (c w) => w a) -> C

class (Runners c, Monad v) => Outer c v where
        fn :: (forall w. (c w) => w a) -> v a

-- Module 2

usage :: (Outer Inner v) => a -> v a
usage a = fn (foo a >>= foo >>= foo)

class Monad w => Inner w where
        foo :: a -> w a

-- Main
main :: IO ()
main = putStrLn "Hello, Haskell!"

However, I now get an error I do not understand:

• Could not deduce (Outer c0 v) arising from a use of ‘fn’
  from the context: Outer Inner v
    bound by the type signature for:
               usage :: forall (v :: * -> *) a. Outer Inner v => a -> v a
    at /home/niek/projects/papers/2-staged-interpreter-generated-c/mwe/app/Main.hs:25:1-36
  The type variable ‘c0’ is ambiguous
  Relevant bindings include
    usage :: a -> v a
      (bound at /home/niek/projects/papers/2-staged-interpreter-generated-c/mwe/app/Main.hs:26:1)
• In the expression: fn (foo a >>= foo >>= foo)
  In an equation for ‘usage’: usage a = fn (foo a >>= foo >>= foo)typecheck(-Wdeferred-type-errors)

The first two lines say it all. Outer c0 v cannot be deduced to be Outer Inner v. I cannot figure out what this means or why this error occur. To me, it seems very easily unifiable, though the constraint solver probably uses a different algorithm to the unification algorithm?

Answer 1

In Haskell, the constraint solver never reasons by elimination. This is also known as the "open world assumption".

In this case, there could be another instance Outer Foo v somewhere else which would match the wanted Outer c0 v constraint just as well.

One simple way to specify that Outer Inner v is really the only suitable instance is to add a functional dependency from v to c:

{-# LANGUAGE FunctionalDependencies #-}
class (Runners c, Monad v) => Outer c v | v -> c where
        fn :: (forall w. (c w) => w a) -> v a

This says that there cannot be two instances Outer c1 v and Outer c2 v, so the c part must always be equal if the v part is equal.

Your example is too minimal for me to tell whether this is the right solution for you or whether you intend something else.