deep recursion was detected at 'live variable analysis'

Stream: general

[Eric Wieser]

I tried replacing docs#Lp.simple_func.module with:

protected def module : module 𝕜 (Lp.simple_func E p μ) :=
function.injective.module 𝕜
  ((Lp.simple_func E p μ).subtype : Lp.simple_func E p μ →+ Lp E p μ)
  subtype.coe_injective
  coe_smul

and got an error message I've never seen before:

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

Is there any way to help lean out here short of just not using function.injective.module?

[Anne Baanen]

I suspect the reason is that Lp.simple_func is a very complicated type since it's a subgroup of a subgroup.

[Kevin Buzzard]

Mathematicians would laugh at the idea that such a notion is "very complicated" :-(