From 3d9e587862c2f565a5b50e8b28dfcfbb13997be3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Mar 2022 09:28:02 -0700
Subject: [PATCH] fix: check type mismatch at dependent pattern matching
 compiler

see issue #1057
---
 src/Lean/Meta/Match/Match.lean    | 8 +++++++-
 tests/lean/1057.lean              | 9 +++++++++
 tests/lean/1057.lean.expected.out | 4 ++++
 3 files changed, 20 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/1057.lean
 create mode 100644 tests/lean/1057.lean.expected.out

diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index f789d81254..4813dddca4 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -51,7 +51,13 @@ where
         loop lhss alts minors
 
 def assignGoalOf (p : Problem) (e : Expr) : MetaM Unit :=
-  withGoalOf p (assignExprMVar p.mvarId e)
+  withGoalOf p do
+    let mvar := mkMVar p.mvarId
+    let mvarType ← inferType mvar
+    let eType ← inferType e
+    unless (← isDefEq mvarType eType) do
+      throwError "dependent elimination failed, type mismatch when solving alternative with type{indentExpr eType}\nbut expected{indentExpr mvarType}"
+    assignExprMVar p.mvarId e
 
 structure State where
   used            : Std.HashSet Nat := {} -- used alternatives
diff --git a/tests/lean/1057.lean b/tests/lean/1057.lean
new file mode 100644
index 0000000000..790677c096
--- /dev/null
+++ b/tests/lean/1057.lean
@@ -0,0 +1,9 @@
+inductive T
+  | t : T
+
+@[reducible] def T.eval : T → Type
+  | T.t => Int
+
+def T.default (τ : T) : τ.eval :=
+  match τ, τ.eval with
+  | T.t, .(Int) => (0 : Int)
diff --git a/tests/lean/1057.lean.expected.out b/tests/lean/1057.lean.expected.out
new file mode 100644
index 0000000000..b74edcc4d2
--- /dev/null
+++ b/tests/lean/1057.lean.expected.out
@@ -0,0 +1,4 @@
+1057.lean:8:2-9:28: error: dependent elimination failed, type mismatch when solving alternative with type
+  motive t Int
+but expected
+  motive t x✝