From c302840c7f7a45c68326174741e39acd3131ea88 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Sat, 7 Sep 2024 15:00:21 -0700
Subject: [PATCH] feat: have IR checker suggest `noncomputable` (#4729)

Currently, `ll_infer_type` is responsible for telling the user about
`noncomputable` when a definition depends on one without executable
code. However, this is imperfect because type inference does not check
every subexpression. This leads to errors later on that users find to be
hard to interpret.

Now, `Lean.IR.checkDecls` has a friendlier error message when it
encounters constants without compiled definitions, suggesting to
consider using `noncomputable`. While this function is an internal IR
consistency check, it is also reasonable to have it give an informative
error message in this particular case. The suggestion to use
`noncomputable` is limited to just unknown constants.

Some alternatives would be to either (1) create another checker just for
missing constants, (2) change `ll_infer_type` to always visit every
subexpression no matter if they are necessary for inferring the type, or
(3) investigate whether `tests/lean/run/1785.lean` is due to a deeper
issue.

Closes #1785
---
 src/Lean/Compiler/IR/Checker.lean |  4 ++--
 tests/lean/run/1785.lean          | 21 +++++++++++++++++++++
 2 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1785.lean

diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index c4e7257e1647a..2f6f785997471 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -50,7 +50,7 @@ def markJP (j : JoinPointId) : M Unit :=
 def getDecl (c : Name) : M Decl := do
   let ctx ← read
   match findEnvDecl' ctx.env c ctx.decls with
-  | none   => throw s!"unknown declaration '{c}'"
+  | none   => throw s!"depends on declaration '{c}', which has no executable code; consider marking definition as 'noncomputable'"
   | some d => pure d
 
 def checkVar (x : VarId) : M Unit := do
@@ -182,7 +182,7 @@ end Checker
 def checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit := do
   let env ← getEnv
   match (Checker.checkDecl decl { env := env, decls := decls }).run' {} with
-  | .error msg => throw s!"compiler IR check failed at '{decl.name}', error: {msg}"
+  | .error msg => throw s!"failed to compile definition, compiler IR check failed at '{decl.name}'. Error: {msg}"
   | _ => pure ()
 
 def checkDecls (decls : Array Decl) : CompilerM Unit :=
diff --git a/tests/lean/run/1785.lean b/tests/lean/run/1785.lean
new file mode 100644
index 0000000000000..2ac8143dd4303
--- /dev/null
+++ b/tests/lean/run/1785.lean
@@ -0,0 +1,21 @@
+/-!
+# Improve compiler IR check message for users when constants are not compiled
+-/
+
+/-
+This is a simplified version of the example in #1785.
+Note that the error changes if the typeclass argument is removed.
+-/
+
+noncomputable
+def char (R : Type) [∀ n, OfNat R n] : Nat := 0
+
+/--
+error: failed to compile definition, compiler IR check failed at 'bug._rarg'. Error: depends on
+declaration 'char', which has no executable code; consider marking definition as 'noncomputable'
+-/
+#guard_msgs in
+def bug (R : Type) [∀ n, OfNat R n] : R :=
+  match char R with
+  | 0 => 1
+  | _ => 0