IR check failed when should be noncomputable

Stream: lean4

[Alex J. Best]

I'm hitting the following IR check failed, unknown declaration on a mathematical project.
Here is a mathlib independent repro:
In the example I believe def bug should be marked noncomputable, but the IR generator doesn't pick up on this for some reason.

namespace WellFounded

variable {α : Sort u} {C : α → Sort v} {r : α → α → Prop}

unsafe def fix'.impl (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
  F x fun y _ => impl hwf F y

@[implemented_by fix'.impl]
def fix' (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x := hwf.fix F x

end WellFounded


namespace Nat

theorem lt_or_eq_of_le {a b : Nat} : a ≤ b → a < b ∨ a = b := sorry
section find
variable (p : Nat → Prop)

private def lbp (m n : Nat) : Prop := m = n + 1 ∧ ∀ k, k ≤ n → ¬p k

variable [DecidablePred p] (H : ∃ n, p n)

private def wf_lbp : WellFounded (lbp p) := by
  refine ⟨let ⟨n, pn⟩ := H; ?_⟩
  suffices ∀ m k, n ≤ k + m → Acc (lbp p) k from fun a => this _ _ (Nat.le_add_left _ _)
  intro m
  induction m with refine fun k kn => ⟨_, fun | _, ⟨rfl, a⟩ => ?_⟩
  | zero => exact absurd pn (a _ kn)
  | succ m IH => exact IH _ (by rw [Nat.add_right_comm]; exact kn)

protected def find_x : {n // p n ∧ ∀ m, m < n → ¬p m} :=
(wf_lbp p H).fix' (C := fun k => (∀n, n < k → ¬p n) → {n // p n ∧ ∀ m, m < n → ¬p m})
  (fun m IH al => if pm : p m then ⟨m, pm, al⟩ else
      have this : ∀ n, n ≤ m → ¬p n := fun n h =>
        (lt_or_eq_of_le h).elim (al n) fun e => by rw [e]; exact pm
      IH _ ⟨rfl, this⟩ fun n h => this n $ Nat.le_of_succ_le_succ h)
  0 fun n h => absurd h (Nat.not_lt_zero _)

protected def find : Nat := (Nat.find_x p H).1
end find
end Nat

variable (R : Type) [∀ n, OfNat R n]

open Classical

noncomputable
def char : Nat := Nat.find (fun n => (1 : R) = 1) ⟨1, rfl⟩

def bug : R := -- IR check failed at 'bug._rarg', error: unknown declaration 'char'
  match char R with
  | 0 => 1
  | _ => 0

[Leonardo de Moura]

We are currently working on a new code generator for Lean 4. We will address this issue there.
Could you please create a GitHub issue?

[Kevin Buzzard]

For what it's worth: in lean 3 it was also possible to confuse lean about whether something was computable or not. You could write inductive types where lean would complain however you tagged them. Gabriel fixed this with noncomputable! (which was very helpful in mathlib because beyond some point in algebra pretty much everything is noncomputable)

[Kyle Miller]

@Kevin Buzzard My understanding is that the Lean 4 system for noncomputability checking is completely different, where the code generator tries to compile a definition and if it fails the definition is marked noncomputable. In Lean 3, there's a separate system (the "noncomputability checker") that tries to predict exactly whether or not the VM compiler will succeed, and our addition of noncomputable! to Lean 3 is to override this check when this system is inaccurate (or when the it's a theoretical definition that we do not care to compile and the VM compiler will happily spend an hour compiling it). While the "right" solution is to fix this system in Lean 3, this isn't time well spent at the moment.

[Alex J. Best]

This is now #1785

[Kevin Buzzard]

Is that lean4#1785 ?