#12061 fix: avoid adding inconsistent equations in functor error messages

[Octachron]

This PR fixes by #12061 by making sure that the diffing algorithm for functor errors doesn't add inconsistent equations to the typing environment when exploring potential patches.

More precisely, this PR ensures that whenever the type of the concrete functor argument and the type of the abstract parameter disagree, we don't add any equations between the two.

It might be possible to be more finer-grained and keep consistent equations but that's probably better done at a later point. Note that the second commit in this PR removes a test which is no longer relevant without such addition of consistent equations.

Along the way, this PR fixes a small fixes when the diffing algorithm was not adding enough equations when inserting a missing argument.

Fix #12061

[gasche]

I tried to jump at the diff and read the code, but I need more context to understand what is going on, and I am too lazy to look it up myself so let's just ask here.

1. What is the specification of update again? My guess is that it takes a "diff", that is a move inside the edit matrix (it is a move from a pair of states to compare (S1, S2) to a "larger" pair (S1', S2'))), and it has to update some "state" that made sense in (S1, S2) and now has to make sense in (S1', S2').

2. In the case of functors, the state contains a typing environment. What is the assumption on the relation between the typing environment and the pair of (S1, S2)? (How do we call S1,S2 if not "states"? positions?) My vague guess is that, depending on the move, it tries to maintain an environment that makes sense for both S1 and S2, and sometimes it gives up. From your PR description it sounds like you are moving more cases to the "give up" category, but in trying to match this intuition to the patch I... gave up.

3. What does expand_params do? Eyeballing its implementation, and also lookup_expansion, did not answer this question immediately. Are they documented somewhere?

[Octachron]

1. The update function computes the new state (here the environment and substitutions) at the tip of the current patch after a move in the edit matrix.
   There are no pair of equivalent states, we have

   • a common environment to add abstract functor parameters that are bound only inside the functor
   • a substitution that represent equations between the expected and actual argument

2. We need to add an equation between the two sides whenever they are compatible, in other words in the Keep case. Previously, the update function was adding the same equation even in the Change case when we know that there are some incompatibilities. That might lead to better errors in some case because the incompatibilities might be harmless for the diffing algorithm (e.g. one value with incompatible type). But in general, this breaks some invariant in the typechecker. For instance Invalid_argument("List.iter2") under moregen with ill-aritied type in functor argument #12061 is due to the fact that the current code is breaking the precondition that the arity of type constructors would be always the same on the two side of the comparison.
   The current patch is thus "giving" up on keeping the possibly consistent equations in the Change case and it is moving the Change case to the Insert _ group that may still need to add the abstract parameter to the typing environment, but doesn't add equations between the argument and the parameter.

3. At the end of the update, we may have discovered equalities that may change the concrete arity of the functor, the expand_params function recompute this concrete arity

[gasche]

There are no pair of equivalent states

I wasn't meaning to suggest that states in a pair are equivalent. I view the edit matrix for the words W1 and W2 as formed of pairs of prefixes of W1 and W2, with (empty, empty) on one end and (W1, W2) on the other end, and any other point is (P1, P2) for two prefixes. I assume, in the case of "functor diffing", words/prefixes are sequences of module applications abstractions. (Sometimes we call "telescopes" such sequences of abstractions.)

we have

• a common environment to add abstract functor parameters that are bound only inside the functor
• a substitution that represent equations between the expected and actual argument

This is too abstract for me and I would need an example (or to think hard about it, but who wants to do that?). Would you introduce some documentation for Functor_inclusion_diff.Defs.state, with an example?

[Octachron]

Would you introduce some documentation for Functor_inclusion_diff.Defs.state,

This would not be the right place for such documentation, since your questions concern the typing of functor applications or functor inclusion in general and are not related to the diffing algorithm.

[Octachron]

I added some more comments (and one fix for an error detected while writing the comments). More generally, the higher level specification of update in function of the move in the edit matrix is that:

• Keep update the typing environment as usual (it is the only case which updates the set of equalities between modules).

• Delete and Insert add their consumed module to the environment if it was an abstract parameter (always for Insert, and while typing functor inclusion in the Delete case). This is useful because those abstract modules may contain equations between exterior component:

Consider for instance:

module _: sig
    module F: functor (X: sig type 'a t = 'a * 'a end)(Y: sig type 'a t = 'a X.t * 'a list end) -> sig end
end = struct
    module F(X: sig type 'a s = 'a list end)(Y: sig type 'a t = ('a * 'a) * 'a X.s end) = struct end
end

The second parameters ought to be considered as matching because they both extend to

sig type 'a t = ('a * 'a) * 'a list

however this equality rely on the type abbreviations defined in the diverging first arguments X.

• Change is Delete + Insert.

[gasche]

I looked at the Functor_inclusion_diff part (not the Function_app_diff part), it looks okay. The new comments are really helpful for me to make sense of what is going on.

[gasche]

(looking just at the new commit)

[gasche]

Nit: I would have env before subst in the parameter list, because subst lives "over" env (its well-formedness depends on the value of env).

[Octachron]

I would rather keep the same order as the one in the non-error path.

[gasche]

Question: in the error code there was a nice symmetry between the None, Some and the Some, None case, this is not the case here -- there is a rename in one case and not in the other. Why the difference?

[Octachron]

This is a bugfix from #10693 to avoid potential identifier collisions in the non-error path.

[gasche]

Approved, with minor nitpicks to be taken into account or not depending on the author's whims.

[gasche]

I reviewed this part with @Octachron's help and I agree that it does what it says it does.

[gasche]

The nice refactoring has the slight downside of having heterogeneous abstraction levels across the different cases here, a minor issue which could be solved by moving the Subst+Env logic to their own auxiliary functions as well.

[Octachron]

I have added a small auxiliary function for binding abstractions in the environment.

[gasche]

I am happy with the new state of the code, and the extra documentation. Approved.

[Octachron]

Since this is a localized bug fix, I am thinking of cherry-picking it to 4.14 . Any objections?

[gasche]

Sounds fine to me.