I am looking for debugging help on a unification issue that pops up 40 minutes into a non-open source proof. Luckily, the problem is pretty easy to explain: I have a goal of the form `bi_entails P ?Q`

and solve it using `refine (bi_entails_refl P)`

. Those are iris definitions but you can substitute with `eq P ?Q`

and `eq_refl P`

. After that call to `refine`

, the contents of `?Q`

are *almost* `P`

except that a few terms have been changed. In my specific example, `P`

is a huge term that contains the subterm `(0 < nb)%N`

under a few binders (one of which is `nb`

). In `?Q`

that subterm has been changed to `(?GoalX < nb)%N`

where `?GoalX`

(X is some number) is a new evar. I am extremely confused by this. The reason I think that this is a unification bug is that Requiring unicoq and using `Set Use Unicoq`

fixes the problem (i.e. `?Q`

is instantiated exactly with `P`

). My suspicion is that the value `0`

in `0 < nb`

was originally an evar that got instantiated with `0`

and somehow that evar got messed up during unification. Does anyone have any ideas about this? I'd love to report this as a bug with a reproducible example.

This is way obvious but did you try adding prints at a few key points of the unifier and inspect the output? Since you know which terms get messed up, it should be possible to search this in the logs. Also you might be ok to share at least parts of this log. I don't see much of an alternative for debugging code that runs 40 minutes until it gets to the spot.

Is the issue that you don't know what to print where?

I have debug output before and after `refine`

. I know the exact value of `P`

and I know the exact value(s) of `?Q`

. I can see the output of `Set Debug Unification`

(which print the correct unification problem for `P ~ ?Q`

). I think I have all the data.. I just don't know why this particular call to `refine`

produces new evars and puts them into the `?Q`

. I am slowly reproducing the exact circumstances in which `refine`

gets called so that I can find out what parts of the goal are necessary for the bug to trigger.

I managed to rephrase things in terms of `eq`

. Here's the proof script..

```
ltac2:(lazy_match! goal with
| [ |- ?p = ?q ] =>
let prf := constr:(@eq_refl _ $p) in
Message.print (Message.of_string "DIFF");
Message.print (Message.of_constr q);
Message.print (Message.of_constr p);
refine prf;
Message.print (Message.of_constr q);
()
end).
```

.. and the output: (my `?Q`

, or `?q`

in the ltac2 code above, is called `?F`

)

```
DIFF
?F@{x45:=0%N; p'1:=nullptr}
(my_term 0)
(my_term ?Goal3@{x45:=0; p'1:=nullptr})
```

And here with `Set Printing All`

to avoid any scope confusion around numeric literals:

```
DIFF
?F@{x45:=N0; p'1:=nullptr}
(my_term N0)
(my_term ?Goal3@{x45:=N0; p'1:=nullptr})
```

Okay, this is enough nightmare material for me. I'll go to bed...

there's probably a delayed constraint `?Goal3@{x45:=N0; p'1:=nullptr} == N0`

(which can be solved by both Goal3 = N0 and Goal3 = x45)

maybe solve_constraints after the refine helps

Thanks a lot! `solve_contraints`

does indeed help! Judging by the documentation of `Solve Unification Constraints`

it seems like one of our custom tactic isn't maintaining the no-remaining-constraints invariant. I wonder if makes sense to invest time into figuring out exactly which tactic leaves unsolved constraints or if I should just stick `solve_constraints`

at the end of all our tactics.

Hm, maybe it is not so clear cut after all. The *only* place where `progress solve_constraints`

works is right after the call to `refine`

. Is this a bug in `refine`

itself?

Oh.. this only comes up in Ltac2's `refine`

. So it's not really a unification problem. I suspect Unicoq simply doesn't delay the constraint. But evarconv does delay it and Ltac2 does not honor `Solve Unification Constraints`

. @Pierre-Marie Pédrot is this on purpose?

ltac2 should respect the option, it goes through the same Proof.solve as ltac1 which is where that's handled

Maybe it's the ltac1/ltac2 boundary that enforces it in this case. I'll write the whole snippet in ltac1 to find out which one out of `exact`

/`refine`

/`exact:`

does the right thing.

note that Solve Unification Constraints basically replaces `tac.`

by `tac;solve_constraint.`

ie it's sentence based

it has nothing to do with atoms like refine/exact/etc

Ah!

looking at the doc that's not very clear

But.. hm. That makes the whole thing even more puzzling. I can definitely get these unresolved evars to show up after a sentence.

(Not in my tiny reproduction of the problem but in the original example.)

I might have reproduced the wrong thing..

Or can I? I need to try this again.

I cannot. I only observed the unresolved constraints by printing after `refine`

. Well, I guess none of this was actually a problem then.

I just got one step closer to figuring out at a problem that's actually real: Using Ltac2's `refine`

(like in my minimal proof script) I get new a subgoal that corresponds to the already-defined evar. I can solve that subgoal with any value of `N`

I like. For example, `refine prf > [refine '99%N]`

works just fine and it seems `99%N`

disappears into a black hole. I cannot find any trace of it in any term afterwards. Ltac1's `refine`

doesn't leave such a subgoal. Also, the subgoal disappears at the end of the sentence (probably because the contraints are being solved).

if you unset the option does it still disappear?

Just tried that and the goal is returned, i.e. it no longer disappears

And I can get the corresponding(does it correspond?) evar to show up in the other goal.. that's pretty much to be expected, I guess.

Ha, what's even better is that this apparently loses the constraint and I can now solve the goal with `99%N`

and the value shows up in the other goal.

(I imagine that in the other scenario where I solve the goal with `99%N`

before the end of the sentence the value is ignored because it violates the constraint?)

I wish I could push this all the way to `Qed`

to see what explodes but I don't have 20+40 minutes for getting there and returning to the current position in the proof :(

```
Goal True.
let g := open_constr:((fun x => _) 0 = 0) in
assert g.
Unset Solve Unification Constraints.
refine eq_refl.
exact 1.
constructor.
Qed. (* Error: The term "eq_refl" has type "1 = 1" while it is expected to have type "1 = 0". *)
```

Is this a bug? What's the spec of unsetting the unification constraints solver?

I believe it's a bug; I'll report it

https://github.com/coq/coq/issues/13893

Note that `reflexivity`

correctly leaves the constraint behind, while `refine`

does not

Hm, reflexivity uses tactic unification..

So maybe this is an evarconv bug after all? I don't know what to think anymore :D

Last updated: Dec 05 2023 at 12:01 UTC