Smart unfolding produces ununfoldable terms

Stream: lean4

[Mario Carneiro]

It appears that smart unfolding can put the idRhs quite deep in the term, in particular behind a if, which can cause the term to be blocked for unfolding in a generic context:

def foo (i j : Nat) : Nat :=
  if i < 5 then 0 else
  match j with
  | Nat.zero => 1
  | Nat.succ j => foo i j

#print foo._sunfold
-- def foo._sunfold : Nat → Nat → Nat :=
-- fun (i j : Nat) =>
--   if i < 5 then 0 else
--     match j with
--     | Nat.zero => idRhs Nat 1
--     | Nat.succ j => idRhs Nat (foo i j)

example (h : i < 5) : foo i j = 0 := by
  simp [foo, h] -- fails to unfold foo

[Mario Carneiro]

In fact, there is no delta or dsimp or dunfold or unfold tactic to use instead, and the elaborator outright rejects a straight unfolding of this definition by rfl:

theorem foo_eq : foo = fun (i j : Nat) =>
  @Nat.brecOn.{1} (fun (j : Nat) => Nat) j
    fun (j : Nat) (f : @Nat.below.{1} (fun (j : Nat) => Nat) j) =>
      @ite.{1} Nat (@HasLess.Less.{0} Nat instHasLessNat i (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5)))
        (Nat.decLt i (@OfNat.ofNat.{0} Nat 5 (instOfNatNat 5))) (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))
        (foo.match_1.{1} (fun (j : Nat) => @Nat.below.{1} (fun (j : Nat) => Nat) j → Nat) j
          (fun (a : Unit) (x : @Nat.below.{1} (fun (j : Nat) => Nat) Nat.zero) =>
            @OfNat.ofNat.{0} Nat 1 (instOfNatNat 1))
          (fun (j : Nat) (x : @Nat.below.{1} (fun (j : Nat) => Nat) (Nat.succ j)) =>
            @PProd.fst.{1, 1} ((fun (j : Nat) => Nat) j)
              (@Nat.rec.{2} (fun (t : Nat) => Type) PUnit.{1}
                (fun (n : Nat) (v_0 : Type) => PProd.{1, 1} (PProd.{1, 1} ((fun (j : Nat) => Nat) n) v_0) PUnit.{1}) j)
              (@PProd.fst.{1, 1}
                (PProd.{1, 1} ((fun (j : Nat) => Nat) j)
                  (@Nat.rec.{2} (fun (t : Nat) => Type) PUnit.{1}
                    (fun (n : Nat) (v_0 : Type) => PProd.{1, 1} (PProd.{1, 1} ((fun (j : Nat) => Nat) n) v_0) PUnit.{1})
                    j))
                PUnit.{1} x))
          f) := rfl -- failed