A tentative fix for #4413

[herbelin]

This is a regression wrt v8.4 related to the change of order of resolution of evar-evar unification problems.

One possible "fix" is to give priority to the instantiation of the non pre-existing evar to solve a ?x=?y problem. Note that it happens to incidentally fix also #4095!

Started a coq-contribs test but I feel this kind of "fix" should also be tested on contribs using type inference intensively [Edited afterwards: no failures on contribs here, nor for a simpler version based on trunk+4413-evar-evar-fix2 here].

[herbelin]

Hi, can someone try branch trunk+4413-evar-evar-fix at https://github.com/herbelin/github-coq.git on a type inference intensive development (@JasonGross maybe?)? On all examples I could test, it is strictly better than the evar-evar order of v8.5 and v8.6.

[gares]

I had a look at the problem and the proposed fix. It think the fix is going in the wrong direction. Similarly it was wrong to change the evar/evar solution of unification in 8.5.

The bugreport is about "pose proof t" where t is a term like "f ?x H" where f is a constant, ?x is an implicit argument and H is an existing hypothesis of type "T ?a" and "?a" is in evar that exists before one runs pose proof. ?x is too an evar, generated while interpreting the term. The type of "f" is "forall x, T x -> P" so "f ?x H" is well type as long as ?x and ?a are identified.
The tactic tries, IMHO, to understand if the given term is a complete proof or not. The way it does it, is by checking if evars are still present in the term after type inference is run. Depending how you solve ?x=?a you may end up with a normalized term "f ?a H" or "f ?x H". In one case the tactic says OK because ?x is pre-existing evar. In the other case it says FAIL because ?a is fresh. This is the regression.

This way of doing is too simplistic, and too syntactic. Since ?a is now accessible-via/visible-by ?x (if you take the evars pre-existing and normalize their evar_info you find ?a in there) ?a has not to be considered as a fresh evar. The point being that is ?x was a (shelved) goal also ?a is. It is not a new goal.
Note that the proof engine has proper countermeasures to the goal previously named ?x being renamed ?a (advance IIRC), so the proof structure is not changed by the renaming of ?x in ?a.

This is not a bug in unification but in the way tactic(s?) compute if they generate new goals or not. Having unification making choices based on what is "declared to probably be a new goal unless solved before" is making the algorithm even harder to predict.

[herbelin]

@gares: Thanks a lot for caring about the technicalities of this bug. Your analysis is very precise which is great. I agree that the new evar does not have to be considered as a fresh evar. How to proceed? It seemed to me that advance and the cleared flag were not involved here because the tactic engine is not properly involved, only the unification is. Do you think you can solve the problem in a better way?

If I'm not mistaken, there are a few typos, with ?a and ?x sometimes swapped, but this does not change the essence of the analysis.

[gares]

I think the fix should be made by a tactical: it saves the original evar map, runs the tactic, tells you the list of new evars (that are new wrt the old evar map and not reachable by the assignments in the new evar map to evars that were open in the old evar map). Once you have such list you decide what to do: fail, succeed, shelve. Note that such list is stable w.r.t. the choice of solution in evar-evar unif problems.

[herbelin]

@gares: If I understand well your proposal, and if I leave aside at the current time the idea of passing via a tactical, what you are suggesting is to change the detection of what is a "derived" evar in the function Pretyping.frozen_and_pending_holes so that any evar reachable by the assignments in the new evar map to evars that were open in the old evar map is considered derived. Am I correct?

What is the price that we are ready to pay with this proposal. For instance, in:

Goal exists A, forall f : A -> nat, True.
eexists ?[A]; intro.
pose (x := fun l : list ?[B] => f l).

do we want to consider ?B unresolved or not (if I understand your criterion, it would consider it resolved, because ?B would be detected as a subevar of ?A which has been instantiated by list ?B)?

This being said, I don't know how to make progresses. Maybe could we continue collecting examples of what we would like to have? What do you think? How would you like yourself to proceed?

Otherwise, about evar-evar unification specifically, I would like to mention one my concerns which is the propagation of evar names. Consider

Goal exists A, forall f : A -> nat, True.
eexists ?[A]; intro.
pose (x := fun l => f l).

which we a priori want it to work. I think that we would like to see is

x := fun l : ?A => f l : ?A -> nat

and not, say ?T, in place of ?A. So that names of original evars are preserved in such situations, I don't see how to address it without operating at the level of the evar-evar resolution problem, i.e. by resolving ?T:=?A rather than ?A:=?T. Do you agree?

BTW, it would be very convenient that PR #248 is integrated to work on such case studies. @maximedenes: would you like and be ready to dedicate time at merging it soon?

[herbelin]

@gares: Did you have the opportunity to think more at this PR? Do you still feel unsatisfied with the criterion and would like to propose something else?

