Impossible: ill-typed application on inference

[mtzguido]

Getting an inference blowup with the following code:

module A

assume val m : Type -> Type
assume val return_m : #a:Type -> a -> m a
assume val bind_m : #a:Type -> #b:Type -> m a -> (a -> m b) -> m b
assume val push_m : #a:Type -> #b:(a -> Type) -> (x:a -> m (b x)) -> m (x:a -> b x)

val push_sum : #a:Type -> #b:(a -> Type) ->
                  dtuple2 a (fun (x:a) -> m (b x)) -> m (dtuple2 a b)
let push_sum (#a:Type) (#b:(a -> Type)) (p : (dtuple2 a (fun (x:a) -> m (b x)))) =
    match p with
    | Mkdtuple2 x y ->
        bind_m #(b x) (* #(dtuple2 a b) *) y (fun (y' : b x) ->
        return_m (* #(dtuple2 a b) *) (Mkdtuple2 x y'))

Running F* gives:

Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Impossible: ill-typed application ?26724 : Type
	a:Type ->
b:(uu___151587:a -> Prims.Tot Type) -> p:x:a & A.m (b x) -> x:a -> y:A.m (b x) -> Prims.Tot Type

The example is a bit complex, but I couldn't really minimize it any more. Uncommenting any of the two #(dtuple2 a b) annotations makes the file succeed.

I think inference should succeed here, but even if not, this is a blowup and should be a proper error

[mtzguido]

This doesn't blow up anymore, but fails due to #1091 at encoding time (so --lax works OK). Closing this one and commenting there.