Cross mudule timeout w/ @[to_additive] handle

Stream: mathlib4

[Fengyang Wang]

I had this timeout problem. Calling an instance generated by to_additive within a module with an explicit typeclass signature has no issue, but importing this module in another file and then calling it results in a timeout.

@[to_additive (dont_translate := R) (relevant_arg := 1) lp.one_addMulConvolution_memℓp
  /-- The additive ring multiplication convolution of ℓ¹ functions is in ℓ¹. -/]
theorem lp.one_mulConvolution_memℓp (f g : lp (fun _ : M => R) 1) :
    Memℓp (mulConvolution (⇑f) (⇑g)) 1 := by

/-- Newtype wrapper for ℓ¹ with additive convolution.
`AddLp M R` is `lp (fun _ : M => R) 1` with multiplication via `addMulConvolution`. -/
structure AddLp (M : Type*) (R : Type*) [NormedAddCommGroup R] where
  /-- The underlying lp element. -/
  toLp : lp (fun _ : M => R) 1

namespace AddLp
/- * `DiscreteConvolution.addMulConvolution f g`:
additive ring multiplication `f ⋆₊ₘ g` -/

instance instMul : Mul (AddLp M R) where
  mul f g := ⟨(⇑f.toLp) ⋆₊ₘ (⇑g.toLp), lp.one_addMulConvolution_memℓp f.toLp g.toLp⟩

instMul runs fine. However, importing this module and then running the exact lines in the new file times out.

set_option profiler.threshold 10000 in
set_option trace.profiler true in
instance instMul' : Mul (AddLp M R) where
  mul f g := ⟨(⇑f.toLp) ⋆₊ₘ (⇑g.toLp), lp.one_addMulConvolution_memℓp f.toLp g.toLp⟩

Its trace looks something like

 lp.one_addMulConvolution_memℓp f.toLp g.toLp ▼
                    [] [9.029899] expected type: ↥(lp (fun x ↦ R) 1), term
                        f.toLp ▼
                      [Meta.isDefEq] [9.029631] 💥️ ↥(lp (fun x ↦ ?m.25) 1) =?= ↥(lp (fun x ↦ R) 1) ▼
                        [] [9.029443] 💥️ fun x ↦ x ∈ lp (fun x ↦ ?m.25) 1 =?= fun x ↦ x ∈ lp (fun x ↦ R) 1 ▼
                          [] [9.028767] 💥️ x ∈ lp (fun x ↦ R) 1 =?= x ∈ lp (fun x ↦ R) 1

Meanwhile, in that new file, calling the same instance as below doesn't leads to timeout

protected lemma addMulConvolution_memℓp' (f g : lp (fun _ : M => R) 1) :
    Memℓp ((⇑f) ⋆₊ₘ (⇑g)) 1 :=
  @lp.one_addMulConvolution_memℓp M R _ _ f g

protected lemma addDelta_memℓp' : Memℓp (addDelta (M := M) (1 : R)) 1 :=
  @lp.one_addDelta_memℓp M R _ _ _

Seems to be a unification problem. I can't figure out why it behaves differently across locations. There are also times when I place the lemmas in a different order resolves the timeout. Has anyone had this issue before? Any workaround?

[Fengyang Wang]

I sort of figured out the cause. It was surprisingly exactly because of the placement of the lemmas. More precisely, it was because of sectional variables creating †wo paths to the same type, and Lean wants to unify these two instances, which is fairly expensive.

variable {R : Type*}

-- With ONLY NormedCommRing: unique path to NormedAddCommGroup
example [NormedCommRing R] : NormedAddCommGroup R := inferInstance

-- With BOTH in scope: two distinct instance terms for NormedAddCommGroup
variable [inst1 : NormedAddCommGroup R] [inst2 : NormedCommRing R]

/- These are two DIFFERENT terms of type NormedAddCommGroup R: -/

-- the explicit variable
#check (inst1 : NormedAddCommGroup R)            -- Output: inst1 : NormedAddCommGroup R

-- derived from inst2
#check (inferInstance : NormedAddCommGroup R)       -- Output: inferInstance : NormedAddCommGroup R

During elaboration, Lean may need to unify these two instances. Since they are not definitionally equal, this requires expensive checks. So we have

-- BAD: causes timeout (two paths to NormedAddCommGroup R)
-- variable [NormedAddCommGroup R] [AddMonoid M] [NormedCommRing R] [DecidableEq M]

-- GOOD: single path to NormedAddCommGroup R via NormedCommRing
variable [AddMonoid M] [NormedCommRing R] [DecidableEq M]

This can decisively trigger and resolve the timeout problem. Is it me extra dumb, or should I blame this on Lean? Or both?

[Ruben Van de Velde]

Yeah, you shouldn't have both of these present at the same time, I don't think

[Fengyang Wang]

Learned a cool phrase, instance diamond, although in a hard way.