It is unfortunate that the idea I propose did not come at the time of v8.5 but it seems to me to remain the best evar-evar criterion we can propose currently (simple code, simple criterion, less examples failing than at the time of v8.5, no impact on tests).

[gares]

Names of evars, which evar gets assigned and which evar is considered as a new goal are all different matters.

When 2 evars are unified, the one that survives should have as a name the "union" of the two names. A user-given name is higher than a generated one. An evar may also have two names if it is the result of merging two named evars, what is wrong with it?
More in general the discipline of merging "evar metadata" should be put in place for each and every kind of metadata.

My proposal of delegating the job to a tactical was only for deciding if a new goal is created or not, and
the definition I gave should make it stable no matter which evar gets instantiated.

[herbelin]

@gares: what would you then propose concretely? Would you like to propose the tactical you are taking about? Would you like to develop an evar metadata merging discipline?

In any case, your ideas do not seem essentially contradictory with the very simple patch I'm proposing. So, what about already merging this without procrastinating further (*) to get the benefit of it and then you can concentrate on developing your proposal?

(*) A remark which by the way applies to other PRs as well...

[herbelin]

@gares, @maximedenes: on coqdev, @maximedenes said "evar/evar resolution depending on considerations of clients unification seems to be a wrong approach". May I insist and ask what is concretely the right approach for you?

Having to deal with evar/evar unification problem is intrinsic to any unification algorithm and choices have unavoidably to be made. On what considerations do you think choices should be based then?

[mattam82]

From what I understand @gares proposal avoid making user-visible choices of naming and instantiation when we don't actually have to make any, so I'd rather be in favor of pushing that idea too. The less internals of unification we expose to the user the more freedom we get. You seem to both agree on the criterion for deciding what's new and what's not, an issue I've been facing in unifall as well (for apply based on evars). If that's right then I'll take time to design that tactical.

[herbelin]

After a corridor discussion with @mattam82, it seems to me that there is a misunderstanding.

I started from the regression shown by bug #4413 and I arrived to what I consider to be an improvement of the evar-evar heuristic. Improvement because a 7-line criterion is replaced by a simple one-line criterion. Improvement because not relying anymore on the evar source. If I had found this criterion early enough for v8.5, I would clearly have implemented it for v8.5 and it is a pity that I was not clever enough to having found it already for v8.5.

So, even if I started from #4413, the result goes beyond the question of just fixing #4413. And a good sign is also that it e.g. fixes the regression #4095 which has nothing to do with deciding if an evar is new or not after evaluation of a tactic.

So, I think we should really separate the questions:

• How to solve evar-evar problems per se, independently of tactics, and there, I believe that the criterion I'm proposing is a simple and clear one which works in practice.
• How to design a criterion which is independent of how evar-evar problems are solved to decide what is a new evar after application of a tactic? This is what I understand @gares and @mattam82 are interested in. Somehow, this criterion should be robust enough so that if we randomize the way evar-evar problems are solved, this should not affect the result of the decision, and designing such criterion is clearly worth to be done.

[herbelin]

My assumption that the improved one-line evar-evar heuristic (trunk+4413-evar-evar-fix2) is as good as the former one (trunk+4413-evar-evar-fix) failed. There is again an unexpected interaction with classes: When solving an evar-evar problem involving a (recent) resolvable evar and a (recent) non-resolvable evar, compatibility expects (at least in some cases) that we don't drop the resolvable tag.

This actually highlights that at the current time, the situation is not symmetric in evar-evar problems wrt resolvable evars. Here is an example in current trunk:

Class A.
Instance a:A.
Check fun H:?[x]=a :> id A => f_equal (fun x:A => x) H.
(* fun H : a = a => f_equal (fun x : A => x) H *)
Check fun H:?[x]=a :> A => f_equal (fun x:id A => x) H.
(* fun H : ?x = a => f_equal (fun x : id A => x) H *)

@mattam82, @gares: Don't we want to aim a type class resolution which is independent on the order in which evar-evar are resolved?

While I'm at it, @gares, you said: "When 2 evars are unified, the one that survives should have as a name the "union" of the two names". What is your idea to implement this? To attach list of names to evars? Should we make a union for the resolvable tag as well?

[mattam82]

I think for resolvable indeed true should be the top value during merges.

[gares]

What is your idea to implement this? To attach list of names to evars?

yes. more in general the entire "store" should be merged (i.e. it should require each data to come with a union operation or something along these lines).

[herbelin]

@gares: Yes, this looks like a good idea. Would you do it?

[gares]

No, I've no time now.

[mattam82]

I'll do it, after all I'm responsible for resolvable :) I'll work on the improved check for unresolved evars as well, it's badly needed in my unifall branch too.

[herbelin]

