FunctionalDependencies does not unify on uniquely identified type

Question

Here is the definition for MonadState, but question applies to any such class with FunctionalDependencies:

class Monad m => MonadState s m | m -> s where
...

Consider I have data type that uses s as the type argument and a type class that works works with it:

data StateType s = StateType

class MonadState s m => FunDeps s m a where
  workWithStateType :: a -> StateType s -> m ()

I can happily create an instance for this class which compiles and works as expected:

instance (MonadIO m, MonadState s m) => FunDeps s m (IORef (StateType s)) where
  workWithStateType ref a = liftIO $ writeIORef ref a

But it feels to me that s in FunDeps class is redundant and I could define a class like so:

class FunDepsProblem m a where
  workWithStateTypeNoCompile :: MonadState s m => a -> StateType s -> m ()

instance (MonadIO m, MonadState s m) => FunDepsProblem m (IORef (StateType s)) where
  ...

The problem is when I try to implement it:

instance (MonadIO m, MonadState s m) => FunDepsProblem m (IORef (StateType s)) where
  workWithStateTypeNoCompile ref a = liftIO $ writeIORef ref a

I get a compilation error that tells me that it can't unify the state token s in the instance head and in the function:

fun-deps.hs:18:62: error: …
    • Couldn't match type ‘s1’ with ‘s’
      ‘s1’ is a rigid type variable bound by
        the type signature for:
          workWithStateTypeNoCompile :: forall s1.
                                        MonadState s1 m =>
                                        IORef (StateType s) -> StateType s1 -> m ()
        at /path/to/fun-deps.hs:18:3-28
      ‘s’ is a rigid type variable bound by
        the instance declaration
        at /path/to/fun-deps.hs:17:10-78
      Expected type: StateType s
        Actual type: StateType s1
    • In the second argument of ‘writeIORef’, namely ‘a’
      In the second argument of ‘($)’, namely ‘writeIORef ref a’
      In the expression: liftIO $ writeIORef ref a
    • Relevant bindings include
        a :: StateType s1
          (bound at /path/to/fun-deps.hs:18:34)
        ref :: IORef (StateType s)
          (bound at /path/to/fun-deps.hs:18:30)
        workWithStateTypeNoCompile :: IORef (StateType s)
                                      -> StateType s1 -> m ()
          (bound at /path/to/fun-deps.hs:18:3)
   |
Compilation failed.

I understand that when it is defined in such form there is an implicit forall there:

  workWithStateTypeNoCompile :: forall s m a . MonadState s m => a -> StateType s -> m ()

so technically it should work for every s, and it would totally make sense with absence of FunctionalDependencies, but s is known when m is known, so that is the part that I don't get.

In other words the monad m is unified to be the same in the class head and in the function, so it should uniquely identify the state type s both in instance head and in the function type. So my question is how come it is not being unified? Is there a theoretical reason for this or is it simply not implemented in ghc?

In fact, if I rewrite MonadState into a conceptually the same functionality, but using TypeFamilies instead of FunctionalDependencies the problem seem to go away:

class Monad m => MonadStateFamily m where
  type StateToken m :: *

class Family m a where
  familyStateType :: MonadStateFamily m => a -> StateType (StateToken m) -> m ()

instance (MonadIO m, MonadStateFamily m, s ~ StateToken m) => Family m (IORef (StateType s)) where
  familyStateType ref a = liftIO $ writeIORef ref a

Answer 1

Apparently this is a known limitation of FunctionalDependencies. I dug up a Haskell-cafe message by Manuel Chakravarty from over a decade ago which mentions that FunctionalDependencies don't work with existential types and provided a very concise and clear example:

class F a r | a -> r
instance F Bool Int

data T a = forall b. F a b => MkT b

add :: T Bool -> T Bool -> T Bool
add (MkT x) (MkT y) = MkT (x + y)

Example above produces the compiler error which says that it can't unify on the uniquely identified type, essentially the title of the question.

    • Couldn't match expected type ‘b’ with actual type ‘b1’
      ‘b1’ is a rigid type variable bound by
        a pattern with constructor: MkT :: forall a b. F a b => b -> T a,
        in an equation for ‘add’

This is the compilation error from the question, which looks very similar to the one above.

    • Couldn't match type ‘s1’ with ‘s’
      ‘s1’ is a rigid type variable bound by
        the type signature for:
          workWithStateTypeNoCompile :: forall s1.
                                        MonadState s1 m =>
                                        IORef (StateType s) -> StateType s1 -> m ()

I suspect that exactly the same concepts are at play here, because of the forall on the workWithStateTypeNoCompile, the type variable s1 in the error is the existential.

In any case not all is lost and there is a decent workaround for the problem I was having. In particular removal of the s from the class instance head is necessary, which can be achieved with a newtype:

class FunDepsWorks m a where
  workWithStateTypeCompile :: MonadState s m => a s -> StateType s -> m ()

newtype StateTypeRef s = StateTypeRef (IORef (StateType s))

instance MonadIO m => FunDepsWorks m StateTypeRef where
  workWithStateTypeCompile (StateTypeRef ref) a = liftIO $ writeIORef ref a

Note that the a is now a type variable with arity one and is applied to s.

Thanks to Ben Gamari for compiling tf vs fd wiki page, otherwise I would have never found that example with existential types.