fix: make elabAsElim aware of explicit motive arguments (#4817)

Some eliminators (such as `False.rec`) have an explicit motive argument.
The `elabAsElim` elaborator assumed that all motives are implicit.

If the explicit motive argument is `_`, then it uses the elab-as-elim
procedure, and otherwise it falls back to the standard app elaborator.

Furthermore, if an explicit elaborator is not provided, it falls back to
treating the elaborator as being implicit, which is convenient for
writing `h.rec` rather than `h.rec _`. Rationale: for `False.rec`, this
simulates it having an implicit motive, and also motives are generally
not going to be available in the expected type.

Closes #4347

src/Lean/Elab/App.lean

@@ -743,7 +743,7 @@ structure State where
 abbrev M := ReaderT Context $ StateRefT State TermElabM
 
 /-- Infer the `motive` using the expected type by `kabstract`ing the discriminants. -/
-def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
+def mkMotive (discrs : Array Expr) (expectedType : Expr) : MetaM Expr := do
   discrs.foldrM (init := expectedType) fun discr motive => do
     let discr ← instantiateMVars discr
     let motiveBody ← kabstract motive discr
@@ -878,7 +878,16 @@ partial def main : M Expr := do
     main
   let idx := (← get).idx
   if (← read).elimInfo.motivePos == idx then
-    let motive ← mkImplicitArg binderType binderInfo
+    let motive ←
+      match (← getNextArg? binderName binderInfo) with
+      | .some arg =>
+        /- Due to `Lean.Elab.Term.elabAppArgs.elabAsElim?`, this must be a positional argument that is the syntax `_`. -/
+        elabArg arg binderType
+      | .none | .undef =>
+        /- Note: undef occurs when the motive is explicit but missing.
+           In this case, we treat it as if it were an implicit argument
+           to support writing `h.rec` when `h : False`, rather than requiring `h.rec _`. -/
+        mkImplicitArg binderType binderInfo
     setMotive motive
     addArgAndContinue motive
   else if let some tidx := (← read).elimInfo.targetsPos.indexOf? idx then
@@ -970,15 +979,34 @@ where
     unless (← shouldElabAsElim declName) do return none
     let elimInfo ← getElimInfo declName
     forallTelescopeReducing (← inferType f) fun xs _ => do
-      if h : elimInfo.motivePos < xs.size then
-        let x := xs[elimInfo.motivePos]
+      /- Process arguments similar to `Lean.Elab.Term.ElabElim.main` to see if the motive has been
+         provided, in which case we use the standard app elaborator.
+         If the motive is explicit (like for `False.rec`), then a positional `_` counts as "not provided". -/
+      let mut args := args.toList
+      let mut namedArgs := namedArgs.toList
+      for x in xs[0:elimInfo.motivePos] do
         let localDecl ← x.fvarId!.getDecl
-        if findBinderName? namedArgs.toList localDecl.userName matches some _ then
+        match findBinderName? namedArgs localDecl.userName with
+        | some _ => namedArgs := eraseNamedArg namedArgs localDecl.userName
+        | none   => if localDecl.binderInfo.isExplicit then args := args.tailD []
+      -- Invariant: `elimInfo.motivePos < xs.size` due to construction of `elimInfo`.
+      let some x := xs[elimInfo.motivePos]? | unreachable!
+      let localDecl ← x.fvarId!.getDecl
+      if findBinderName? namedArgs localDecl.userName matches some _ then
+        -- motive has been explicitly provided, so we should use standard app elaborator
+        return none
+      else
+        match localDecl.binderInfo.isExplicit, args with
+        | true, .expr _ :: _  =>
           -- motive has been explicitly provided, so we should use standard app elaborator
           return none
-        return some elimInfo
-      else
-        return none
+        | true, .stx arg :: _ =>
+          if arg.isOfKind ``Lean.Parser.Term.hole then
+            return some elimInfo
+          else
+            -- positional motive is not `_`, so we should use standard app elaborator
+            return none
+        | _, _ => return some elimInfo
 
   /--
   Collect extra argument positions that must be elaborated eagerly when using `elab_as_elim`.

tests/lean/276.lean

@@ -5,5 +5,5 @@ 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'
+-- error: code generator does not support recursor 'PEmpty.rec' yet
 def PEmpty.elim' {α : Sort v} := PEmpty.rec (fun _ => α)

tests/lean/276.lean.expected.out

@@ -1,3 +1,2 @@
-276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available
-fun {α : Sort v} => @?m α : {α : Sort v} → @?m α
-276.lean:9:33-9:56: error: failed to elaborate eliminator, expected type is not available
+fun {α : Sort v} => PEmpty.rec.{v, u_1} fun (x : PEmpty.{u_1}) => α : {α : Sort v} → PEmpty.{u_1} → α
+276.lean:9:4-9:16: error: code generator does not support recursor 'PEmpty.rec' yet, consider using 'match ... with' and/or structural recursion

tests/lean/run/elabAsElim.lean

@@ -175,3 +175,14 @@ def leRecOn {C : Nat → Sort _} {n : Nat} : ∀ {m}, n ≤ m → (∀ {k}, C k
 theorem leRecOn_self {C : Nat → Sort _} {n} {next : ∀ {k}, C k → C (k + 1)} (x : C n) :
     (leRecOn n.le_refl next x : C n) = x :=
   sorry
+
+/-!
+Issue https://github.com/leanprover/lean4/issues/4347
+
+`False.rec` has `motive` as an explicit argument.
+-/
+
+example (h : False) : Nat := False.rec (fun _ => Nat) h
+example (h : False) : Nat := False.rec _ h
+example (h : False) : Nat := h.rec
+example (h : False) : Nat := h.rec _

tests/lean/run/emptyLcnf.lean

@@ -3,7 +3,7 @@ import Lean
 inductive MyEmpty
 
 def f (x : MyEmpty) : Nat :=
-  MyEmpty.casesOn x
+  MyEmpty.casesOn _ x
 
 set_option trace.Compiler.result true
 /--