TC synthesis timeout

Stream: mathlib4

[Henrik Böving]

I have a timeout in TC synthesis in https://github.com/leanprover-community/mathlib4/pull/1229 on the second last instance in the file. The MWE is:

import Mathlib.Data.Int.Cast.Prod
import Mathlib.Algebra.Order.Monoid.Prod

/-!
# Semiring, ring etc structures on `R × S`

In this file we define two-binop (`semiring`, `ring` etc) structures on `R × S`. We also prove
trivial `simp` lemmas, and define the following operations on `ring_hom`s and similarly for
`non_unital_ring_hom`s:

* `fst R S : R × S →+* R`, `snd R S : R × S →+* S`: projections `prod.fst` and `prod.snd`
  as `ring_hom`s;
* `f.prod g : `R →+* S × T`: sends `x` to `(f x, g x)`;
* `f.prod_map g : `R × S → R' × S'`: `prod.map f g` as a `ring_hom`,
  sends `(x, y)` to `(f x, g y)`.
-/


variable {α β R R' S S' T T' : Type _}

namespace Prod

/-- Product of two distributive types is distributive. -/
instance [Distrib R] [Distrib S] : Distrib (R × S) :=
  { inferInstanceAs (Add (R × S)), inferInstanceAs (Add (R × S)) with
    left_distrib := fun _ _ _ => mk.inj_iff.mpr ⟨left_distrib _ _ _, left_distrib _ _ _⟩
    right_distrib := fun _ _ _ => mk.inj_iff.mpr ⟨right_distrib _ _ _, right_distrib _ _ _⟩ }

/-- Product of two semirings is a semiring. -/
instance [Semiring R] [Semiring S] : Semiring (R × S) :=
  { inferInstanceAs (AddCommMonoid (R × S)), inferInstanceAs (MonoidWithZero (R × S)), inferInstanceAs (Distrib (R × S)), inferInstanceAs (AddMonoidWithOne (R × S)) with }

/-- Product of two rings is a ring. -/
instance [Ring R] [Ring S] : Ring (R × S) :=
  { inferInstanceAs (AddCommGroup (R × S)), inferInstanceAs (AddGroupWithOne (R × S)), inferInstanceAs (Semiring (R × S)) with }

end Prod

/-! ### Order -/

instance [OrderedSemiring α] [OrderedSemiring β] : OrderedSemiring (α × β) :=
  { inferInstanceAs (Semiring (α × β)), inferInstanceAs (PartialOrder (α × β)) with
    add_le_add_left := fun _ _ => add_le_add_left
    zero_le_one := ⟨zero_le_one, zero_le_one⟩
    mul_le_mul_of_nonneg_left := fun _ _ _ hab hc =>
      ⟨mul_le_mul_of_nonneg_left hab.1 hc.1, mul_le_mul_of_nonneg_left hab.2 hc.2⟩
    mul_le_mul_of_nonneg_right := fun _ _ _ hab hc =>
      ⟨mul_le_mul_of_nonneg_right hab.1 hc.1, mul_le_mul_of_nonneg_right hab.2 hc.2⟩ }

--instance [OrderedRing α] [OrderedRing β] : OrderedRing (α × β) :=
--  { Prod.ring, Prod.orderedSemiring with
--    mul_nonneg := fun a b ha hb => ⟨mul_nonneg ha.1 hb.1, mul_nonneg ha.2 hb.2⟩ }
instance [OrderedRing α] [OrderedRing β] : OrderedRing (α × β) :=
  { inferInstanceAs (Ring (α × β)), inferInstanceAs (OrderedSemiring (α × β)) with
    mul_nonneg := fun a b ha hb => ⟨mul_nonneg ha.1 hb.1, mul_nonneg ha.2 hb.2⟩ }

Error is just a simple heartbeat timeout:

63:0:
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
64:2:
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
64:2:
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
64:2:
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
64:2:
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
64:2:
(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
63:0:
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

Locally increasing the heartbeats does also not help, it seems to be stuck.

[Yury G. Kudryashov]

I'm going to checkout the branch.

[Yury G. Kudryashov]

My guess: Lean tries to unpack/repack instances and fails defeq.

[Yury G. Kudryashov]

This can be a side effect of the new structure eta rfl rule.

[Henrik Böving]

So how do we proceed with this?

[Yury G. Kudryashov]

I fixed compile but this is a workaround.

[Yury G. Kudryashov]

I reordered all inferInstanceAs to mirror extends, then copied zero_le_one instead of inheriging it.

[Henrik Böving]

How did you know it was specifically zero_le_one?

[Yury G. Kudryashov]

It is repeated in the definition of OrderedRing