I know this is a trap question, but do we have any idea about the expected semantics for the Unification functions? I was naively expecting that if w_unify succeeds on t ~ u where t is meta-free, then after that t would be *convertible* to u. But there are actually not so complicated instances where this is just not true.

I came up with a simple example arising from the stdlib:

```
Definition relation (A : Type) := A -> A -> Prop.
Axiom Reflexive : forall {A : Type}, relation A -> Prop.
Axiom Equivalence : forall {A : Type}, relation A -> Prop.
Definition equiv {A} (R : relation A) (_ : Equivalence R) : relation A := R.
Axiom equiv_reflexive : forall (A : Type) (R : relation A) (sa : @Equivalence A R), @Reflexive A (@equiv A R sa).
Lemma respecting_equiv A B (R : relation B) :
Reflexive (fun (f g : A -> B) => forall (x : A), R (f x) (g x)).
Proof.
apply equiv_reflexive.
```

apply internally tries to unify the goal with the type of its argument, but even after unification some metas remain unsolved, due to non-empty rel contexts.

More precisely on the problem

```
(Reflexive (forall _ : A, B) (fun f g : forall _ : A, B => forall x : A, R (f x) (g x)))
~
(Reflexive ?M150 (equiv ?M150 ?M151 ?M152))
```

the unification produces the result

```
(Reflexive (forall _ : A, B) (equiv (forall _ : A, B) (fun f g : forall _ : A, B => forall x : A, R (f x) (g x)) ?M152))
```

note the uninstantiated meta ?M152 at the end corresponding to the sa argument of equiv_reflexive

my question / complaint: is it somewhat expected and if yes is there really no hope about legacy unification?

I don't understand what the issue is. There is nothing to unify `?M152`

with, is there? So, it seems expected that it is still there at the end.

Oh, you're right, I misunderstood the example. Actually unification performs arbitrary δ-unfolding so M152 just disappears.

But to give a bit more context, this shifts the burden on the Clenv algorithm for dependency computation.

I guess I'll have to dig deeper.

Pierre-Marie Pédrot has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC