From dc87bef04c3de796f649c60baaeba7563c708d10 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 11 Mar 2021 12:16:15 -0800
Subject: [PATCH] fix: error message

This is a fix for bug reported by @JasonGross at Zulip
---
 src/Lean/Elab/StructInst.lean               | 12 ++++++------
 tests/lean/structSorryBug.lean              |  3 +++
 tests/lean/structSorryBug.lean.expected.out |  3 +++
 3 files changed, 12 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/structSorryBug.lean
 create mode 100644 tests/lean/structSorryBug.lean.expected.out

diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 135984fa9a..e52eb02dc8 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -147,16 +147,16 @@ private def elabModifyOp (stx modifyOp source : Syntax) (expectedType? : Option
     cont val
 
 /- Get structure name and elaborate explicit source (if available) -/
-private def getStructName (stx : Syntax) (expectedType? : Option Expr) (sourceView : Source) : TermElabM Name := do
+private def getStructName (stx : Syntax) (expectedType? : Option Expr) (sourceView : Source) : TermElabM (Name × Expr) := do
   tryPostponeIfNoneOrMVar expectedType?
-  let useSource : Unit → TermElabM Name := fun _ =>
+  let useSource : Unit → TermElabM (Name × Expr) := fun _ =>
     match sourceView, expectedType? with
     | Source.explicit _ src, _ => do
       let srcType ← inferType src
       let srcType ← whnf srcType
       tryPostponeIfMVar srcType
       match srcType.getAppFn with
-      | Expr.const constName _ _ => pure constName
+      | Expr.const constName _ _ => return (constName, srcType)
       | _ => throwUnexpectedExpectedType srcType "source"
     | _, some expectedType => throwUnexpectedExpectedType expectedType
     | _, none              => throwUnknownExpectedType
@@ -165,7 +165,7 @@ private def getStructName (stx : Syntax) (expectedType? : Option Expr) (sourceVi
   | some expectedType =>
     let expectedType ← whnf expectedType
     match expectedType.getAppFn with
-    | Expr.const constName _ _ => pure constName
+    | Expr.const constName _ _ => return (constName, expectedType)
     | _                        => useSource ()
 where
   throwUnknownExpectedType :=
@@ -782,9 +782,9 @@ def propagate (struct : Struct) : TermElabM Unit :=
 end DefaultFields
 
 private def elabStructInstAux (stx : Syntax) (expectedType? : Option Expr) (source : Source) : TermElabM Expr := do
-  let structName ← getStructName stx expectedType? source
+  let (structName, structType) ← getStructName stx expectedType? source
   unless isStructureLike (← getEnv) structName do
-    throwError "invalid \{...} notation, '{structName}' is not a structure"
+    throwError "invalid \{...} notation, structure type expected{indentExpr structType}"
   match mkStructView stx structName source with
   | Except.error ex  => throwError ex
   | Except.ok struct =>
diff --git a/tests/lean/structSorryBug.lean b/tests/lean/structSorryBug.lean
new file mode 100644
index 0000000000..a1113dbcae
--- /dev/null
+++ b/tests/lean/structSorryBug.lean
@@ -0,0 +1,3 @@
+instance has_arr : HasArr Preorder := { Arr := Function }
+
+def foo : Nat := { first := 10 }
diff --git a/tests/lean/structSorryBug.lean.expected.out b/tests/lean/structSorryBug.lean.expected.out
new file mode 100644
index 0000000000..efdd6c80b2
--- /dev/null
+++ b/tests/lean/structSorryBug.lean.expected.out
@@ -0,0 +1,3 @@
+structSorryBug.lean:1:19-1:25: error: unknown identifier 'HasArr'
+structSorryBug.lean:3:17-3:32: error: invalid {...} notation, structure type expected
+  Nat