Deterministic timeout with Inhabited from Zero

Stream: mathlib4

[Tomas Skrivan]

I wanted to play around with modules, so I ported the basic definitions from original mathlib. Unfortunately, these definitions combined with this instance of Inhabited: instance {α} [Zero α] : Inhabited α := ⟨0⟩ do not work properly. Simple scalar multiplication r*x gives deterministic timeout, you can crank up the maxHeartbeats to 2000 but we probably want to keep that low as possible, so I'm reporting it.

Few notes:

1. Setting low priority to the instance of Inhabited does not solve the problem.
2. The problem occurs only when you import the whole mathlib import Mathlib

[Tomas Skrivan]

mwe:

-- import Mathlib.Algebra.Ring.Basic -- ok with only this
import Mathlib

instance {α} [Zero α] : Inhabited α := ⟨0⟩
instance {α} [One α] : Inhabited α := ⟨1⟩

class MulAction (α : Type u) (β : Type v) [Monoid α] extends HMul α β β :=
(one_smul : ∀ b : β, (1 : α) * b = b)
(mul_smul : ∀ (x y : α) (b : β), (x * y) * b = x * y * b)

class DistribMulAction (M : Type u) (A : Type v) [Monoid M] [AddMonoid A]
  extends MulAction M A :=
(smul_add : ∀(r : M) (x y : A), r * (x + y) = r * x + r * y)
(smul_zero : ∀(r : M), r * (0 : A) = 0)

-- set_option synthInstance.maxHeartbeats 2000

variable {R M} [Ring R] [AddCommGroup M] [DistribMulAction R M] (r s : R) (x y : M)

#check r * x  -- (deterministic) timeout at 'typeclass'

class Module (R : Type u) (M : Type v) [Semiring R]
  [AddCommMonoid M] extends DistribMulAction R M :=
(add_smul : ∀(r s : R) (x : M), (r + s) * x = r * x + s * x)
(zero_smul : ∀x : M, (0 : R) * x = 0)

variable {R M} [Ring R] [AddCommGroup M] [Module R M] (r s : R) (x y : M)

#check (r * x)

[Kevin Buzzard]

Those two instances at the top are likely to cause diamonds

[Tomas Skrivan]

Is that a problem in Lean 4?

[Kevin Buzzard]

(unless inhabited is a Prop)

[Tomas Skrivan]

No it is not Prop

[Kevin Buzzard]

I have no idea if it's a problem in lean 4. In Lean 3 I thought we used outparams to do this, or did at some point. Am I out of date?

[Gabriel Ebner]

Setting low priority to the instance of Inhabited does not solve the problem.

Instance priorities rarely do what you want them to do, just avoid them.

[Johan Commelin]

@Tomas Skrivan Do you want Nonempty instead?

[Tomas Skrivan]

Johan Commelin said:

Tomas Skrivan Do you want Nonempty instead?

Good idea! I'm using it in noncomputational context anyway, so I can use Classical.choice to actually get an element.

[Gabriel Ebner]

The inhabited instances need to go of course. But the issue why this blows up here is because of something different: when lean elaborates m * n it tries to coerce m into n (to see if it can turn the heterogeneous operation into a homogeneous one). In other words, (x : R) triggers the same type class timeout.

The reason is that instance [Numeric α] : Coe ℕ α is apparently too general, and introduces metavariables during TC synthesis. Changing the Coe to CoeTC here makes the example work even with the conflicting inhabited instances.

[Tomas Skrivan]

Thanks a lot for investigating, I have noticed lots of Coe and Numeric in the trace output but was unable to make sense of.

[Tomas Skrivan]

In other words, (x : R) triggers the same type class timeout.

I can't reproduce that. It works fine for me.

[Gabriel Ebner]

You won't see it in the error message, the coercion code will silently ignore the timeout. But you can still see the type class search in the trace output.