chore: improve error message when compiling code containing axioms or noncomputable definitions

closes #496

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

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");
         }
     }
 

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

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