Stream: Coq users

Topic: Tactic-unification bug - 1.5m constraints for 3 evars


view this post on Zulip Lef Ioannidis (Dec 20 2023 at 19:02):

I posted a few weeks ago about an issue with tactic-unification, unfortunately I still have not been able to figure out the cause.

The way it materializes has convinced me this is a Coq bug, as the same three evars generate over 1.5m unification constraints measured by
Set Debug "unification,tactic-unification"

Here's the setup, I have a
Definition comp (E: Type) {HE: Foo E} (X: Type) and two equivalence relations, where L is a relation on E and R is a relation on X

ss L R: comp E X -> comp E X -> Prop
equ R: comp E X -> comp E X-> Prop

Then in a proof

H: equ eq b a
=====================
equ eq a b

I use the symmetry tactic and over 1.5m lines of output are generated by tactic-unification and it never terminates but I was able to copy a few lines of output. If I disable logging, it resolves in 10'.

If I use the deprecated filter unification this resolves in a few seconds with only 26 lines of tactic-unification output.

Set Typeclasses Filtered Unification.
symmetry.
Unset Typeclasses Filtered Unification.

I have attached the logs, Unification.txt is filtered unification, Unification_bad.txt is what is generated after running symmetry.

Note: By looking at Unification_bad.txt we see the same evars ?M3784, ?M3785, ?M3786 repeating over and over again. Even when those get matched

Debug: [tactic-unification] comp ?M3784 ?M3786 ~= comp E X
Debug: [tactic-unification] comp ~= comp
Debug: [tactic-unification] ?M3784 ~= E
Debug: [tactic-unification] ?M3785 ~= HE
Debug: [tactic-unification] ?M3786 ~= X
Debug: [tactic-unification] Prop ~= Prop

They repeat again. I know nothing about Coq's internal mechanism but are partially matched unification constraints cached? What could be causing this explosion? Logs attached.

Unification.txt
Unification_bad.txt

view this post on Zulip Lef Ioannidis (Dec 20 2023 at 19:07):

If the logs are not useful to figure out the issue I will try to construct a minimum reproducible example, it is a bit difficult because many definitions are required but if this is indeed a bug it might be worth it.

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 22:15):

Symmetry uses typeclass search to find proof that equ is symmetric.

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 22:16):

So if you want to look at logs, you should enable TC logs — and probably disable unification logs.

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 22:20):

TC search does not have caching, and it definitely can loop

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 22:22):

and when it loops, it usually means you ended up with a looping TC problem, often because of some bad TC instance

view this post on Zulip Lef Ioannidis (Dec 20 2023 at 22:53):

I already eliminated TC resolution as the source of the problem, using Typeclasses eauto := debug.

Only a few instances are checked and each takes 2-3’ to discharge. Probably because the unification log (Unification_bad.txt) shows over 1.5 million constraints attempted.

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 23:29):

In this case, the appropriate fix might be to make some definitions typeclass opaque.

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 23:29):

But it seems the first step would be turning the TC search problem into a problem applying one of the instances.

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 23:30):

A relevant trick is that the TC log lies: it claims it uses simple (e)apply, but the code it runs is much closer to (IIRC) uses of class_apply

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 23:38):

For instance, the log mentions

fun t u : comp ?M3784 ?M3786 =>
                     lattice.body (ss ?M3787) x t u /\ lattice.body (ss (flip ?M3787)) (flip x) u t ~=
fun t1 t2 : comp E X => equF eq x (observe t1) (observe t2)

so, it sounds like the equ relation in your goal is being unfolded by TC search, unnecessarily.

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 23:39):

Such unfolding is convenient for completeness but bad for performance, so you probably want something like Typeclasses Opaque equ. Any necessary instance that was proven automatically must now be proven explicitly

view this post on Zulip Paolo Giarrusso (Dec 20 2023 at 23:45):

for instance, you probably want to export that equ is an equivalence relation — Reflexive, Symmetric and Transitive — then sth like the following should work.

Section foo.
  Context {E: Type} {HE: Foo E} {X: Type} (R : relation X).
  Definition equ : relation (comp E X) := ...
  #[export] Instance : Reflexive equ := _. (* works *)
  #[export] Instance : Symmetric equ.
  Proof.
  (* you can try [apply _.], your snippet suggests automatic search diverges, so you might need a different proof *)
  Qed.
  #[export] Instance : Transitive equ := _.
  #[global] Typeclasses Opaque equ.
End foo.

in this case, we can collapse the 3 instances to:

  #[export] Instance : Equivalence equ.
  Proof. split; apply _. Qed.
  #[global] Typeclasses Opaque equ.

view this post on Zulip Paolo Giarrusso (Dec 21 2023 at 00:13):

I should say, it is not impossible there is a bug, but ultimately if nothing is marked opaque, unification will do some approximation of "normalize lemma to be applied and goal and try to unify them", and there's no reason to expect this to be feasible.


Last updated: Jun 23 2024 at 05:02 UTC