Zulip Chat Archive

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

Kevin Buzzard (Apr 24 2018 at 16:18):

so I figured that it was about time I read the error properly

Kevin Buzzard (Apr 24 2018 at 16:18):

and I realised it was hard for me to increase the max_depth

Kevin Buzzard (Apr 24 2018 at 16:18):

because I didn't know what it currently was

Kevin Buzzard (Apr 24 2018 at 16:18):

so I looked at the trace

Kevin Buzzard (Apr 24 2018 at 16:18):

and it was really long

Kevin Buzzard (Apr 24 2018 at 16:18):

and complicated

Kevin Buzzard (Apr 24 2018 at 16:19):

and I spent some time trying to understand it

Kevin Buzzard (Apr 24 2018 at 16:19):

and in total spent over half an hour on this issue

Kevin Buzzard (Apr 24 2018 at 16:19):

before it occurred to me

Kevin Buzzard (Apr 24 2018 at 16:19):

that actually

Kevin Buzzard (Apr 24 2018 at 16:19):

maybe

Kevin Buzzard (Apr 24 2018 at 16:19):

the maximum class-instance resolution depth had been reached!

Kevin Buzzard (Apr 24 2018 at 16:19):

So I wrote set_option class.instance_max_depth 100

Kevin Buzzard (Apr 24 2018 at 16:19):

and the error went away!

Kenny Lau (Apr 24 2018 at 16:20):

lol

Kevin Buzzard (Apr 24 2018 at 16:20):

So I came to the conclusion

Kevin Buzzard (Apr 24 2018 at 16:20):

that either my code is really really cool and I am using type class resolution like a pro now

Kevin Buzzard (Apr 24 2018 at 16:20):

maybe my code is really really bad

Kevin Buzzard (Apr 24 2018 at 16:21):

and anyone who needs to change the default setting of the max class-instance resolution might want to take a look at what they're doing and how they're doing it.

Kevin Buzzard (Apr 24 2018 at 16:22):

And one thing that occured to me was that I might be being sloppy with the difference between proofs and data

Kevin Buzzard (Apr 24 2018 at 16:23):

but this might not be relevant, I'm not sure.

Kevin Buzzard (Apr 24 2018 at 16:23):

Here's a structure:

Kevin Buzzard (Apr 24 2018 at 16:23):

-- Here is the way KMB wants to package all these things together.
structure is_unique_R_alg_hom {R : Type u} {α : Type v} {β : Type w} [comm_ring R] [comm_ring α] [comm_ring β]
(sα : R → α) (sβ : R → β) (f : α → β) [is_ring_hom sα] [is_ring_hom sβ] [is_ring_hom f] :=
(R_alg_hom : sβ = f ∘ sα)
(is_unique : ∀ (g : α → β) [is_ring_hom g], sβ = g ∘ sα → g = f)

Kevin Buzzard (Apr 24 2018 at 16:23):

You make an instance of that structure by giving two proofs.

Kevin Buzzard (Apr 24 2018 at 16:24):

But the structure turns out to be a Type.

Kevin Buzzard (Apr 24 2018 at 16:24):

I could have rewritten this as is_unique_R_alg_hom blah := proof1 and proof2

Kevin Buzzard (Apr 24 2018 at 16:25):

and then it would be a Prop.

Kevin Buzzard (Apr 24 2018 at 16:25):

Should I change this, or does it not make a difference to anything?

Kevin Buzzard (Apr 24 2018 at 16:25):

And is it completely unrelated to the max class-instance resolution?

Kevin Buzzard (Apr 24 2018 at 16:26):

Oh I seem to just be able to make the structure a Prop anyway

Kevin Buzzard (Apr 24 2018 at 16:28):

aah, and now I don't need set_option class.instance_max_depth 52 (for 52 was the min to make it work)

Chris Hughes (Apr 24 2018 at 16:28):

Probably best to make it a Prop, to avoid issues with not recognizing that two instances of the same thing are equal.

Kevin Buzzard (Apr 24 2018 at 16:28):

because I seem to have forgotten things

Kevin Buzzard (Apr 24 2018 at 16:29):

Whyever would Lean make a structure whose constructor involved giving two proofs into a type??

Kevin Buzzard (Apr 24 2018 at 16:30):

Probably also best to make it into a Prop, because then I don't need to change a max depth to 52

Kevin Buzzard (Apr 24 2018 at 16:33):

no, the error is back

Kevin Buzzard (Apr 24 2018 at 16:33):

