feat: have IR checker suggest noncomputable

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 :=

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