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

@@ -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}'"

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

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

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