Error using support when importing `data.real.basic`

Stream: general

[Stanislas Polu]

Hi, here's a minimal example showing that importing data.real.basic may cause an unexpected deep recursion error:

import algebra.big_operators.basic
import group_theory.perm.support
import data.nat.interval
import data.real.basic --delete this line and it compiles

open_locale big_operators

theorem amc12a_2012_p24
  (a : ℕ → ℕ)
  (σ : equiv.perm (finset.Ico (1 : ℕ) 2012))
  (h₆ : ∀ i j, i < j → (a ∘ coe ∘ σ) j ≤ (a ∘ coe ∘ σ) i) :
  ∑ k in σ.support, (k : ℕ) = 1341 := sorry

(h/t @Mantas Baksys)

What is the preferred process to report this as a potential bug? :pray:

[Stanislas Polu]

For context:

• the original statements has additional hypothesis that require the reals.
• this statement used to compile correctly without recursion error on older mathlib, in particular: 2fd713a76e15eebdcdfd2f94472584b3f5f2bfc7

[Mantas Baksys]

Note that a more minimal example (wrt imports of data.real.basic) on the import chain is the following

import group_theory.perm.support
import data.nat.interval
import data.pnat.basic --delete this line and it compiles

open_locale big_operators

theorem amc12a_2012_p24
  (a : ℕ → ℕ)
  (σ : equiv.perm (finset.Ico (1 : ℕ) 2012))
  (h₆ : ∀ i j, i < j → (a ∘ coe ∘ σ) j ≤ (a ∘ coe ∘ σ) i) :
  ∑ k in σ.support, (k : ℕ) = 1341 := sorry

[Alex J. Best]

Even more minimal

import data.nat.interval
import data.pnat.basic --delete this line and it compiles

#check (infer_instance : decidable_eq (finset.Ico (0 : ℕ) 2012))

[Alex J. Best]

I guess lean is recursing a lot trying to unify pnat with finset.Ico 0 2012, when searching for decidable equality instances

[Alex J. Best]

A workaround is local attribute [-instance] pnat.decidable_eq

[Alex J. Best]

Alternatively marking pnat as irreducible locally also works

[Gabriel Ebner]

Oh wait, does this mean the α in decidable_eq α is unified with semireducible transparency because it only appears as an implicit argument after unfolding decidable_eq α?