IR check failed in presence of noncomputable

[alexjbest]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Code generator sometimes doesn't correctly flag noncomputaility

Steps to Reproduce

In this (somewhat) minimal 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

Expected behavior: message saying def bug must be marked noncomputable

Actual behavior: IR check failed

Reproduces how often: 100% but seems to need a fairly complicated example

Versions

nightly-10-25

[digama0]

minimized:

noncomputable def char (x : α) : Bool := true
def bug (x : α) : Bool := not (char x)
-- IR check failed at 'bug._rarg', error: unknown declaration 'char'

[leodemoura]

@digama0 Thanks for minimizing the problem. The minimized version makes it clear what the issue is.

@alexjbest We will improve the error message and make it clear code generation failed because char is marked as noncomputable.

[alexjbest]

Thanks, and sorry for being so bad at minimizing! All modifications I tried gave the correct error message, so I assumed this problem was somehow more complicated than it appears to actually be :)

[kim-em]

Here's another example of the same issue, discovered on zulip. (Original by @kbuzzard, minimized by @digama0.)

class More (R : Type) extends Mul R, Add R

def Foo (R : Type) [Sub R] := R

noncomputable instance bar {R} [Sub R] : More (Foo R) := sorry

instance foo {R} [Sub R] : Add (Foo R) := inferInstance
-- compiler IR check failed at 'foo._rarg', error: unknown declaration 'bar'

[BoltonBailey]

Here are two more examples from Zulip.

[kbuzzard]

Here's another one.

[LibertasSpZ]

Yet another example is here. (And indeed a new-user papercut :) )

[kbuzzard]

Here's another. The user initially asked completely the wrong question, led astray by error: unknown declaration 'CategoryTheory.Limits.pullback after the IR message, when the declaration was known.

[kbuzzard]

Here's another. "This is giving weird errors, I'm not sure what's the problem here."

[sgraf812]

Here is another rather small example:

axiom Later : Type → Type
axiom gfix {α : Type} (f : Later α → α) : Later α
def gfix2 {α : Type} (f : Later α → α) : α := f (gfix f)

It certainly triggers a related error message (4.10-rc2):

compiler IR check failed at 'IGDTT.gfix2._rarg', error: unknown declaration 'IGDTT.gfix'

It took me a bit, but of course the error is that gfix indeed has no code and thus I shall add noncomputable to the definitions that use it.

[kbuzzard]

Two people caught out by this in one day today: here's the other one.