Am I correct that Coq if Coq tries to unify `f x y`

with `f x' y'`

, and `y`

cannot be unified with `y'`

, then it gives up, rather than seeing if unifying `x`

with `x'`

resolves some evars in `y`

or `y'`

which would allow unification to succeed? (Why is it this way?)

old unification or evarconv?

I think evarconv is left to right, for instance

```
Universes u1 u2 v1 v2.
Constraint u1 < v1.
Constraint u2 < v2.
Axiom P : Type -> Type -> Prop -> Prop.
Axiom p : forall T (* needed to avoiding calling unification on evar free application *), P Type@{u1} Type@{u2} T.
Goal P Type@{v1} Type@{v2} True.
refine (p _).
```

reports universe inconsistency about `u1 = v1`

ie the first argument

old unification also seems left to right, but it doesn't substitute the metas while unifying

and may treat defined evars in strange way, see use of EConstr.Unsafe in unification.ml

I think I saw an old comment or commit message which claimed that this was deliberate for performance but I don't remember details

Which one is used by `typeclasses eauto`

and reported with `Set Debug "tactic-unification".`

?

old

Last updated: Dec 05 2023 at 12:01 UTC