trace.class_instances

Stream: general

[Chris Hughes]

Is there a way of finding the actual instance search that's failing trace.class_instances requires me to scroll through a lot of useless information, and sometimes I can't even find anything. Is it possible to write some new option for this?

[Paul van Wamelen]

If type class resolution loops, I get the usual max depth reached error, but even with
set_option trace.class_instances true
I only see traces for other type class resolutions, the one that loops just says maximum class-instance resolution depth has been reached etc. Is that how it works, or am I missing something? (I'm in vscode)

[Paul van Wamelen]

Here is a #mwe:

import ring_theory.unique_factorization_domain

local attribute [instance] associated.setoid

set_option trace.class_instances true
lemma int.gcd_eq_inf [decidable_eq ℤ] [decidable_eq (associates ℤ)] {a b : ℤ}
  : (associates.mk a) ⊓ (associates.mk b) = associates.mk (int.gcd a b) := sorry

And my infoview:
mwe.PNG.jpg
Also, why do things seem to be duplicated?

[Floris van Doorn]

The resolution that is problematic is the one you can see when selecting ⊓. The error is just shown in a weird place.

[Floris van Doorn]

The offending instances that loop are
docs#unique_factorization_monoid.to_wf_dvd_monoid
docs#ufm_of_gcd_of_wf_dvd_monoid

[Floris van Doorn]

One of them should not be an instance.

[Floris van Doorn]

The reason that errors are duplicated is (I'm guessing) that Lean is backtracking after a first error, tries something else, and then hits the same error.

[Floris van Doorn]

@Aaron Anderson added/modified these instances in #4156. Can you make one of them not an instance?

[Floris van Doorn]

Probably ufm_of_gcd_of_wf_dvd_monoid should not be an instance.

[Floris van Doorn]

Ideally the fails_quickly linter should have caught this. However, the loop only happens if you have a [gcd_monoid α] instance, which is not the case in the test of the linter.

[Paul van Wamelen]

Thanks Floris, I see it now!
FWIW the error goes away when you also import ring_theory.principal_ideal_domain