Set Typeclasses Debug should inform when instances are skipped due to Hint Mode

[RalfJung]

Version

8.8

Operating system

Linux

Description of the problem

I've spent many frustrating hours debugging typeclass issues that ended up being related to Hint Mode. We are fairly aggressive in setting modes because that's the only way to avoid having exponential behavior all over the place, all the time -- but the downside is that if you get it wrong, Set Typeclasses Debug will just silently skip your instances and not even tell you that it is doing so, let alone why.

it would be extremely helpful if the typeclass debug output could say things like "not considering hint XYZ due to Hint Mode".

[Zimmi48]

Even with verbosity level 2? I agree that it should mention what it is skipping and why when using this verbosity level.

[RalfJung]

This is the first time I ever hear about "verbosity levels". The doc search doesn't know about them though?

[Zimmi48]

https://coq.inria.fr/refman/addendum/type-classes.html#coq:opt.typeclasses-debug-verbosity-num

[RalfJung]

Interesting, I did not know this can be tuned further. But it doesn't seem to help either:

<prompt>cinv_cancel < 119 |cinv_cancel| 0 < </prompt>Set Typeclasses Debug Verbosity 2.

<prompt>cinv_cancel < 121 |cinv_cancel| 0 < </prompt>iInv N as "[HP|>Hγ']".
<infomsg>
Debug:
Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded
</infomsg>
<infomsg>Debug: 1: looking for (IntoInv (inv N (P' ∨ cinv_own γ 1)%I) N) without backtracking
</infomsg>
<infomsg>
Debug: 1.1: simple apply @into_inv_inv on (IntoInv (inv N (P' ∨ cinv_own γ 1)%I) N), 0 subgoal(s)
</infomsg>
<infomsg>Debug: 1.1: after simple apply @into_inv_inv finished, 0 goals are shelved and unsolved ( )
</infomsg>
<infomsg>
Debug:
Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded
</infomsg>
<infomsg>
Debug:
1: looking for (ElimInv ?φ (inv N (P' ∨ cinv_own γ 1)%I) ?Pin ?Pout None (|={E}=> (▷ P)%I) ?Q') with backtracking
</infomsg>
<infomsg>
Debug:  shelving dependent subgoals: 745 (() → uPredSI (iResUR Σ)) 746 (() → uPredSI (iResUR Σ)) 747
(BiFUpd (uPredSI (iResUR Σ))) 748 coPset 749 coPset 750 (() → uPredSI (iResUR Σ)) 751
(() → option (uPredSI (iResUR Σ)))</infomsg>
<infomsg>
Debug: 1.1: simple eapply @class_instances_sbi.elim_inv_acc_without_close on
(ElimInv ?φ (inv N (P' ∨ cinv_own γ 1)%I) ?Pin ?Pout None (|={E}=> (▷ P)%I) ?Q'), 2 subgoal(s)
</infomsg>
<infomsg>Debug: 1.1-1 : (IntoAcc (inv N (P' ∨ cinv_own γ 1)%I) ?φ ?Pin ?E1 ?E2 ?α ?β ?γ)</infomsg>
<infomsg>Debug: calling eauto recursively at depth 2 on 1 subgoals</infomsg>
<infomsg>
Debug:
1.1-1: looking for (IntoAcc (inv N (P' ∨ cinv_own γ 1)%I) ?φ ?Pin ?E1 ?E2 ?α ?β ?γ) with backtracking
</infomsg>
<infomsg>
Debug:
1.1-1: no match for (IntoAcc (inv N (P' ∨ cinv_own γ 1)%I) ?φ ?Pin ?E1 ?E2 ?α ?β ?γ), 0 possibilities
</infomsg>
<infomsg>
Debug:
1.1: simple eapply @class_instances_sbi.elim_inv_acc_without_close failed with: Proof-search failed.
</infomsg>

The IntoAcc typeclass is the one that has a too restrictive mode.

[RalfJung]

Somewhat related, Hint Extern that match the goal but fail are also not logged at all -- which can make debugging much harder:

Class C (n:nat) := KLASSE : unit.
Hint Extern 0 (C _) => fail : typeclass_instances.

Set Typeclasses Debug.
Goal (C 10).
Fail apply _.
(*
Debug: 1: looking for (C 10) without backtracking
Debug: 1: no match for (C 10), 1 possibilities
The command has indeed failed with message:
Cannot infer this placeholder of type "C 10" (no type class instance found).
*)

Restart.
Hint Extern 10 (C _) => exact tt : typeclass_instances.
apply _.
(*
Debug: 1: looking for (C 10) without backtracking
Debug: 1.1: (*external*) exact tt on (C 10), 0 subgoal(s)
*)