deep recursion

Stream: general

[Johan Commelin]

How can I debug the following error?

deep recursion was detected at 'replace' (potential solution: increase stack space in your system)

It showed up while trying to define a class. As far as I can see there is no loop or something...

[Kenny Lau]

have you tried turning Lean off and on again?

[Johan Commelin]

Yes, in fact I have.

[Johan Commelin]

I've found the culprit:

-- somewhere in the perfectoid project
local attribute [instance] topological_add_group.to_uniform_space

[Johan Commelin]

I've now put a section ... end around this attribute (and its one use) and the problem is gone.
So... this question is solved. Thanks for letting me rubber-duck this issue!

[Yaël Dillies]

I'm hitting this error in #7123. MWE

import data.fintype.basic

open_locale classical

/-- A finite bounded lattice is complete. -/
noncomputable instance fintype.to_complete_lattice (α : Type*) [fintype α] [hl : lattice α]
  [hb : bounded_order α] :
  complete_lattice α :=
{ Sup := λ s, s.to_finset.sup id,
  Inf := λ s, s.to_finset.inf id,
  le_Sup := sorry,
  Sup_le := sorry,
  Inf_le := sorry,
  le_Inf := sorry,
  .. hl, .. hb }

variables {α : Type*} [bounded_order α]
-- deep recursion was detected at 'expression equality test' (potential solution: increase stack
-- space in your system)

and I don't know how to circumvent it.

[Yaël Dillies]

Precisely, it happens because [bounded_order α] looks for [has_le α], which it tries to get from [complete_lattice α], which it tries to get using fintype.to_complete_lattice, which needs [bounded_order α]... This instance is bad, and I know it, but in this PR I need it to prove 2 lemmas about it (and then it's used once on fin).

[Yakov Pechersky]

does lowering priority help?

[Yaël Dillies]

Should I simply give up on stating those lemmas generally and simply provide them for fin?

[Yaël Dillies]

Nope...

[Yaël Dillies]

Btw Yakov this is an unforeseen consequence of your refactor :sad:

[Yakov Pechersky]

Yeah I can see that

[Yakov Pechersky]

I'll have to take a look in a couple of days

[Yaël Dillies]

One solution is

variables {α : Type*} [hα : lattice α] [@bounded_order α $ @preorder.to_has_le α $ @partial_order.to_preorder α $ semilattice_inf.to_partial_order α]

:nauseated:

[Eric Wieser]

If this instance is bad, why not make it a def?

[Yaël Dillies]

In the PR, it is a def. The point was to make it an instance for one section to prove general lemmas about when it's used, but TC inference already pukes at the variables.

[Eric Wieser]

I think it would be better to use by haveI := ...; exact ... in the theorem statement

[Eric Wieser]

(which elaborates without any let bindings)

[Yaël Dillies]

So I solved it by simply swapping the variables and local attribute.

variables {ι α : Type*} [fintype ι] [fintype α] [lattice α] [bounded_order α]

-- this line is crucially *after* the `variables` so that `bounded_order` gets filled in correctly
local attribute [instance] fintype.to_complete_lattice

Apparently Lean fills in the arguments in stuff declared in variables at declaration time rather than at each lemma?

[Floris van Doorn]

This is correct. For example, see the difference here:

variables {α : Type*}
example : α = ℕ := sorry -- error
example {β : Type*} : β = ℕ := sorry -- no error

The first example fails, because α : Type u_1, and the universe variable u_1 cannot be unified with 0. The second example works, because the universe metavariable in the type of β can be unified with 0 (of course, the Type* is super misleading, since it's just Type).

[Yakov Pechersky]

Ah, I see, you wanted to have bounded_order without specifying the order (has_le) or anything else. Yeah, that won't work.

[Yakov Pechersky]

Do you get the the same style of error if you invoke a new type alpha and [topological_group alpha] without saying [group alpha]?