Bad type inference when using subtyping with monads

[TWal]

The problem is described in the comments of the following code:

// Two monads, with returns and binds
assume val m1: Type0 -> Type0
assume val m2: Type0 -> Type0

assume val return1: #a:Type0 -> a -> m1 a
assume val return2: #a:Type0 -> a -> m2 a

assume val (let?): #a:Type0 -> #b:Type0 -> m2 a -> (a -> m2 b) -> m2 b
assume val (let*?): #a:Type0 -> #b:Type0 -> m1 (m2 a) -> (a -> m1 (m2 b)) -> m1 (m2 b)

// Suppose we have a monadic function that returns a `nat`
// (a refined type, namely a subtype of `int`)
assume val f: unit -> m2 nat

// And we want to lift it in a double monadic function that returns an `int`
val g: unit -> m1 (m2 int)

// The naive lifting with `return1` fails as expected:
// return1 (f ()) has type m1 (m2 nat),
// which cannot be converted to m1 (m2 int),
// (well-known problem of sub-typing under an inductive)
[@@ expect_failure]
let g () =
  return1 (f ())

// The standard fix with inductive subtyping is to unwrap and re-wrap,
// but this fails:
[@@ expect_failure]
let g () =
  // We would hope that x here has type `nat`
  let*? x = return1 (f ()) in
  // we can do the subtyping on x, and return x as an int
  return1 (return2 x)

// It doesn't work, because the last line implies that `x` must have type `int`,
// therefore `return1` is used with `a = m2 int`,
// which doesn't work becuase `f` returns an `m2 nat`

// We now explicit the implicits of `return1`, but it still fails:
[@@ expect_failure]
let g () =
  // We would hope that x here has type `nat`
  let*? x = return1 #(m2 nat) (f ()) in
  // we can do the subtyping on x, and return x as an int
  return1 (return2 x)

// It still fails, because `x` has type `nat`, so obviously `return1 (return2 x)` has type `m1 (m2 nat)`!
// Adding a coercion finally fixes things
let g () =
  // We would hope that x here has type `nat`
  let*? x = return1 #(m2 nat) (f ()) in
  // we can do the subtyping on x, and return x as an int
  return1 (return2 (x <: int))

// If we are not lucky to have a type abbreviation like `nat`,
// but an explicit refinement, the workaround looks like this:
val g': unit -> m1 (m2 int)
let g' () =
  //                      vvvvvvvv (ugh)
  let*? x = return1 #(m2 (_:int{_})) (f ()) in
  return1 (return2 (x <: int))

// One other workaround, with an utility function

val unrefine:
  #a:Type0 -> #p:(a -> Type0) ->
  x:a{p x} ->
  a
let unrefine #a #p x = x

val g'': unit -> m1 (m2 int)
let g'' () =
  let*? x = return1 (f ()) in
  return1 (return2 (unrefine x))

I feel like it would be reasonable to expect that the second attempt at defining g (un-wrapping and re-wrapping the inductive) should work, why isn't it the case?

In the line let*? x = return1 (f ()) in, the implicit must be resolved as nat because anything else would lead to a type error, and in the line return1 (return2 x) the implicit must be resolved as int for the same reason, I don't get why the type inference take other decisions.