Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Inaccurate tactic trace from Set Typeclasses Debug #19930

Open
JonasOberhauser opened this issue Dec 13, 2024 · 0 comments
Open

Inaccurate tactic trace from Set Typeclasses Debug #19930

JonasOberhauser opened this issue Dec 13, 2024 · 0 comments
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Error messages, warnings, etc. needs: triage The validity of this issue needs to be checked, or the issue itself updated.

Comments

@JonasOberhauser
Copy link

Description of the problem

When using Set Typeclasses Debug Verbosisty 2, a failed typeclass search will claim that it used simple apply. This is confusing when simple apply succeeds. The tactic trace should instead show that it used class_apply.

Small Rocq / Coq file to reproduce the bug

Require Import Utf8.
Require Import Setoid.
Require Import Basics.
Require Import Coq.Classes.RelationClasses.


Goal ∀  (r : predicate (Tcons nat Tnil)), predicate_implication r r.
Proof.
Succeed simple apply @PreOrder_Reflexive.

Set Typeclasses Debug Verbosity 2.
Fail reflexivity.

(*
  1.1: simple apply @PreOrder_Reflexive on
  (@Reflexive (arrows (Tcons nat Tnil) Prop) (@predicate_implication (Tcons nat Tnil))) failed with: In environment
  r : arrows (Tcons nat Tnil) Prop
  Unable to unify "binary_relation (arrows (Tcons nat Tnil) Prop)" with "relation (arrows (Tcons nat Tnil) Prop)".

*)

Version of Rocq / Coq where this bug occurs

8.19.2

Last version of Rocq / Coq where the bug did not occur

No response
@JonasOberhauser JonasOberhauser added kind: bug An error, flaw, fault or unintended behaviour. needs: triage The validity of this issue needs to be checked, or the issue itself updated. labels Dec 13, 2024
@SkySkimmer SkySkimmer added the kind: user messages Error messages, warnings, etc. label Dec 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. kind: user messages Error messages, warnings, etc. needs: triage The validity of this issue needs to be checked, or the issue itself updated.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JonasOberhauser @SkySkimmer