Leo White

> My impression is that we want to propagate the type inside a function definition, and also from a function to its argument (not so clear here, but needed for...

> I do not see strong motivation Consistency is important. If we are doing it for `match` then we should do it for `if` and `try` as they are just...

It would be good to include this fix: https://github.com/ocaml-flambda/flambda-backend/pull/4102

I've reviewed this patch and I believe it is correct. However, this is a complicated part of the type-checker and I think that @garrigue ought to review it before we...

> using propagation of the result type to disambiguate constructor overloading would be bad, because this is clearly not principal. @garrigue Could you explain why or give an example that...

I'm fine with just doing this in non-principal mode. I don't really see how the example of non-monotonicity is made worse by propagating through applications though. The following already type-checks...

> In the example of Jacques, let k x y = x has an inferred type, but inferring a less general type would change the disambiguation behavior if that PR...

`j`'s type is getting generalized, including all the structure in it, so that we consider the fact that `j`'s first argument is a `t1` to be "known principally". This is...

Oh, I didn't notice your output had `int -> int -> t1`. I'm pretty sure it should be `int -> bool -> t1`. I suspect the order of the type-definitions...

I intend to get to this this month