Lack of type inference results in failed compilation, no instance ambiguities

Question

I am stumped as to why this code compiles with type hints, but does not compile without. There shouldn't be any instance ambiguities (there is one instance).

class Monad m => FcnDef β m | β -> m where
    def :: String -> β -- takes a name

instance Monad m => FcnDef (m α -> m α) m where
    def s body = body

dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" ((return ()) :: m ())

On the other hand, if one omits the :: m (), or all type declarations, the compilation fails with this error,

No instance for (FcnDef (m0 () -> t0) m0)
  arising from a use of `def'

For clarification, the code is trying to make a multi-variate type for def, so one can write e.g.

def "dummy2" "input" $ \in -> return ()

Edit

This question is more intersting than a no monomorphism restriction issue. If one adds such code, then resolves instances to concrete types, namely

dummyTest = def "dummy" (return ())
g :: IO ()
g = dummyTest

the compilation fails similarly.

Answer 1

The need for the outer type signature is caused by the monomorphism restriction.

The giveaway for this is the left hand side of your definition.

dummyTest = ...

Since this definition does not have any arguments, the compiler will try to make the definition monomorphic. Adding the type signature overrides this behavior.

However, as you pointed out, this is not enough. For some reason the compiler is not able to infer the type of the inner expression. Why? Let's find out. Time to play type inference engine!

Let's start with the outer type and try to work out the type of the inner expression.

dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" (return ())

The type of def is FcnDef β m => String -> β, but here we have applied def to two arguments. This tells us that β must be a function type. Let's call it x -> y.

We can then easily infer that y must be equal to m (), in order to satisfy the outer type. Furthermore, the type of the argument return () is Monad m1 => m1 (), so we can deduce that the type of def we're looking for must have type FcnDef (m1 () -> m ()) m0 => def :: String -> m1 () -> m ().

Next, we'll proceed to look up the instance to use. The only instance available is not generic enough, as it requires that m1 and m are the same. So we complain loudly with a message like this:

Could not deduce (FcnDef (m1 () -> m ()) m0)
  arising from a use of `def'
from the context (Monad m)
  bound by the type signature for dummyTest :: Monad m => m ()
  at FcnDef.hs:10:1-51
Possible fix:
  add (FcnDef (m1 () -> m ()) m0) to the context of
    the type signature for dummyTest :: Monad m => m ()
  or add an instance declaration for (FcnDef (m1 () -> m ()) m0)
In the expression: def "dummy" ((return ()))
In an equation for `dummyTest':
    dummyTest = def "dummy" ((return ()))

The key thing to note here is that the fact that a particular instance happened to be lying around did not affect our choices while we were trying to infer the type.

So we're stuck with either having to specify this constraint manually using scoped type variables, or we can encode it in the type class.

class Monad m => FcnDef β m | β -> m where
    def :: String -> β -> β

instance Monad m => FcnDef (m α) m where
    def s body = body

-- dummyTest :: forall m. Monad m => m ()
dummyTest = def "dummy" (return ())

Now the type inference engine can easily determine that the monad of return must be the same as the monad in the result, and using NoMonomorphismRestriction we can also drop the outer type signature.

Of course, I'm not 100% sure what you're trying to accomplish here, so you'll have to be the judge of whether or not this makes sense in the context of what you're trying to do.