chore: fix tests

closes #4365

src/Lean/Elab/App.lean

@@ -59,7 +59,7 @@ private def mkProjAndCheck (structName : Name) (idx : Nat) (e : Expr) : MetaM Ex
 def synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) : TermElabM Unit :=
   for mvarId in instMVars do
     unless (← synthesizeInstMVarCore mvarId) do
-      registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass
+      registerSyntheticMVarWithCurrRef mvarId (.typeClass none)
       registerMVarErrorImplicitArgInfo mvarId (← getRef) app
 
 /-- Return `some namedArg` if `namedArgs` contains an entry for `binderName`. -/

src/Lean/Elab/BuiltinTerm.lean

@@ -190,8 +190,18 @@ private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr :=
     | some val => pure val
     | none     => throwIllFormedSyntax
   let typeMVar ← mkFreshTypeMVarFor expectedType?
-  let u ← getDecLevel typeMVar
-  let mvar ← mkInstMVar (mkApp2 (Lean.mkConst ``OfNat [u]) typeMVar (mkRawNatLit val))
+  let u ← try
+    getDecLevel typeMVar
+  catch ex =>
+    match expectedType? with
+    | some expectedType =>
+      if (← isProp expectedType) then
+        throwError m!"numerals are data in Lean, but the expected type is a proposition{indentExpr expectedType} : Prop"
+      else
+        throwError m!"numerals are data in Lean, but the expected type is universe polymorphic and may be a proposition{indentExpr expectedType} : {← inferType expectedType}"
+    | none => throw ex
+  let extraMsg := m!"numerals are polymorphic in Lean, but the numeral `{val}` cannot be used in a context where the expected type is{indentExpr typeMVar}\ndue to the absence of the instance above"
+  let mvar ← mkInstMVar (mkApp2 (Lean.mkConst ``OfNat [u]) typeMVar (mkRawNatLit val)) extraMsg
   let r := mkApp3 (Lean.mkConst ``OfNat.ofNat [u]) typeMVar (mkRawNatLit val) mvar
   registerMVarErrorImplicitArgInfo mvar.mvarId! stx r
   return r

src/Lean/Elab/SyntheticMVars.lean

@@ -59,10 +59,10 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
 /--
   Similar to `synthesizeInstMVarCore`, but makes sure that `instMVar` local context and instances
   are used. It also logs any error message produced. -/
-private def synthesizePendingInstMVar (instMVar : MVarId) : TermElabM Bool :=
+private def synthesizePendingInstMVar (instMVar : MVarId) (extraErrorMsg? : Option MessageData := none): TermElabM Bool :=
   instMVar.withContext do
     try
-      synthesizeInstMVarCore instMVar
+      synthesizeInstMVarCore instMVar (extraErrorMsg? := extraErrorMsg?)
     catch
       | ex@(.error ..) => logException ex; return true
       | _              => unreachable!
@@ -180,7 +180,7 @@ private def synthesizeSomeUsingDefaultPrio (prio : Nat) : TermElabM Bool := do
     | mvarId :: pendingMVars =>
       let some mvarDecl ← getSyntheticMVarDecl? mvarId | visit pendingMVars (mvarId :: pendingMVarsNew)
       match mvarDecl.kind with
-      | .typeClass =>
+      | .typeClass .. => -- TODO: use `errorMsg?` in `typeClass`.
         if (← withRef mvarDecl.stx <| synthesizeUsingDefaultPrio mvarId prio) then
           modify fun s => { s with pendingMVars := pendingMVars.reverse ++ pendingMVarsNew }
           return true
@@ -211,12 +211,13 @@ def reportStuckSyntheticMVar (mvarId : MVarId) (ignoreStuckTC := false) : TermEl
   let some mvarSyntheticDecl ← getSyntheticMVarDecl? mvarId | return ()
   withRef mvarSyntheticDecl.stx do
     match mvarSyntheticDecl.kind with
-    | .typeClass =>
+    | .typeClass extraErrorMsg? =>
+      let extraErrorMsg := extraMsgToMsg extraErrorMsg?
       unless ignoreStuckTC do
          mvarId.withContext do
           let mvarDecl ← getMVarDecl mvarId
           unless (← MonadLog.hasErrors) do
-            throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}"
+            throwError "typeclass instance problem is stuck, it is often due to metavariables{indentExpr mvarDecl.type}{extraErrorMsg}"
     | .coe header expectedType e f? =>
       mvarId.withContext do
         throwTypeMismatchError header expectedType (← inferType e) e f?
@@ -365,7 +366,7 @@ mutual
     let some mvarSyntheticDecl ← getSyntheticMVarDecl? mvarId | return true -- The metavariable has already been synthesized
     withRef mvarSyntheticDecl.stx do
     match mvarSyntheticDecl.kind with
