From 7a79ef62d1ee7ff34ac3141eacbecb537ec62e28 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 5 Mar 2021 19:08:10 -0800
Subject: [PATCH] fix: bug at `hasSyntheticSorry`

It was missing a constructor, and not taking assigned metavariables
into account.

Fixes a problem reported by @JasonGross at Zulip
---
 src/Lean/Exception.lean                   |  2 +-
 src/Lean/Util/Sorry.lean                  | 22 +++++++++++++---------
 tests/lean/sorryAtError.lean              | 13 +++++++++++++
 tests/lean/sorryAtError.lean.expected.out |  8 ++++++++
 4 files changed, 35 insertions(+), 10 deletions(-)
 create mode 100644 tests/lean/sorryAtError.lean
 create mode 100644 tests/lean/sorryAtError.lean.expected.out

diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index c1c502420a..42736be1a1 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -47,7 +47,7 @@ section Methods
 def throwError [Monad m] [MonadError m] (msg : MessageData) : m α := do
   let ref ← getRef
   let (ref, msg) ← AddErrorMessageContext.add ref msg
-  throw $ Exception.error ref msg
+  throw <| Exception.error ref msg
 
 def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α :=
   throwError m!"unknown constant '{mkConst constName}'"
diff --git a/src/Lean/Util/Sorry.lean b/src/Lean/Util/Sorry.lean
index 9d858e88c0..57232f3b93 100644
--- a/src/Lean/Util/Sorry.lean
+++ b/src/Lean/Util/Sorry.lean
@@ -45,15 +45,19 @@ partial def MessageData.hasSorry : MessageData → Bool
   | MessageData.node msgs         => msgs.any hasSorry
   | _                             => false
 
-partial def MessageData.hasSyntheticSorry : MessageData → Bool
-  | MessageData.ofExpr e          => e.hasSyntheticSorry
-  | MessageData.withContext _ msg => msg.hasSyntheticSorry
-  | MessageData.nest _ msg        => msg.hasSyntheticSorry
-  | MessageData.group msg         => msg.hasSyntheticSorry
-  | MessageData.compose msg₁ msg₂ => msg₁.hasSyntheticSorry || msg₂.hasSyntheticSorry
-  | MessageData.tagged _ msg      => msg.hasSyntheticSorry
-  | MessageData.node msgs         => msgs.any hasSyntheticSorry
-  | _                             => false
+partial def MessageData.hasSyntheticSorry (msg : MessageData) : Bool :=
+  visit msg.instantiateMVars
+where
+  visit : MessageData → Bool
+  | MessageData.ofExpr e                => e.hasSyntheticSorry
+  | MessageData.withContext _ msg       => visit msg
+  | MessageData.withNamingContext _ msg => visit msg
+  | MessageData.nest _ msg              => visit msg
+  | MessageData.group msg               => visit msg
+  | MessageData.compose msg₁ msg₂       => visit msg₁ || visit msg₂
+  | MessageData.tagged _ msg            => visit msg
+  | MessageData.node msgs               => msgs.any hasSyntheticSorry
+  | _                                   => false
 
 def Exception.hasSyntheticSorry : Exception → Bool
   | Exception.error _ msg => msg.hasSyntheticSorry
diff --git a/tests/lean/sorryAtError.lean b/tests/lean/sorryAtError.lean
new file mode 100644
index 0000000000..bc7f1c1667
--- /dev/null
+++ b/tests/lean/sorryAtError.lean
@@ -0,0 +1,13 @@
+structure Ty where
+  ctx : Type
+  ty : ctx → Type
+structure Tm where
+  ty : Ty
+  tm : ∀ {Γ}, ty.ty Γ
+
+#check fun (Γ : Type)
+(A : Ty)
+(Actx : Γ = A.ctx)
+(x : Tm)
+(xTy : x.ty = A)
+=> Eq.rec (motive := fun ty _ => ∀ {Γ}, ty.ty Γ) (fun {Γ:x.ty.ctx} => x.tm (Γ:=Γ)) xTy
diff --git a/tests/lean/sorryAtError.lean.expected.out b/tests/lean/sorryAtError.lean.expected.out
new file mode 100644
index 0000000000..907412aa75
--- /dev/null
+++ b/tests/lean/sorryAtError.lean.expected.out
@@ -0,0 +1,8 @@
+sorryAtError.lean:13:40-13:47: error: application type mismatch
+  Ty.ty ty Γ
+argument
+  Γ
+has type
+  x.ty.ctx
+but is expected to have type
+  ty.ctx