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

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
  开发者_C百科  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.

---

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.

---

As @pigworker noted in a comment:

Instance inference is defensive with respect to possible future instances. Looks like your instance head has the same var twice. It won't fire unless something else forces those types to be the same.

This is indeed the essential problem, and While @hammar's approach of adding an extra parameter is probably the most generally useful solution, in a case like this we can make an observation, and then twist a weakness of the instance selection mechanism to our benefit. To start with, note that we can't write two instances like this:

instance Monad m => FcnDef (m α -> m α) m where -- etc...
instance Monad m => FcnDef (m1 α -> m2 b) m3 where -- etc...

Why not? Somewhat perversely, because they overlap too much. The distinct type variables in the second case could of course be reasonably instantiated with the same types and thus match the first instance; and the OverlappingInstances extension won't really help here.

Given that the first instance is what we want in this case, and that the overlapping means we could never add the second instance anyway, we can pull a fast one on GHC. We'll start by actually writing the second, generic instance, but then we'll slip something into the context (which is only examined afterwards!) that forcibly unifies the types. If you enable TypeFamilies you can use ~ to good effect here, and write this:

instance (m1 ~ m2, m2 ~ m3, a ~ b, Monad m) => FcnDef (m1 α -> m2 b) m3 where -- etc...

What will happen here is that GHC will select the generic instance here regardless of types, then attempt to unify them to satisfy the constraint. If they can't unify, you get a type checking error, as expected and desired. If they match, all is well. But the important part is that, unlike your code, if they could unify but are still ambiguous, this will cause them to be unified.

In most cases it's a real pain that instance selection ignores the context, but it's actually pretty useful in this scenario.