-    | .typeClass => synthesizePendingInstMVar mvarId
+    | .typeClass extraErrorMsg? => synthesizePendingInstMVar mvarId extraErrorMsg?
     | .coe _header? expectedType e _f? => mvarId.withContext do
       if (← withDefault do isDefEq (← inferType e) expectedType) then
         -- Types may be defeq now due to mvar assignments, type class

src/Lean/Elab/Term.lean

@@ -30,8 +30,12 @@ structure SavedContext where
 
 /-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
 inductive SyntheticMVarKind where
-  /-- Use typeclass resolution to synthesize value for metavariable. -/
-  | typeClass
+  /--
+  Use typeclass resolution to synthesize value for metavariable.
+  If `extraErrorMsg?` is `some msg`, `msg` contains additional information to include in error messages
+  regarding type class synthesis failure.
+  -/
+  | typeClass (extraErrorMsg? : Option MessageData)
   /-- Use coercion to synthesize value for the metavariable.
   if `f?` is `some f`, we produce an application type mismatch error message.
   Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)`
@@ -43,9 +47,15 @@ inductive SyntheticMVarKind where
   | postponed (ctx : SavedContext)
   deriving Inhabited
 
+/--
+Convert an "extra" optional error message into a message `"\n{msg}"` (if `some msg`) and `MessageData.nil` (if `none`)
+-/
+def extraMsgToMsg (extraErrorMsg? : Option MessageData) : MessageData :=
+  if let some msg := extraErrorMsg? then m!"\n{msg}" else .nil
+
 instance : ToString SyntheticMVarKind where
   toString
-    | .typeClass    => "typeclass"
+    | .typeClass .. => "typeclass"
     | .coe ..       => "coe"
     | .tactic ..    => "tactic"
     | .postponed .. => "postponed"
@@ -857,8 +867,12 @@ def containsPendingMVar (e : Expr) : MetaM Bool := do
   Return `true` if the instance was synthesized successfully, and `false` if
   the instance contains unassigned metavariables that are blocking the type class
   resolution procedure. Throw an exception if resolution or assignment irrevocably fails.
+
+  If `extraErrorMsg?` is not none, it contains additional information that should be attached
+  to type class synthesis failures.
 -/
-def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := none) : TermElabM Bool := do
+def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := none) (extraErrorMsg? : Option MessageData := none): TermElabM Bool := do
+  let extraErrorMsg := extraMsgToMsg extraErrorMsg?
   let instMVarDecl ← getMVarDecl instMVar
   let type := instMVarDecl.type
   let type ← instantiateMVars type
@@ -891,18 +905,18 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
         let oldValType ← inferType oldVal
         let valType ← inferType val
         unless (← isDefEq oldValType valType) do
-          throwError "synthesized type class instance type is not definitionally equal to expected type, synthesized{indentExpr val}\nhas type{indentExpr valType}\nexpected{indentExpr oldValType}"
-        throwError "synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized{indentExpr val}\ninferred{indentExpr oldVal}"
+          throwError "synthesized type class instance type is not definitionally equal to expected type, synthesized{indentExpr val}\nhas type{indentExpr valType}\nexpected{indentExpr oldValType}{extraErrorMsg}"
+        throwError "synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized{indentExpr val}\ninferred{indentExpr oldVal}{extraErrorMsg}"
     else
       unless (← isDefEq (mkMVar instMVar) val) do
-        throwError "failed to assign synthesized type class instance{indentExpr val}"
+        throwError "failed to assign synthesized type class instance{indentExpr val}{extraErrorMsg}"
     return true
   | .undef => return false -- we will try later
   | .none  =>
     if (← read).ignoreTCFailures then
       return false
     else
-      throwError "failed to synthesize{indentExpr type}\n{useDiagnosticMsg}"
+      throwError "failed to synthesize{indentExpr type}{extraErrorMsg}\n{useDiagnosticMsg}"
 
 def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
@@ -1603,11 +1617,11 @@ def adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab := fun stx expe
   If type class resolution cannot be executed (e.g., it is stuck because of metavariables in `type`),
   register metavariable as a pending one.
 -/
-def mkInstMVar (type : Expr) : TermElabM Expr := do
+def mkInstMVar (type : Expr) (extraErrorMsg? : Option MessageData := none) : TermElabM Expr := do
   let mvar ← mkFreshExprMVar type MetavarKind.synthetic
   let mvarId := mvar.mvarId!
-  unless (← synthesizeInstMVarCore mvarId) do
-    registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass
+  unless (← synthesizeInstMVarCore mvarId (extraErrorMsg? := extraErrorMsg?)) do
+    registerSyntheticMVarWithCurrRef mvarId (.typeClass extraErrorMsg?)
   return mvar
 
 /--

tests/lean/1163.lean

@@ -1,19 +0,0 @@
-import Lean
-open Lean Elab Tactic
-
-macro "obviously1" : tactic => `(tactic| exact sorryAx _)
-
-theorem result1 : False := by obviously1
-
-elab "obviously2" : tactic =>
-  liftMetaTactic1 fun mvarId => mvarId.admit *> pure none
-
-theorem result2 : False := by obviously2
-
-def x : Bool := 0
-
-theorem result3 : False := by obviously2
-
-theorem result4 : False := by -- Does not generate a `sorry` warning because there is an error
-  let x : Bool := 0
-  obviously2

