From 490d16c80d7bdf96a43345d9b307c21d8fbb6a16 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 17 Jul 2024 13:48:03 -0700
Subject: [PATCH] fix: have elabAsElim check inferred motive for type
 correctness (#4722)

Declarations with `@[elab_as_elim]` could elaborate as type-incorrect
expressions. Reported by Jireh Loreaux [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/bug.20in.20revert/near/450522157).

(In principle the elabAsElim routine could revert fvars appearing in the
expected type that depend on the discriminants (if the discriminants are
fvars) to increase the likelihood of type correctness, but that's at the
cost of some complexity to both the elaborator and to the user.)
---
 src/Lean/Elab/App.lean                  | 5 ++++-
 tests/lean/elabAsElim.lean              | 9 +++++++++
 tests/lean/elabAsElim.lean.expected.out | 5 +++++
 3 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 43b5c9f09e..8be94e99eb 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -742,7 +742,10 @@ def mkMotive (discrs : Array Expr) (expectedType : Expr): MetaM Expr := do
     let motiveBody ← kabstract motive discr
     /- We use `transform (usedLetOnly := true)` to eliminate unnecessary let-expressions. -/
     let discrType ← transform (usedLetOnly := true) (← instantiateMVars (← inferType discr))
-    return Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
+    let motive := Lean.mkLambda (← mkFreshBinderName) BinderInfo.default discrType motiveBody
+    unless (← isTypeCorrect motive) do
+      throwError "failed to elaborate eliminator, motive is not type correct:{indentD motive}"
+    return motive
 
 /-- If the eliminator is over-applied, we "revert" the extra arguments. -/
 def revertArgs (args : List Arg) (f : Expr) (expectedType : Expr) : TermElabM (Expr × Expr) :=
diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean
index 1b1352bd97..da254e3a58 100644
--- a/tests/lean/elabAsElim.lean
+++ b/tests/lean/elabAsElim.lean
@@ -87,3 +87,12 @@ noncomputable def f : Nat → Nat :=
 
 example : ∀ x, x ≥ 0 :=
   Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
+
+@[elab_as_elim]
+def Foo.induction {P : (α : Type) → Prop} (α : Type) : P α := sorry
+
+example {n : Type} {T : n} : T = T := Foo.induction n -- motive is not type correct
+
+example {n : Type} : {T : n} → T = T := Foo.induction n -- motive is not type correct
+
+example {n : Type} : {T : n} → T = T := @(Foo.induction n)
diff --git a/tests/lean/elabAsElim.lean.expected.out b/tests/lean/elabAsElim.lean.expected.out
index 6df215ff45..07450ee119 100644
--- a/tests/lean/elabAsElim.lean.expected.out
+++ b/tests/lean/elabAsElim.lean.expected.out
@@ -1,3 +1,8 @@
 elabAsElim.lean:9:2-9:14: error: failed to elaborate eliminator, insufficient number of arguments, expected type:
   Nat
 elabAsElim.lean:26:2-26:24: error: failed to elaborate eliminator, unused named arguments: [a]
+elabAsElim.lean:92:4-92:17: warning: declaration uses 'sorry'
+elabAsElim.lean:94:38-94:53: error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T = T
+elabAsElim.lean:96:40-96:55: error: failed to elaborate eliminator, motive is not type correct:
+  fun x => T✝ = T✝