Attempted minimal example of unification failure problem

parse.ur

datatype result a = Success of a*string | Failure
type t a = string -> result a

fun mreturn [a] (x:a) : t a = fn s => Success (x, s)
fun mbind [a] [b] (p: t a) (f: a -> t b) : t b =
 fn s => case p s of
             Failure => Failure
           | Success (x, s') => f x s'
val monad_parse : monad t = mkMonad {Bind=@@mbind, Return=@@mreturn}

fun string t : t string =
 fn s =>
    let val l = strlen t in
        if strlen s = l && substring s 0 l = t then
            Success (t, strsuffix s (strlen t))
        else
            Failure
    end

fun string' s : t unit =
    fn u =>
       case string s u of
           Failure => Failure
         | Success (_,s') => Success ((),s')

fun string' s =
    mbind (string s) (fn _ => mreturn ())

fun string' s =
    @@bind [t] [string] [unit] monad_parse (string s) (fn _ => @@return [t] [unit] monad_parse ())

(* Uncommenting the following fails with this error:
/home/julian/src/experiments/parse-example/parse.ur:34:9: (to 34:17) Unification failure
Expression:  string s
  Have con:  string -> result string
  Need con:  <UNIF:U83::Type -> Type> <UNIF:U84::Type>
Incompatible constructors
Have:  string -> result string
Need:  <UNIF:U83::Type -> Type> <UNIF:U84::Type>
/home/julian/src/experiments/parse-example/parse.ur:33:12: (to 33:13) Unification failure
Expression:
fn s : string =>
 Basis.bind [<UNIF:U83::Type -> Type>] [<UNIF:U84::Type>] [{}] _
  (string s)
  (fn $x : <UNIF:U84::Type> =>
    case $x of _ => return [<UNIF:U83::Type -> Type>] [{}] _ {})
  Have con:  string -> <UNIF:U83::Type -> Type> {}
  Need con:  string -> string -> result {}
Incompatible constructors
Have:  <UNIF:U83::Type -> Type> {}
Need:  string -> result {}
 *)
(*
 * fun string' s : (t unit) =
 *     _ <- string s; return ()
 *)