Type classes, functional dependencies, and arity

[noughtmare]

I was just writing some code involving type classes:

import Control.Monad.Except

class InSum x xs where
  inject :: x -> xs

instance InSum x (Either x xs) where
  inject = Left

instance InSum x xs => InSum x (Either y xs) where
  inject = Right . inject

throw :: (InSum e es, MonadError es m) => e -> m a
throw = throwError . inject

data ErrorA = ErrorA deriving Show
data ErrorB = ErrorB deriving Show
data Result
data Input

x :: Input
x = undefined

f :: forall es m . (InSum ErrorA es, MonadError es m) => Input -> m Result
f = throw ErrorA

This produces the error:

T.hs:25:5: error:
    • Could not deduce (InSum ErrorA es0) arising from a use of ‘throw’
      from the context: (InSum ErrorA es, MonadError es m)
        bound by the type signature for:
                   f :: forall es (m :: * -> *).
                        (InSum ErrorA es, MonadError es m) =>
                        Input -> m Result
        at T.hs:24:1-74
      The type variable ‘es0’ is ambiguous
      Potentially matching instances:
        instance InSum x (Either x xs) -- Defined at T.hs:7:10
        instance InSum x xs => InSum x (Either y xs)
          -- Defined at T.hs:10:10
    • In the expression: throw ErrorA
      In an equation for ‘f’: f = throw ErrorA
   |
25 | f = throw ErrorA
   |     ^^^^^

I'd say this error message is mostly useless. For who hasn't spotted the mistake yet: the issue is that f should take one argument, but I've not written that explicitly so now it thinks the monad of throw is the function monad. So the simple fix is to write:

f _ = throw ErrorA

The order of the constraints I chose in throw :: (InSum e es, MonadError es m) => e -> m a makes the error message much worse. If I swap those two constraints I get the much more useful error message:

T.hs:25:5: error:
    • Could not deduce (MonadError es0 ((->) Input))
        arising from a use of ‘throw’
      from the context: (InSum ErrorA es, MonadError es m)
        bound by the type signature for:
                   f :: forall es (m :: * -> *).
                        (InSum ErrorA es, MonadError es m) =>
                        Input -> m Result
        at T.hs:24:1-74
      The type variable ‘es0’ is ambiguous
    • In the expression: throw ErrorA
      In an equation for ‘f’: f = throw ErrorA
   |
25 | f = throw ErrorA
   |     ^^^^^

Still, I would expect in this case the suggestion that there might be something wrong with the arity of a function somewhere.

I think the simplest way to improve this error message is just to include all unsolved constraints in the error message. Or at least those that mention the same variables as the "main" unsolved constraint. And especially if another constraint has a functional dependency that would determine the concrete type if it were to be resolved.

[goldfirere]

That sounds like a very reasonable, implementable suggestion.