Slow elaboration using Submodule.span and struct field

Stream: general

[Aaron Hill]

In the following code, elaboration takes ~12 seconds in Lean 4 Web:

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.LinearAlgebra.Finsupp.VectorSpace

set_option trace.profiler true

structure MySpans where
  struct_val: ℕ
  const_arg: Submodule.span ℚ { (Finsupp.single 1 1 : (ℕ →₀ ℚ)) }
  struct_arg: Submodule.span ℚ { (Finsupp.single struct_val 1 : (ℕ →₀ ℚ)) }

with the trace:

[Elab.command] [12.224461] structure MySpans where
      struct_val : ℕ
      const_arg : Submodule.span ℚ {(Finsupp.single 1 1 : (ℕ →₀ ℚ))}
      struct_arg : Submodule.span ℚ {(Finsupp.single struct_val 1 : (ℕ →₀ ℚ))} ▼
  [step] [0.019285] expected type: Sort ?u.6, term
    Submodule.span ℚ {(Finsupp.single 1 1 : (ℕ →₀ ℚ))}
  [Meta.sizeOf] [0.024981] MySpans
  [Meta.injective] [0.031896] MySpans.mk

If I comment out struct_arg, elaboration takes ~0.1 seconds.
Why does this take so long to elaborate?

[Eric Wieser]

Even this is slow:

import Mathlib.Analysis.Normed.Module.Basic
import Mathlib.LinearAlgebra.Finsupp.VectorSpace

-- elaborate this up-front, which is fast
def s (n : ℕ) : Type _ := Submodule.span ℚ {(Finsupp.single struct_val 1 : (ℕ →₀ ℚ))}

suppress_compilation
set_option trace.profiler true

structure MySpans where
  struct_val: ℕ
  struct_arg: s struct_val

[Eric Wieser]

Changing def to opaque makes it instant

[Kevin Buzzard]

For the latter code I currently get unknown identifier 'struct_val', presumably there is a typo somewhere. For the former it's also slow for me. Furthermore the timings don't add up, which is something I never understood.

[Eric Wieser]

Timings not adding up is expected, it corresponds to something like the pseudocode

def foo := time "foo" do
  time "a" doA
  time "b" doB
  doC
  time "d" doD

which will not create any subtiming for doC

[Eric Wieser]

But of course this suggests Lean should add another timing block for whatever is not being categorized here

[Eric Wieser]

See #19855 for an example of real code doing this

[Aaron Hill]

I think the definition of s is supposed to be def s (n : ℕ) : Type _ := Submodule.span ℚ {(Finsupp.single n 1 : (ℕ →₀ ℚ))}