Fix 9663 (Miller pattern unification fails on evars)

[gares]

In particular evar_eqappr_x tries to find a Miller pattern on both sides,
while the fast path for evars tries solve_simple_eqn in one direction
only. So if you have (Evar-not-Miller = Evar-Miller) the code was not
trying to solve the RHS.

Depends on: #7819 (to avoid conflicts)

[gares]

@mattam82 you are fresh on this code, please tell me if my fix is too aggressive.

In particular I start to doubt that the fast path for simple_eqn is just making things more buggy.
As this patch proves, it is less powerful than the code that follows, but does not always backtrack.
So, even if it is faster, it looks like a "random" optimization to me.

[ejgallego]

Would you mind submitting depending PRs as Drafts in the future?

[ggonthier]

This PR does fix the evar-to-Miller issue, but perhaps a related Miller-to-Miller problem should be also be addressed, e.g.:

Definition id_depfn21 {T A R} f := f : forall x y : T, A x -> R.
Definition id_depfn22 {T A R} f := f : forall x y : T, A y -> R.
Fail Definition idn2 f : nat -> nat -> nat := id_depfn21 (id_depfn22 f).

In general, all NotClean errors should check whether the offending occurrences of variables occur only in evar contexts or in arguments of applied evars, as in such cases they can be unambiguously resolved by filtering the evars or assigning them K-terms, respectively.

[ggonthier]

The comment on the following line need to be modified.

[gares]

I think the second bug is morally from the same source, but this time is in imitate from solve_simple_eqn
The original sin is that App(Evar(k,a),b) is not systematically turned into Evar(k',a ++ b) where ?k := fun b => ?k[a,b]). It seem the code for pruning an applied evar in solve_simple_eq understands only the latter form.
Unfortunately the fix is not so trivial, so I'm not going to do it in this PR (not sure I'm going to do it, this code is really bad).

This PR is still OK I think, I'll rebase and fix the comment (I can't make sense of it even for the existing case, ideas?).

[gares]

@mattam82 can you take and review this one?

[gares]

I'd like this to get in 8.10 since math-comp/math-comp#294 needs it and math-comp tries to be compatible with 2 versions of Coq. So if it misses 8.10 we won't even be able to merge the other PR in 6 months...

[mattam82]

Right, it's on my TODO for next week.

[mattam82]

The comment was meant as a reminder that ?X = {| foo := ?X.(foo) |} can fail due to occur-check, while eta-expansion can solve it. IIUC, NotClean can also be raised, while pruning more would succeed, I guess the comment should reflect that.

[gares]

I'm rebasing & updating the comment right away

[gares]

done

[mattam82]

Thanks, I'll wait for a last CI just in case and merge.

[mattam82]

Funny enough, this uncovers a bug in equations, unification is stronger which leads it to produce an ill-typed proof term. I'm working on a fix and will report here.

[mattam82]

@gares I made the fix to equations, basically now a constraint is postponed when it was failing before, I just switched to the new unify which doesn't allow delaying. Interestingly, it is postponed exactly for the (bad) reason that you mentioned of not handling applied evars correctly. But that can be fixed at a later stage indeed. Now the CI is all green :)