I am still getting used to new lean in VS Code

Kevin Buzzard (Apr 24 2018 at 16:33):

OK so my question remains

Kevin Buzzard (Apr 24 2018 at 16:34):

set_option class.instance_max_depth 52 -- !!
/-- universal property of inverting one element and then another -/
theorem away_away_universal_property {R : Type u} [comm_ring R] (f : R)
(g : loc R (powers f)) {γ : Type v} [comm_ring γ] (sγ : R → γ) [is_ring_hom sγ] (Hf : is_unit (sγ f))
(Hg : is_unit (away.extend_map_of_im_unit sγ Hf g)) :
is_unique_R_alg_hom
  ((of_comm_ring (loc R (powers f)) (powers g)) ∘ (of_comm_ring R (powers f)))
  sγ
  (away.extend_map_of_im_unit (away.extend_map_of_im_unit sγ Hf) Hg)
    := sorry

Kevin Buzzard (Apr 24 2018 at 16:34):

Is that first line evidence that I am doing something wrong?

Kevin Buzzard (Apr 24 2018 at 16:37):

If I set_option trace.class_instances true

Kevin Buzzard (Apr 24 2018 at 16:37):

then I get things like https://gist.github.com/kbuzzard/2a135ef1486fc55c3b4c70ca11cf50b4

Chris Hughes (Apr 24 2018 at 16:37):

How deep do you have to go if you try to do type class inference by hand? Maybe it's just a really hard type class inference problem, that requires that depth?

Kevin Buzzard (Apr 24 2018 at 16:37):

I don't think it's hard

Kevin Buzzard (Apr 24 2018 at 16:38):

I compose two ring homomorphisms

Kevin Buzzard (Apr 24 2018 at 16:38):

and I want the result to be a ring homomorphism

Kevin Buzzard (Apr 24 2018 at 16:39):

It's difficult to know where the exact problem is

Kevin Buzzard (Apr 24 2018 at 16:39):

because when I set trace.class_instances true pretty much everything gets underlined in green

Kevin Buzzard (Apr 24 2018 at 16:39):

and if I let it be 51

Kevin Buzzard (Apr 24 2018 at 16:40):

then the name of the theorem gets underlined in red

Kevin Buzzard (Apr 24 2018 at 16:41):

The biggest number I can find in brackets is (14)

Kevin Buzzard (Apr 24 2018 at 16:41):

[class_instances] (14) ?x_314 : discrete_linear_ordered_field R := rat.discrete_linear_ordered_field

Kevin Buzzard (Apr 24 2018 at 16:42):

the mind boggles

Kevin Buzzard (Apr 24 2018 at 16:42):

why is Lean wondering if my ring is a discrete linear ordered field?

Andrew Ashworth (Apr 24 2018 at 17:45):

because type class instance search is really dumb, it's basically searching the graph of all paths that might reach your proof

Andrew Ashworth (Apr 24 2018 at 17:47):

the more definitions and lemmas that you use with nested type class arguments, the bigger you'll need to set the search depth to

Kevin Buzzard (Apr 24 2018 at 17:50):

So are you saying that there is a non-zero chance that I might actually have to set the search depth to 52 and this doesn't just mean that my code is crappy?

Andrew Ashworth (Apr 24 2018 at 17:54):

in most cs applications the type class tree search is going to be somewhat shallow

Kevin Buzzard (Apr 24 2018 at 17:55):

I am pushing it

Kevin Buzzard (Apr 24 2018 at 17:55):

but I didn't realise I was pushing that hard

Andrew Ashworth (Apr 24 2018 at 17:55):

if you think it's going to be super deep, i wouldn't use type class search

Kevin Buzzard (Apr 24 2018 at 17:55):

I didn't think it was going to be super deep

Kevin Buzzard (Apr 24 2018 at 17:55):

I am surprised that I need 52

Kevin Buzzard (Apr 24 2018 at 17:56):

in the sense that I thought that all I was doing was trying to get Lean to spot that (a) the output of some function is a ring homomorphism and (b) the composite of two ring homomorphisms is a ring homomorphism

Kevin Buzzard (Apr 24 2018 at 17:56):

I don't understand how to find out where the pushing is occurring

Reid Barton (Apr 24 2018 at 17:56):

I wonder whether you actually need 52, or it's going off in some other unsuccessful part of the search that needs depth 52

Kevin Buzzard (Apr 24 2018 at 17:56):

I don't know how to find out

