[Ur] Poor inference of monads over "non-canonical" types

[Evan Danaher]

I'm writing a simple parser, and decided to try my hand at a
Parsec-like monadic combinator approach.  Unfortunately, it seems that
monad inference is fairly weak; consider the following:

  con pair t = t * t
  val pairMonad : monad pair = mkMonad {
    Return = fn [t ::: Type] (a : t) => (a, a),
    Bind = fn [t1 ::: Type] [t2 ::: Type] ((a, a') : pair t1) (b : t1 -> pair t2) => b a
  }

  val fail : pair int =
    return 4

(Yes, that's not actually a monad, but the types work.)  This fails to compile:

  Expression:  return [<UNIF:U338::Type -> Type>] [int] _ 4
    Have con:  <UNIF:U338::Type -> Type> int
    Need con:  int * int
  Incompatible constructors
  Have:  <UNIF:U338::Type -> Type> int
  Need:  int * int

It looks like the compiler is simplifying (pair int) to (int * int), then
failing to unify it with the (M t) pattern to pull out the monad.  Sure enough:

  val fail : pair int =
    @return pairMonad 4

works just fine, since pairMonad provides the monad, and then unifying (t * t)
with (int * int) doesn't cause any trouble.

I can see why this could be tricky, and in general possibly ambiguous.  (E.g.,
if there's a second monad (con withInt t = t * int), int * int could be either
of them.)  However, I'd expect it to be reasonable to take the given type (pair
int) and use that one.  (How does Haskell handle this?)

Moreover, this (AFAICT) completely breaks the syntactic sugar for monads; I'd
like to be able to write something like
  
  command <- Parse.word;
  args <- Parse.arguments;
  return {Command=command, Args=args}

but the suger doesn't seem to provide any way to annotate the monad, rendering
it uncompilable.

Hopefully the problem is clear; am I missing an obvious solution?  I can't find
anything in the bug tracker about this; I can't imagine I'm the first to run
into it.