coqc infinite loop in type class resolution

[larsr]

Description of the problem

Compiling this program makes coqc go into an infinite loop.

Note that there is a "bug" in the program because I commented out `(Equivalence F).

This will make coqc search forever for which Equivalence instance it should
use in foo.

Require Import Setoid.
Require Import RelationClasses. (* for Equivalence  *)

Definition equ {T} {e} `(Equivalence T e) := e.
Notation "f == g" := (equ _ f g)  (at level 80).

Class Op (A:Type) := op : A -> A -> A.

Class C F  `(Op F) (* `(Equivalence F) *) :=
{
    foo : forall a b , op a b == op a b;
}.

Coq Version

I installed v8.15.1 with nix.

[nix-shell]$ coqc --version
The Coq Proof Assistant, version 8.15.1
compiled with OCaml 4.12.1

I also tried 8.14.1 and 8.13.1 with the same result.
And I just (July 16, 2022) tried it with master, i.e. 8.17+alpha 672b144 , and it still has the same problem.

[larsr]

Maybe useful to know: collacoq gets "Stack overflow."

https://x80.org/collacoq/apakagupok.coq

Also noteworhty: It doesn't happen if Setoid is not imported. Could it be a kind of "loop" in the instance definitions in RelationClasses.v?

[Alizter]

Here is how to debug:

Require Import Setoid.
Require Import Morphisms. (* for Equivalence  *)

Definition equ {T} {e} `(Equivalence T e) := e.
Notation "f == g" := (equ _ f g)  (at level 80).

Class Op (A:Type) := op : A -> A -> A.

Set Typeclasses Debug.
Set Typeclasses Depth 2.

Class C F  `(Op F) (* `(Equivalence F) *) :=
{
    foo : forall a b , op a b == op a b;
}.

We see that

Calling typeclass resolution with flags: depth = 2,unique = false,do_split = true,fail = false
1: looking for (Equivalence ?e) with backtracking
1.1: simple apply @relation_equivalence_equivalence on
(Equivalence ?e), 0 subgoal(s)
2: looking for (Op (relation ?A)) with backtracking
2: no match for (Op (relation ?A)), 1 possibilities
1.2: simple apply @predicate_equivalence_equivalence on
(Equivalence ?e), 0 subgoal(s)
2: looking for (Op (predicate ?l)) with backtracking
2: no match for (Op (predicate ?l)), 0 possibilities
1.3: exact iff_equivalence on
(Equivalence ?e), 0 subgoal(s)
2: looking for (Op Prop) without backtracking
2: no match for (Op Prop), 0 possibilities
1.4: simple apply @Equivalence.pointwise_equivalence on
(Equivalence ?e), 1 subgoal(s)
1.4-1 : (Equivalence ?eqB)
1.4-1: looking for (Equivalence ?eqB) with backtracking
1.4-1.1: simple apply @relation_equivalence_equivalence on
(Equivalence ?eqB), 0 subgoal(s)
2: looking for (Op (?A -> relation ?A0)) with backtracking
2: no match for (Op (?A -> relation ?A0)), 0 possibilities
1.4-1.2: simple apply @predicate_equivalence_equivalence on
(Equivalence ?eqB), 0 subgoal(s)
2: looking for (Op (?A -> predicate ?l)) with backtracking
2: no match for (Op (?A -> predicate ?l)), 0 possibilities
1.4-1.3: exact iff_equivalence on
(Equivalence ?eqB), 0 subgoal(s)
2: looking for (Op (?A -> Prop)) with backtracking
2: no match for (Op (?A -> Prop)), 0 possibilities
1.4-1.4: simple apply @Equivalence.pointwise_equivalence on
(Equivalence ?eqB), 1 subgoal(s)
1.4-1.4-1 : (Equivalence ?eqB)
1.4-1.5: simple apply @eq_equivalence on
(Equivalence ?eqB), 0 subgoal(s)
2: looking for (Op (?A -> ?B)) with backtracking
2: no match for (Op (?A -> ?B)), 0 possibilities
1.5: simple apply @eq_equivalence on
(Equivalence ?e), 0 subgoal(s)
2: looking for (Op ?T) with backtracking
2.1: exact H on (Op ?T), 0 subgoal(s)
3: looking for (Op F) without backtracking
3.1: exact H on (Op F), 0 subgoal(s)
C is defined
foo is defined

We restricted the depth to 2, so we look for instances that keep repeating. It looks like relation_equivalence_equivalence keeps getting used unhindered, which means when there is no depth restriction, this will spiral out of control.

Another way to check this theory is to use breadth first search typeclass search:

Require Import Setoid.
Require Import Morphisms. (* for Equivalence  *)

Definition equ {T} {e} `(Equivalence T e) := e.
Notation "f == g" := (equ _ f g)  (at level 80).

Class Op (A:Type) := op : A -> A -> A.

Set Typeclasses Iterative Deepening.

Class C F  `(Op F) (* `(Equivalence F) *) :=
{
    foo : forall a b , op a b == op a b;
}.

