Coq fails to unify two terms with a unification variable appearing in both of them, even when simplifying the terms would make one of them disappears. This happens only when the simplification step is under an opaque constant, for instance :

```
From elpi Require Import elpi.
Inductive C (T : Type) := Build_C.
Elpi Command bla.
Elpi Query lp:{{
coq.unify-eq X {{ Build_C (fst (lp:X, lp:Y)) }} Z.
}}.
```

With `id`

instead of `Build_C`

, unification succeeds. Is there a way to have this reduction happen, or otherwise to make this unification problem solvable ?

with Id it succeeds because the two sides are exactly X, while if there is a rigid symbol you get an occur check.

Right, I should have written `snd`

instead of `fst`

, `Build_C (snd (lp:X, lp:Y))`

simplifies to `Build_C lp:Y`

, in which `lp:X`

does not appear, but the unification still fails.

Afaik only agda normalizes a term to minimize the variables it contains. IMO it is too expensive in general.

A message was moved here from #Coq devs & plugin devs > 8.19 by Enrico Tassi.

So I suggest you explain how you ended up there

(Agda normalization is also closer to Coq simpl or Equations's simp, so its cost is very different)

Last updated: Oct 13 2024 at 01:02 UTC