Maximum recursion depth using explicit `UInt64`s inside type

Stream: lean4

[Geoffrey Irving]

I've done a bunch of reduction of this infinite loop example, though I expect it is reducible further. I'd like the bad lemma to work as well as the good lemma does, but instead it hits a maxRecDepth error:

import Mathlib.Data.Real.Basic
import Mathlib.Data.UInt

open scoped Real

structure Int64 where
  n : UInt64
  deriving DecidableEq

instance : Neg Int64 where neg x := ⟨-x.n⟩
instance {n : ℕ} : OfNat Int64 n where ofNat := ⟨n⟩

variable {s t : Int64}

structure Fixed (s : Int64) where
  n : Int64
  deriving DecidableEq

instance : Sub (Fixed s) where sub x y := bif x == y then y else x

def Fixed.ofNat (n : ℕ) : Fixed s :=
  let k := n >>> s.n.toNat
  bif k == 0 then ⟨sorry⟩ else ⟨0⟩

structure Interval (s : Int64) where
  lo : Fixed s
  hi : Fixed s

def Interval.approx (x : Interval s) : Set ℝ := if x.lo = x.hi then Set.univ else sorry

instance : Sub (Interval s) where
  sub x y := ⟨x.lo - y.hi, sorry⟩

lemma subset_approx_sub {a : Set ℝ} {x y : Interval s} : a ⊆ (x - y).approx := sorry

def Interval.ofNat (n : ℕ) : Interval s := ⟨.ofNat n, .ofNat n⟩

instance : One (Interval s) := ⟨.ofNat 1⟩

def mul (x : Fixed s) (y : Fixed t) (u : Int64) : Interval u := sorry

lemma good {x : Fixed s} (c : Fixed t) : {1} ⊆ (1 - mul x c t).approx := by
  -- This one works, presumably because `t` is abstract rather than being `-61`
  apply subset_approx_sub
  repeat sorry

lemma bad {x : Fixed s} (c : Fixed (-61)) : {1} ⊆ (1 - mul x c (-61)).approx := by
  -- maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)
  apply subset_approx_sub
  sorry

Any ideas what might be going wrong?

[Eric Wieser]

refine subset_approx_sub (b := ?_) seems to work

[Eric Wieser]

Are you sure b is supposed to be there? It's not used in the statement in any way

[Geoffrey Irving]

b was residue from minimization. I think I removed it locally (and kept the apply) and the problem remains, but unfortunately I have to run an errand so more later.

[Geoffrey Irving]

Confirmed that refine fixes it. But even after b is gone (fixed above), apply still fails. I'm curious to know why, in order to solve my original non-minimized problem.

[Eric Wieser]

Does refine succeed in your original example?

[Geoffrey Irving]

Yes. However, manually using refine is a poor solution in the original case, as mono seems to do apply and has the same problem. I'd like to use mono to do a bunch of relevant applies in a row.

[Geoffrey Irving]

What does fix it in the original problem for both apply and mono, and in the reduced one, is marking Interval.ofNat as @[irreducible]. So I think I'm set, as that seems like a reasonable fix.