tests/lean/297.lean.expected.out

@@ -1,3 +1,6 @@
 297.lean:1:10-1:11: error: failed to synthesize
   OfNat (Sort ?u) 0
+numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
+  Sort ?u
+due to the absence of the instance above
 use `set_option diagnostics true` to get diagnostic information

tests/lean/345.lean

@@ -1,6 +0,0 @@
-axiom bla : 1
-
-structure Foo where
-  foo : 1
-
-inductive Bla (x : 1) : Type

tests/lean/run/1163.lean

@@ -0,0 +1,37 @@
+import Lean
+open Lean Elab Tactic
+
+macro "obviously1" : tactic => `(tactic| exact sorryAx _)
+
+theorem result1 : False := by obviously1
+
+elab "obviously2" : tactic =>
+  liftMetaTactic1 fun mvarId => mvarId.admit *> pure none
+
+theorem result2 : False := by obviously2
+
+/--
+error: failed to synthesize
+  OfNat Bool 0
+numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
+  Bool
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+def x : Bool := 0
+
+theorem result3 : False := by obviously2
+
+/--
+error: failed to synthesize
+  OfNat Bool 0
+numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
+  Bool
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+theorem result4 : False := by -- Does not generate a `sorry` warning because there is an error
+  let x : Bool := 0
+  obviously2

tests/lean/run/345.lean

@@ -0,0 +1,34 @@
+
+/--
+error: failed to synthesize
+  OfNat (Sort ?u.1) 1
+numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
+  Sort ?u.1
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+axiom bla : 1
+
+/--
+error: failed to synthesize
+  OfNat (Sort ?u.8) 1
+numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
+  Sort ?u.8
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+structure Foo where
+  foo : 1
+
+/--
+error: failed to synthesize
+  OfNat (Sort ?u.210) 1
+numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
+  Sort ?u.210
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+inductive Bla (x : 1) : Type

tests/lean/run/4365.lean

@@ -0,0 +1,78 @@
+universe u
+
+/--
+error: numerals are data in Lean, but the expected type is a proposition
+  True : Prop
+-/
+#guard_msgs in
+#check (1 : True)
+
+/--
+error: numerals are data in Lean, but the expected type is universe polymorphic and may be a proposition
+  α : Sort u
+-/
+#guard_msgs in
+def f (α : Sort u) : α :=
+  1
+
+/--
+error: numerals are data in Lean, but the expected type is universe polymorphic and may be a proposition
+  α : Sort u
+---
+info: fun {α} => id (id (sorryAx α true)) : {α : Sort u} → α
+-/
+#guard_msgs in
+#check fun {α : Sort u} => id (α := α) (id 0)
+
+/--
+error: numerals are data in Lean, but the expected type is a proposition
+  Nat → True : Prop
+-/
+#guard_msgs in
+#check (1 : ∀ (n : Nat), True)
+
+/--
+error: failed to synthesize
+  OfNat String 1
+numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
+  String
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+#check (1 : String)
+
+/--
+error: failed to synthesize
+  OfNat Bool 1
+numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
+  Bool
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+#check (1 : Bool)
+
+/--
+error: failed to synthesize
+  OfNat (Bool → Nat) 1
+numerals are polymorphic in Lean, but the numeral `1` cannot be used in a context where the expected type is
+  Bool → Nat
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+#check (1 : Bool → Nat)
+
+/--
+error: failed to synthesize
+  OfNat String 0
+numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
+  String
+due to the absence of the instance above
+use `set_option diagnostics true` to get diagnostic information
+-/
+#guard_msgs in
+def foo : String :=
+  let x := 0
+  x ++ x

tests/lean/run/guard_msgs.lean

@@ -48,6 +48,9 @@ example : α := x
 /--
 error: failed to synthesize
   OfNat α 22
+numerals are polymorphic in Lean, but the numeral `22` cannot be used in a context where the expected type is
+  α
+due to the absence of the instance above
 use `set_option diagnostics true` to get diagnostic information
 -/
 #guard_msgs(error) in