Jacques Garrigue

Indeed, this is mostly a problem of motivation. I had a look at the code last week. The natural place to call the recomputation would be in `env.ml`, but then...

Cannot reproduce either. I am using gmake 4.4.1 on macos-arm64, but there is a `sourceView2Enums.ml` after compilation.

I suppose that you are talking of `n >= n2` at line 2217. Here the order does not matter as long as it is total, so I suppose that your...

This is a big change in terms of modified outputs, but I agree this looks nicer. The `functor` keyword does not seem to bring any useful information here.

I am probably not going to be able to look at this PR in detail for a few weeks. Two remarks. > There are existing ways to work around this...

I had a (quick) look at the code, and I did not find anything untoward. My only concern with respect to principality is how to properly define upward propagation through...

> I think I'd probably want to include a few more things that this -- although perhaps you were already including some of these implicitly -- for instance: I would...

OK, I'll try to look into this. But this requires a change in approach, since the current code is just taking advantage that we now that those existentials, which I...

The way type information is propagated to arguments has a direct impact on principality. So this needs to be checked carefully. I will look at that when I have time...

Answering Alain's comment, using propagation of the result type to disambiguate constructor overloading would be bad, because this is clearly not principal. Currently, this patch does not generalize the type...