@mattam82: resolvable: good! (incidentally, if you have an idea of how long this will postpone the follow-up of this PR, this will help me to organize myself)

Test for unresolved evars: can you roughly sketch how it compares to tclWITHHOLES, if it is not taking too much time of you?

[mattam82]

@herbelin I'm looking into it right now so hopefully I'll have a PR ready soon.

My first impression is that tclWITHHOLES should simply be refined actually, and I think some refactoring might be needed with check_evars_are_solved in pretyping, the two are performing very similar tests (and in this pose proof example, both are performed).

[mattam82]

Hmm, actually in your example it's not the resolvable flag which is at fault, but the fact that in one case the resulting undefined evar has type [A] and in the other [id A], and only the first is recognized by typeclass resolution as a class evar on which resolution can be launched.

[herbelin]

@mattam82: Ah, you mean that the decision to apply search for type classes instances is taken after the decision of solving the evar-evar equation. It is a bit more tricky to fix then.

[herbelin]

@mattam82: Maybe we can then take also the union of types, and an instance be searched if at least one of the types is a class?

[mattam82]

@herbelin yes, it's solved after the evar-evar solution. It's rather unfortunate but the test for an evar type to be a class or not is purely syntactic (no reduction), so we should maybe rely on a more semantic criterion (i.e. a tag on the evar, but that's not stable by instantiation of evars in the conclusion), or allow taking then whnf on the conclusion (but that will be source of incompatibilities and inefficiencies). I'm trying to figure out what to do actually. Looking at the union of types seems a bit too strong to me.

[mattam82]

What we would like eventually is that typeclass resolution is insensitive to the evar-evar solutions, so it should be insensitive to types convertible to a class.

[herbelin]

@mattam82: But a class can evaluate to another class, right? So, how to decide if a type convertible to a class is considered as related to one class or to the other. I vaguely remember that a problem of this kind happens with coercions.

[mattam82]

Indeed, the reduction should be parameterized at least not to unfold classes.

[ppedrot]

This has been waiting for a loooong time. The unifall Arlésienne doesn't seem to get any closer, so I am forcefully closing this PR and let @herbelin reopen it when it finally lands.

[herbelin]

My overall analysis of the unifall Arlésienne is the following:

• it spanned over too many years for @mattam82 still have the energy to carry on; additionally, @mattam82 has more and more various involvements which reduce his implementation time
• the question of how to make the transition for apply and rewrite towards an evarconv-based semantics was not clear
• suspectingly - but I'm not enough in the intimacy of the unifall PRs to evaluate how far - there are a couple of subtle blocking compatibilities issues to address

In my perception, one way to solve all three problems is first to get a large enough support on the following question: Are we ready, collectively, to make unifall and the question of unification algorithms a priority, meaning, are we ready to target and concentrate our force towards a unification model we are proud of, and to propose a transition model for those tactics impacted by moving to this new unification model (an option, an updating tool, ...)? Are we ready to share with @mattam82 the effort of completing the unifall program (as some of us already did)?

In any case, we definitely cannot accept the current "technical debt" of w_unify, knowing how better we can do. Something has to be done.

[Zimmi48]

Are we ready, collectively, to make unifall and the question of unification algorithms a priority, meaning, are we ready to target and concentrate our force towards a unification model we are proud of, and to propose a transition model for those tactics impacted by moving to this new unification model (an option, an updating tool, ...)? Are we ready to share with @mattam82 the effort of completing the unifall program (as some of us already did)?

I think we are clearly not ready, and this is what the last years have shown, and I don't think anything has changed about that. It seems that unless someone takes a strong leadership (like @ppedrot in the case of Ltac2, or @ejgallego in the Dune case) and is strongly supported by a few others which manage to take time to help (e.g. @maximedenes who integrated Ltac2 or myself who helped merge the Dune PRs), collective efforts are bound to fail. Diluted responsibility usually does not work.

[herbelin]

I'd like to see unification improved and unifall integrated. My time is short but we are many people in the team. Do you mean that we would not be able to organise ourselves to complete the effort (assuming that the importance of unifall is shared of course)? We managed to organise ourselves in moving the manual to sphinx, for instance. I don't think that collective efforts mean dilution of responsibility. We can take collective decisions about what to do and decide at the same time that someone is responsible for these decisions being brought to an end, no?

[Zimmi48]

We managed to organise ourselves in moving the manual to sphinx, for instance.

The way that was done was pretty catastrophic. Don't get me started on that... I spent lots of time fixing the mess.

I don't think that collective efforts mean dilution of responsibility. We can take collective decisions about what to do and decide at the same time that someone is responsible for these decisions being brought to an end, no?

Absolutely. As long as there is someone shepherding the work (and shepherding by itself is a lot of work), collective efforts can succeed. I just meant collective works don't happen by pure magic.