maximum class-instance resolution depth has been reached

Stream: new members

[Kris Brown]

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]

put a newline after your backticks tog et syntax highlighting

[Jalex Stark]

i don't get any error

[Jalex Stark]

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

[Kris Brown]

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]

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

[Jalex Stark]

managing that installation is easy with the leanproject tool

[Jalex Stark]

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

[Jalex Stark]

you can use the lean web editor in the meantime

[Jalex Stark]

web editor

[Scott Morrison]

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]

Thanks everyone, upgrading fixed this!

[Antoine Labelle]

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]

@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]

Usually, this means that it ran into an infinite loop

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

works fine

[Kevin Buzzard]

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

[Antoine Labelle]

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

[Kevin Buzzard]

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]

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

[Antoine Labelle]

Oh thanks, it's good to know :)

[Eric Wieser]

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!)