chore: improve error message

closes #276

src/Lean/AuxRecursor.lean

@@ -7,15 +7,30 @@ import Lean.Environment
 
 namespace Lean
 
+def casesOnSuffix       := "casesOn"
+def recOnSuffix         := "recOn"
+def brecOnSuffix        := "brecOn"
+def binductionOnSuffix  := "binductionOn"
+
+def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix
+def mkRecOnName (indDeclName : Name) : Name   := Name.mkStr indDeclName recOnSuffix
+def mkBRecOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName brecOnSuffix
+def mkBInductionOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName binductionOnSuffix
+
 builtin_initialize auxRecExt : TagDeclarationExtension ← mkTagDeclarationExtension `auxRec
 
 @[export lean_mark_aux_recursor]
-def markAuxRecursor (env : Environment) (n : Name) : Environment :=
-  auxRecExt.tag env n
+def markAuxRecursor (env : Environment) (declName : Name) : Environment :=
+  auxRecExt.tag env declName
 
 @[export lean_is_aux_recursor]
-def isAuxRecursor (env : Environment) (n : Name) : Bool :=
-  auxRecExt.isTagged env n
+def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
+  auxRecExt.isTagged env declName
+
+def isCasesOnRecursor (env : Environment) (declName : Name) : Bool :=
+  match declName with 
+  | Name.str _ s _ => s == casesOnSuffix && isAuxRecursor env declName
+  | _ => false
 
 builtin_initialize noConfusionExt : TagDeclarationExtension ← mkTagDeclarationExtension `noConf
 

src/Lean/Meta/RecursorInfo.lean

@@ -9,16 +9,6 @@ import Lean.Meta.ExprDefEq
 
 namespace Lean.Meta
 
-def casesOnSuffix       := "casesOn"
-def recOnSuffix         := "recOn"
-def brecOnSuffix        := "brecOn"
-def binductionOnSuffix  := "binductionOn"
-
-def mkCasesOnName (indDeclName : Name) : Name := Name.mkStr indDeclName casesOnSuffix
-def mkRecOnName (indDeclName : Name) : Name   := Name.mkStr indDeclName recOnSuffix
-def mkBRecOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName brecOnSuffix
-def mkBInductionOnName (indDeclName : Name) : Name  := Name.mkStr indDeclName binductionOnSuffix
-
 inductive RecursorUnivLevelPos where
   | motive                -- marks where the universe of the motive should go
   | majorType (idx : Nat) -- marks where the #idx universe of the major premise type goes

src/Lean/MonadEnv.lean

@@ -5,6 +5,9 @@ Authors: Leonardo de Moura
 -/
 import Lean.Environment
 import Lean.Exception
+import Lean.Declaration
+import Lean.Util.FindExpr
+import Lean.AuxRecursor
 
 namespace Lean
 
@@ -16,11 +19,14 @@ def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
   | some (ConstantInfo.inductInfo ..) => return true
   | _ => return false
 
-def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
-  match (← getEnv).find? declName with
+def isRecCore (env : Environment) (declName : Name) : Bool :=
+  match env.find? declName with
   | some (ConstantInfo.recInfo ..) => return true
   | _ => return false
 
+def isRec [Monad m] [MonadEnv m] (declName : Name) : m Bool := 
+  return isRecCore (← getEnv) declName
+  
 @[inline] def withoutModifyingEnv [Monad m] [MonadEnv m] [MonadFinally m] {α : Type} (x : m α) : m α := do
   let env ← getEnv
   try x finally setEnv env
@@ -99,10 +105,27 @@ def addDecl [Monad m] [MonadEnv m] [MonadError m] [MonadOptions m] (decl : Decla
   | Except.ok    env => setEnv env
   | Except.error ex  => throwKernelException ex
 
+private def supportedRecursors := 
+  #[``Empty.rec, ``False.rec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]
+
+private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Declaration) : m Unit := do
+  let env ← getEnv 
+  decl.forExprM fun e =>
+    let unsupportedRecursor? := e.find? fun 
+      | Expr.const declName .. => 
+        ((isAuxRecursor env declName && !isCasesOnRecursor env declName) || isRecCore env declName)
+        && !supportedRecursors.contains declName
+      | _ => false
+    match unsupportedRecursor? with 
+    | some (Expr.const declName ..) => throwError! "code generator does not support recursor '{declName}' yet, consider using 'match ... with' and/or structural recursion"
+    | _ => pure ()
+
 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 ex => throwKernelException ex
+  | 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
   addDecl decl;

tests/lean/276.lean

@@ -0,0 +1,13 @@
+universes u v
+
+-- `Type u` version can be defined without this option, but I get the same error
+set_option bootstrap.inductiveCheckResultingUniverse false in
+inductive PEmpty : Sort u
+
+-- `#check` works
+set_option pp.all true in
+#check fun {α : Sort v} => PEmpty.rec (fun _ => α)
+
+-- but `def` doesn't work
+-- error: (kernel) compiler failed to infer low level type, unknown declaration 'PEmpty.rec'
+def PEmpty.elim {α : Sort v} := PEmpty.rec (fun _ => α)

tests/lean/276.lean.expected.out

@@ -0,0 +1,2 @@
+fun {α} => PEmpty.rec.{v, u_1} fun x => α : {α : Sort v} → PEmpty.{u_1} → α
+276.lean:13:4-13:8: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion