From 349901689510d8ff1daeb5af8cec80c15733a1bd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 31 May 2021 20:24:53 -0700
Subject: [PATCH] chore: improve error message when compiling code containing
 axioms or noncomputable definitions

closes #496
---
 src/Lean/MonadEnv.lean                 | 6 +++++-
 src/library/compiler/ll_infer_type.cpp | 2 +-
 tests/lean/496.lean                    | 9 +++++++++
 tests/lean/496.lean.expected.out       | 2 ++
 4 files changed, 17 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/496.lean
 create mode 100644 tests/lean/496.lean.expected.out

diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
index c727074d64..a6170d685d 100644
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -122,6 +122,8 @@ def addDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Decla
 private def supportedRecursors :=
   #[``Empty.rec, ``False.rec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
 
+/- This is a temporary workaround for generating better error messages for the compiler. It can be deleted after we
+   rewrite the remaining parts of the compiler in Lean.  -/
 private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Declaration) : m Unit := do
   let env ← getEnv
   decl.forExprM fun e =>
@@ -137,8 +139,10 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla
 def compileDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Declaration) : m Unit := do
   match (← getEnv).compileDecl (← getOptions) decl with
   | Except.ok env   => setEnv env
+  | Except.error (KernelException.other msg) =>
+    checkUnsupported decl -- Generate nicer error message for unsupported recursors and axioms
+    throwError msg
   | Except.error ex =>
-    checkUnsupported decl -- Generate nicer error message for unsupported recursors
     throwKernelException ex
 
 def addAndCompile [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Declaration) : m Unit := do
diff --git a/src/library/compiler/ll_infer_type.cpp b/src/library/compiler/ll_infer_type.cpp
index 9fa58c1496..71e1202732 100644
--- a/src/library/compiler/ll_infer_type.cpp
+++ b/src/library/compiler/ll_infer_type.cpp
@@ -199,7 +199,7 @@ class ll_infer_type_fn {
                 }
                 return *g_bot;
             }
-            throw exception(sstream() << "compiler failed to infer low level type, unknown declaration '" << const_name(e) << "'");
+            throw exception(sstream() << "failed to compile definition, consider marking it as 'noncomputable' because it depends on '" << const_name(e) << "', and it does not have executable code");
         }
     }
 
diff --git a/tests/lean/496.lean b/tests/lean/496.lean
new file mode 100644
index 0000000000..a4455b4898
--- /dev/null
+++ b/tests/lean/496.lean
@@ -0,0 +1,9 @@
+axiom F : Type
+axiom foo : F
+def foo' : F := foo
+
+axiom bla : Nat
+
+noncomputable def bla1 : Nat := id bla
+
+def bla2 := id bla1
diff --git a/tests/lean/496.lean.expected.out b/tests/lean/496.lean.expected.out
new file mode 100644
index 0000000000..56c6f4c5fb
--- /dev/null
+++ b/tests/lean/496.lean.expected.out
@@ -0,0 +1,2 @@
+496.lean:3:4-3:8: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'foo', and it does not have executable code
+496.lean:9:4-9:8: error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'bla1', and it does not have executable code