Zulip Chat Archive

Stream: new members

Topic: maximum class-instance resolution depth has been reached


Kris Brown (Jun 18 2020 at 01:37):

I'm trying to prove a theorem related to permutations of finite sets. At the beginning (trying to define a predicate on permutations to assert they are cyclic) and running into an issue that I don't know how to debug. The error (which is on the very last x of the very last definition) is "maximum class-instance resolution depth has been reached". I tried restarting Lean, setting class.instance_max_depth 1000, and I turned on trace.class_instances, though that spits out something extremely long that I can't make sense of. How should I approach this error, as a beginner?

import data.equiv.basic
import data.finset

open equiv -- "perm x" is "equiv x x" AKA "x ≃ x"
open nat

-- Repeat a binary function n times
def rep {α : Type*} :   (α  α)  α  α
 | 0 _ x := x
 | (succ n) f x := f (rep n f x)

-- Π (n : ℕ), perm (fin n) → fin n → fin n
#check λ (n:) (p: perm (fin n)) (x: fin n),
        rep n p.to_fun x

-- Predicate for a permutation on a finite set to be cyclic
def cyclic {n : } (p : perm (fin n)) :=
     x : fin n, rep n p.to_fun x = x

Jalex Stark (Jun 18 2020 at 01:38):

put a newline after your backticks tog et syntax highlighting

Jalex Stark (Jun 18 2020 at 01:39):

i don't get any error

Jalex Stark (Jun 18 2020 at 01:41):

you should change your instance_max_depth back to default, this may cause slowdowns for you later

Kris Brown (Jun 18 2020 at 01:42):

Thanks! and that's interesting; I'm using Lean 3.4.2 - are there any candidates for settings I could change to match your setup?

Jalex Stark (Jun 18 2020 at 01:43):

around here the suggestion is to use that latest leanprover-community build with the latest mathlib

Jalex Stark (Jun 18 2020 at 01:43):

managing that installation is easy with the leanproject tool

Jalex Stark (Jun 18 2020 at 01:44):

https://leanprover-community.github.io/get_started.html

Jalex Stark (Jun 18 2020 at 01:46):

you can use the lean web editor in the meantime

Jalex Stark (Jun 18 2020 at 01:46):

web editor

Scott Morrison (Jun 18 2020 at 01:52):

3.4.2 is pretty old by now (it's the last "official" release before switching to community development), and in particular is missing lots of nice improvements to the typeclass search algorithm.

Kris Brown (Jun 18 2020 at 03:46):

Thanks everyone, upgrading fixed this!

Antoine Labelle (Nov 10 2021 at 15:07):

Can someone help me figure out what the following error message means, and how to fix it?
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')
Here is my code :

import linear_algebra.trace

variables (k G V : Type*) [comm_ring k] [monoid G] [add_comm_group V]
variables [module k V] [distrib_mul_action G V] [smul_comm_class k G V]

def smul.linear_map (g : G) : V →ₗ[k] V :=
{ to_fun := λ m, g  m,
  map_add' := λ v w, by simp,
  map_smul' := λ r v, by simp [smul_comm] }

def character : G  k :=  λ g, linear_map.trace (smul.linear_map k G V g)

Johan Commelin (Nov 10 2021 at 15:16):

@Antoine Labelle It means that after a lot of searching Lean didn't find what it was looking for, but there was still stuff left to search.

Johan Commelin (Nov 10 2021 at 15:16):

Usually, this means that it ran into an infinite loop

Kevin Buzzard (Nov 10 2021 at 15:16):

If you hover over linear_map.trace or type #check linear_map.trace you'll see that it is expecting a ring and a module before the map

Kevin Buzzard (Nov 10 2021 at 15:16):

Lean is probably trying to find a ring structure on some linear map or space of linear maps, and getting confused.

Kevin Buzzard (Nov 10 2021 at 15:17):

noncomputable def character : G  k :=  λ g, linear_map.trace _ _ (smul.linear_map k G V g)

works fine

Kevin Buzzard (Nov 10 2021 at 15:17):

as does noncomputable def character : G → k := λ g, linear_map.trace k V (smul.linear_map k G V g)

Antoine Labelle (Nov 10 2021 at 15:20):

Thank I didn't see that. Sorry for the dumb question.

Kevin Buzzard (Nov 10 2021 at 15:21):

The error message is confusing. Usually when you make a mistake like this the error is "I was expecting a type and you gave me a morphism" and you can easily fix the problem yourself. But when Lean just gets utterly confused, like it does in this case for some reason, the error message is far less helpful; I debugged it by just building everything piece by piece instead of all in one go.

Eric Wieser (Nov 10 2021 at 15:24):

FWIW, your def is docs#distrib_mul_action.to_linear_map, I think

Antoine Labelle (Nov 10 2021 at 15:27):

Oh thanks, it's good to know :)

Eric Wieser (Nov 10 2021 at 17:19):

If it exists, you might also be interested in docs#distrib_mul_action.to_module_End (guess it doesn't exist, but docs#distrib_mul_action.to_add_monoid_End` should suggest what the statement is supposed to be!)


Last updated: Dec 20 2023 at 11:08 UTC