This finishes, so it probably is the instance outlined above repeating over and over again. The fix would be to not make this an instance or somehow cut it from being repeated.

[Alizter]

@coq/typeclasses-maintainers What is the correct way to restrict this instance short of removing it?

[SkySkimmer]

We restricted the depth to 2, so we look for instances that keep repeating. It looks like relation_equivalence_equivalence keeps getting used unhindered, which means when there is no depth restriction, this will spiral out of control.

That makes no sense, relation_equivalence_equivalence has no typeclass argument so it can't recurse.
The problem is Equivalence.pointwise_equivalence, which gets repeatedly applied because we're searching for an equivalence at an evar type (Set Printing All says Debug: 1: looking for (@Equivalence ?T ?e) with backtracking etc)

You can Hint Mode Equivalence ! - : typeclass_instances., in this case the Class C will still suceed because it will resolve Op which has no hint mode and gets Op F, then the type of the equivalence is resolved so it continues resolving and succeeds by picking eq_equivalence.
If you also Hint Mode Op ! : typeclass_instances. you then need to annotate foo : forall a b : F, ....

Putting Hint Mode on Equivalence may or may not break setoid rewriting or other stuff.
See also #38

[SkySkimmer]

Also note that the notation == will not work with the hint mode ! ! asked for in #38

[larsr]

Here is another small test case that goes into an infinite loop, for what I think is the same reason.

Require Import Coq.Classes.Equivalence.
Set Implicit Arguments.

Class A (F:Type) `{Equivalence F}  := { }.
Class V (V K:Type) `{Equivalence V} `{A K}  := { }.

Check (V  (K:=nat) ).  (* This works fine *)
Check V.             (* This goes into an infinite loop and never prints anything. *)

[Blaisorblade]

It seems indeed a duplicate of #38; this is one reason why hint modes are important.

[StevenTschantz]

I want to endorse this report as a serious problem. I too made a small error so that an intended Equivalence instance could not be found, sending the typeclass inference engine into an infinite regress with no clue where I had gone wrong. I recognize that I can err in writing instances that recurse infinitely and get what I deserve when I do. I found my mistake but then went searching for where I could have introduced the looping behavior. I traced the problem to Equivalence.pointwise_equivalence. This comes in indirectly through Setoids.Setoid from all over the standard library. I can't give up setoid rewriting so there is no avoiding this. I note in other places in the Classes libraries where there are comments about Hint Extern ... : typeclass_instances needed to drive typeclass inference avoiding looping from full resolution. I can only hope there can be some analogous fix here. Typeclass inference for setoid rewriting is magical and I can't begin to suggest how to repair this. But having typeclass inference looping when it can't find a needed instance isn't acceptable when it is due to something embedded so deeply in the standard library.