Implicit variables and quotients

Stream: lean4

[Andrés Goens]

I ran into an issue where defining a function won't work with some implicit variables and quotients, because Lean can't figure out that two types are defeq because it won't unify the implicit parameters. (@Chris Hughes helped me figure out more or less what was happening there). Here's an attempt of mine to minimize it. I couldn't get this to work without Quotients, but I'm not sure if quotients are actually required or I just didn't find a minimal example without them:

import Mathlib.RingTheory.Polynomial.Quotient
import Mathlib.RingTheory.Ideal.Quotient

open Polynomial
noncomputable def f (n : Nat) : ℤ[X] := X^n + 1
abbrev R (n : Nat) := ℤ[X] ⧸ (Ideal.span {f n})

noncomputable def R.monomial {n : Nat} (k : Nat) : R n := Ideal.Quotient.mk (Ideal.span {f n}) (Polynomial.monomial k 1)
noncomputable def addXk : R n → Nat → R n
   --| p, k => p + R.monomial k -- (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
   | p, k => p + R.monomial k (n:=n) -- works

Is this a known problem? Is there a way to avoid doing that accidentally, or even better, help Lean figure out these things more easily? @Chris Hughes conjectured it might actually be the reason behind a bunch of the mysterious timeouts we seem to get with quotient rings.

[Junyan Xu]

I recall seeing some commands to enable/disable * as notation for docs#HMul, but forgot where. Maybe we should disable docs#HAdd here?

[Andrés Goens]

yeah, disabling HAdd would fix that behavior but it feels like avoiding the issue rather than addressing it, doesn't it? It sounds like getting this to work would require changes in core (or even in the kernel), so maybe that's the best way to do from the user's point of view, but I was hoping people who know the internals better than I do might have some more insights about it

[Junyan Xu]

Oh I think what I saw was lean4#2220 where Lean 4 assumes x and y are of the same type in x ^ y by default, which is undesirable. Here it's desirable to assume x and y are of the same type in x + y, and it's weird that Lean doesn't do so.