## Stream: Coq devs & plugin devs

### Topic: ✔ Legacy unification semantics

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:17):

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.

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:17):

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.
``````

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:18):

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.

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:19):

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))
``````

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:20):

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

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:21):

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

#### Guillaume Melquiond (Apr 27 2023 at 11:24):

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.

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:28):

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

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:28):

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

#### Pierre-Marie Pédrot (Apr 27 2023 at 11:30):

I guess I'll have to dig deeper.

#### Notification Bot (Apr 27 2023 at 11:30):

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

Last updated: Nov 29 2023 at 22:01 UTC