The Coq mailing list

[Daniel Selsam <daniel.selsam AT protonmail.com>]

Hello Coq community,

I am working on a new typeclass resolution procedure for Lean4, and I would like to make sure I understand how typeclass resolution works in Coq. Here are a bunch of examples of typeclass resolution succeeding and failing in Coq, with my attempted explanations. I would greatly appreciate if someone with expert knowledge could confirm or correct these interpretations. Thank you very much in advance for your help.

```

Module Diamonds.

Class Bottom (n : nat) : Set := {}.

Class Left (n : nat) : Set := {}.

Class Right (n : nat) : Set := {}.

Class Top (n : nat) : Set := {}.

Instance LeftToBottom (n : nat) (_ : Left n) : Bottom n := {}.

Instance RightToBottom (n : nat) (_ : Right n) : Bottom n := {}.

Instance TopToLeft (n : nat) (_ : Top n) : Left n := {}.

Instance TopToRight (n : nat) (_ : Top n) : Right n := {}.

Instance BottomToTop (n : nat) (_ : Bottom n) : Top (1+n) := {}.

(*

Problem: Succeeding tower of diamonds.

Result:  Succeeds in linear time.

*)

Example succeeding_tower (_ : Bottom 0) : Top 100 := _.

(*

Problem: Failing tower of diamonds.

Result:  Fails in exponential time.

Explain: No tabling/caching of failing subgoals.

*)

(* Example failing_tower : Top 100 := _. *)

Class None0 : Set := {}.

Class None1 (n : nat) : Set := {}.

Instance None0TopToNone1 (n : nat) (_ : Top n) (_ : None0) : None1 n := {}.

(*

Problem: Succeeding tower of diamonds, followed by failing subgoal.

Result:  Fails in linear time.

Explain: Coq detects that the `Top n` subgoal has no metavariables, and so it disables backtracking for this subgoal by replacing `Proofview.tclOR` with `Proofview.tclORELSE`.

*)

(* Example succeed_then_fail (_ : Bottom 0) : None1 100 := _. *)

Class Dep1 (n : nat) {top : Top n} : Set.

Class Dep2 (n : nat) {top : Top n} {dep1 : Dep1 n} : Set.

Instance Dep2ToNone1 (n : nat) (_ : Top n) (_ : Dep1 n) (_ : Dep2 n) : None1 n := {}.

Instance Dep1ToDep2 (n : nat) (_ : Top n) (_ : Dep1 n) : Dep2 n := {}.

(*

Problem: Succeeding tower of diamonds, followed by failing subgoal, with nested dependencies.

Result:  Fails in exponential time.

Explain: After applying `Dep2ToNone1`, Coq shelves `Top 100` and `Dep1 100`, since `Dep2 100` depends on them. However, when it finally unshelves, it unshelves them both at the same time, and fails to recognize that the latter depends on the former. Thus it tries to solve `Top 100` first *with* backtracking. This issue seems like it could be fixed easily, and is perhaps better more appropriately considered a bug than a limitation of the algorithm.

*)

(* Example multiple_shelved_goals (_inst_1 : Bottom 0) : None1 100 := _. *)

End Diamonds.

Module Loops.

Class Bottom : Set := {}.

Class Left : Set := {}.

Class Right : Set := {}.

Class Top : Set := {}.

Instance TopToLeft (_ : Top) : Left := {}.

Instance TopToRight (_ : Top) : Right := {}.

Instance LeftToBottom (_ : Left) : Bottom := {}.

Instance LeftToRight (_ : Left) : Right := {}.

Instance RightToLeft (_ : Right) : Left := {}.

(*

Problem: unsolvable problem with cycle.

Result:  infinite loop.

*)

(* Example BottomDfs : Bottom := _. *)

(*

Problem: unsolvable problem with cycle and iterative deepening.

Result:  infinite loop.

*)

Set Typeclasses Iterative Deepening.

(* Example BottomID : Bottom := _. *)

Unset Typeclasses Iterative Deepening.

(*

Problem: solvable problem with cycle (and unlucky instance ordering).

Result:  infinite loop.

*)

(* Example TopToBottomDfs (_ : Top) : Bottom := _. *)

(*

Problem: solvable problem with cycle and unlucky instance ordering, using iterative deepening.

Result:  success.

*)

Set Typeclasses Iterative Deepening.

Example TopToBottomID (_ : Top) : Bottom := _.

Unset Typeclasses Iterative Deepening.

End Loops.

Module Nested.

(* We tried exporting to Coq simplified versions of typeclass resolution problems arising in Mathlib, and found that many problems that succeed in Lean3 fail quickly in Coq. Although debugging issues like this can be tricky, I was able to construct a minimal example that seems to isolate a feature that Mathlib relies on heavily which is not supported in Coq. *)

Class Bottom (X : Set) : Set.

Class Left (X : Set) : Set.

Class Right (X : Set) : Set.

Instance LeftToBot {X : Set} (_left : Left X) : Bottom X := {}.

Instance RightToBot {X : Set} (_right : Right X) : Bottom X := {}.

Class Foo (X : Set) {bot : Bottom X} : Set.

Instance RightToLeft {X : Set} {right : Right X} : Left X := {}.

Instance LeftToFoo {X : Set} (left : Left X) : Foo X := {}.

(*

Problem: Typeclass resolution problem that requires synthesis during unification.

Result:  Fails.

Explain: Applying `FooLeft` to `Foo X` produces the unification problem `LeftToBot ?left =?= RightToBot right` which Coq is unable to solve. Note than in Lean (both versions 3 and 4), the unifier is able to solve constraints of this form by triggering typeclass resolution for `?left`, and would assign `?left := RightToLeft right`.

*)

(* Example needs_synth_on_failure (X : Set) {right : Right X} : Foo X := _. *)

End Nested.

```

Thanks very much,

Daniel