Jacques Garrigue

@diml This shouldn't help for `x |> f`, as this patch only propagates information from the expected type of a function's result to its arguments, i.e. not between arguments.

My position has not much changed. I am not opposed to this change if it helps Merlin in particular, but we have to be careful about principality. So this would...

@lpw25 Actually, here the problem is with defaulting rather than propagation. Defaulting comes from the previous behavior for record disambiguation, but it clearly goes against monotonicity. My point was just...

To clarify, the problem is not so much about backward propagation _through_ application as about the fact propagating from a function to its argument, using just the type of the...

BTW, T6 is mentioned in the header of `separation_axioms.v`, but there does not seem to be a definition for it.

The code here is a transcription of the explanation in https://www.math.nagoya-u.ac.jp/~garrigue/papers/injectivity2.pdf, particularly the last paragraph of section 2. Namely, since injectivity annotations are on type parameters, in presence of constraints...

This is potentially a semantical change (the semantics of optional arguments depends on where the parenthesis are), so we should be very careful. If the semantics is unchanged, and this...

I only have a small concern with this approach: is the meaning exactly the same ? Intuitively yes, and looking at the code code in typemod, addition of constraint is...

The problem with the alternative approach is that `contains_gadt` is too coarse. In particular, just using the GADT-like syntax without actually introducing equations already makes `contains_gadt` true. For this reason,...

> The specification of the type given to `x` in `p as x` is that it is the most general type that can be given to `p` **such that the...