Reid Barton (Apr 24 2018 at 17:56):

Me neither

Kevin Buzzard (Apr 24 2018 at 17:56):

I put the debugging on and am immediately swimming in output

Patrick Massot (Apr 24 2018 at 18:09):

Maybe have a look at https://github.com/leanprover/mathlib/blob/master/data/real/basic.lean#L74

Patrick Massot (Apr 24 2018 at 18:09):

Sometimes you can help the type class resolution algorithm

Patrick Massot (Apr 24 2018 at 18:09):

By precomputing some shortcut

Patrick Massot (Apr 24 2018 at 18:09):

I have no idea if this applies in your case

Mario Carneiro (Apr 24 2018 at 18:13):

Do you have something I can test here myself?

Kevin Buzzard (Apr 24 2018 at 18:27):

I have a MWE but it didn't need 52

Kevin Buzzard (Apr 24 2018 at 18:27):

Kevin Buzzard (Apr 24 2018 at 18:30):

I can point you to a theorem in lean-stacks-project if that's what you mean

Kevin Buzzard (Apr 24 2018 at 18:30):

line 138 of tag01HR.lean

Kevin Buzzard (Apr 24 2018 at 18:31):

https://github.com/kbuzzard/lean-stacks-project

Kevin Buzzard (Apr 24 2018 at 18:31):

wait

Kevin Buzzard (Apr 24 2018 at 18:31):

I need to push

Kevin Buzzard (Apr 24 2018 at 18:33):

https://github.com/kbuzzard/lean-stacks-project/blob/179ff95b6bd8d4998e1a007b2e8942179d9e24a8/src/tag01HR.lean#L138

Kevin Buzzard (Apr 24 2018 at 18:36):

Thanks for pointing that out Patrick. I don't know if this applies in my situation because I have no idea what the problem is. I didn't think I was doing anything too weird.

Kevin Buzzard (Apr 24 2018 at 18:37):

PS @Mario Carneiro I commented everything out from line 171 onwards (I mention this because it's not so easy to spot in VS Code)

Mario Carneiro (Apr 24 2018 at 20:15):

By the way another way to comment everything out after a certain point is #exit, which also causes a notification so it's not so hard to spot

Kevin Buzzard (Apr 24 2018 at 22:28):

woohoo

Kevin Buzzard (Apr 24 2018 at 22:28):

new record

Kevin Buzzard (Apr 24 2018 at 22:28):

noncomputable definition loc_is_loc_loc {R : Type u} [comm_ring R] (f g : R) :
R_alg_equiv
  ((of_comm_ring (loc R (powers f)) (powers (of_comm_ring R (powers f) g)))
  ∘ (of_comm_ring R (powers f)))
  (of_comm_ring R (powers (f * g))) :=

Kevin Buzzard (Apr 24 2018 at 22:28):

proof that R[1/f][1/g] = R[1/fg]

Kevin Buzzard (Apr 24 2018 at 22:28):

set_option class.instance_max_depth 93

Kevin Buzzard (Apr 24 2018 at 22:28):

:-)

Kevin Buzzard (Apr 24 2018 at 22:28):

I don't like the way this is going...

Kevin Buzzard (Apr 24 2018 at 22:31):

Here's the proof:

Kevin Buzzard (Apr 24 2018 at 22:31):

R_alg_equiv_of_unique_homs
  (away_away_universal_property' f g (of_comm_ring R (powers (f * g)))
    (unit_of_loc_more_left f g) -- proof that f is aunit in R[1/fg]
    (unit_of_loc_more_right f g) -- proof that g is a unit in R[1/fg]
  )
  (away_universal_property (f*g)
    ((of_comm_ring (loc R (powers f)) (powers (of_comm_ring R (powers f) g)))
      ∘ (of_comm_ring R (powers f)))
    (tag01HR.unitfg f g) -- proof that fg is a unit in R[1/f][1/g]
  )
  (away_away_universal_property' f g ((of_comm_ring (loc R (powers f)) (powers (of_comm_ring R (powers f) g))) ∘ (of_comm_ring R (powers f)))
    (tag01HR.unitf f g) -- proof that f is a unit in R[1/f][1/g]
    (tag01HR.unitg f g) -- proof that g is a unit in R[1/f][1/g]
  )
  (id_unique_R_alg_from_loc _)

Kevin Buzzard (Apr 24 2018 at 22:31):

All universal properties

Last updated: Dec 20 2023 at 11:08 UTC