Zulip Chat Archive

Stream: general

Topic: trace.class_instances


view this post on Zulip Chris Hughes (Jul 15 2019 at 12:04):

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?

view this post on Zulip Paul van Wamelen (Sep 26 2020 at 21:02):

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)

view this post on Zulip Paul van Wamelen (Sep 26 2020 at 21:46):

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?

view this post on Zulip Floris van Doorn (Sep 26 2020 at 22:18):

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

view this post on Zulip Floris van Doorn (Sep 26 2020 at 22:18):

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

view this post on Zulip Floris van Doorn (Sep 26 2020 at 22:18):

One of them should not be an instance.

view this post on Zulip Floris van Doorn (Sep 26 2020 at 22:19):

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.

view this post on Zulip Floris van Doorn (Sep 26 2020 at 22:21):

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

view this post on Zulip Floris van Doorn (Sep 26 2020 at 22:23):

Probably ufm_of_gcd_of_wf_dvd_monoid should not be an instance.

view this post on Zulip Floris van Doorn (Sep 26 2020 at 22:24):

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.

view this post on Zulip Paul van Wamelen (Sep 26 2020 at 22:40):

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


Last updated: May 08 2021 at 18:17 UTC