feat: include type of type in "mismatch errors"

@Kha we do that in Lean 3. It helps when the error is due to incorrect universe levels.

BTW, I had to update `tests/lean/server/content_diag.json` since the
error message is different, but a few other stuff changed too.
Could you please take a look whether the test is still correct?

src/Lean/Meta/Check.lean

@@ -114,8 +114,15 @@ where
   Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
 -/
 def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) : MetaM MessageData := do
-  let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
-  m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
+  try
+    let givenTypeType ← inferType givenType
+    let expectedTypeType ← inferType expectedType
+    let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
+    let (givenTypeType, expectedTypeType) ← addPPExplicitToExposeDiff givenTypeType expectedTypeType
+    m!"has type{indentD m!"{givenType} : {givenTypeType}"}\nbut is expected to have type{indentD m!"{expectedType} : {expectedTypeType}"}"
+  catch _ =>
+    let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
+    m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
 
 def throwAppTypeMismatch {α} (f a : Expr) (extraMsg : MessageData := Format.nil) : MetaM α := do
   let (expectedType, binfo) ← getFunctionDomain f

tests/lean/301.lean.expected.out

@@ -3,6 +3,6 @@
 301.lean:1:21-1:24: error: type mismatch
    ( fun (x : Nat) => ?m x)
 has type
-  (n : Nat) → ?m ( fun (x : Nat) => ?m x) n
+  (n : Nat) → ?m ( fun (x : Nat) => ?m x) n : Type ?u
 but is expected to have type
-  ?m x n
+  ?m x n : Type ?u

tests/lean/autoPPExplicit.lean.expected.out

@@ -3,6 +3,6 @@ autoPPExplicit.lean:2:2-2:32: error: application type mismatch
 argument
   b = c
 has type
-  Prop
+  Prop : Type
 but is expected to have type
-  α
+  α : Sort ?u

tests/lean/doErrorMsg.lean.expected.out

@@ -1,30 +1,30 @@
 doErrorMsg.lean:3:2-3:13: error: type mismatch
   IO.getStdin
 has type
-  EIO IO.Error IO.FS.Stream
+  EIO IO.Error IO.FS.Stream : Type
 but is expected to have type
-  EIO IO.Error PUnit
+  EIO IO.Error PUnit : Type
 doErrorMsg.lean:15:19-15:21: error: type mismatch
   f1
 has type
-  ExceptT String (StateT Nat Id) Nat
+  ExceptT String (StateT Nat Id) Nat : Type
 but is expected to have type
-  ExceptT String (StateT Nat Id) String
+  ExceptT String (StateT Nat Id) String : Type
 doErrorMsg.lean:19:19-19:24: error: type mismatch
   f2 10
 has type
-  ExceptT String (StateT Nat Id) Nat
+  ExceptT String (StateT Nat Id) Nat : Type
 but is expected to have type
-  ExceptT String (StateT Nat Id) String
+  ExceptT String (StateT Nat Id) String : Type
 doErrorMsg.lean:24:2-24:4: error: type mismatch
   f1
 has type
-  ExceptT String (StateT Nat Id) Nat
+  ExceptT String (StateT Nat Id) Nat : Type
 but is expected to have type
-  ExceptT String (StateT Nat Id) String
+  ExceptT String (StateT Nat Id) String : Type
 doErrorMsg.lean:23:10-23:12: error: type mismatch
   f2
 has type
-  Nat → ExceptT String (StateT Nat Id) Nat
+  Nat → ExceptT String (StateT Nat Id) Nat : Type
 but is expected to have type
-  ExceptT String (StateT Nat Id) ?m
+  ExceptT String (StateT Nat Id) ?m : Type

tests/lean/doIssue.lean.expected.out

@@ -1,20 +1,20 @@
 doIssue.lean:2:2-2:3: error: type mismatch
   x
 has type
-  Nat
+  Nat : Type
 but is expected to have type
-  EIO IO.Error PUnit
+  EIO IO.Error PUnit : Type
 doIssue.lean:10:2-10:13: error: type mismatch
   Array.set! xs 0 1
 has type
-  Array Nat
+  Array Nat : Type
 but is expected to have type
-  EIO IO.Error PUnit
+  EIO IO.Error PUnit : Type
 doIssue.lean:18:2-18:20: error: application type mismatch
   pure (Array.set! xs 0 1)
 argument
   Array.set! xs 0 1
 has type
-  Array Nat
+  Array Nat : Type
 but is expected to have type
-  PUnit
+  PUnit : Type

tests/lean/doNotation1.lean.expected.out

@@ -2,21 +2,21 @@ doNotation1.lean:4:0-4:6: error: 'y' cannot be reassigned
 doNotation1.lean:8:2-8:18: error: 'y' cannot be reassigned
 doNotation1.lean:12:2-12:17: error: 'p' cannot be reassigned
 doNotation1.lean:20:7-20:22: error: invalid reassignment, value has type
-  Vector Nat (n + 1)
+  Vector Nat (n + 1) : Type
 but is expected to have type
-  Vector Nat n
+  Vector Nat n : Type
 doNotation1.lean:25:7-25:11: error: invalid reassignment, value has type
-  Bool
+  Bool : Type
 but is expected to have type
-  Nat
+  Nat : Type
 doNotation1.lean:24:0-25:11: error: type mismatch, 'for' has type
-  PUnit
+  PUnit : Sort ?u
 but is expected to have type
-  List Bool
+  List Bool : Type
 doNotation1.lean:28:0-29:14: error: type mismatch, 'for' has type
-  PUnit
+  PUnit : Sort ?u
 but is expected to have type
-  List Nat
+  List Nat : Type
 doNotation1.lean:33:2-33:7: error: invalid 'do' element, it must be inside 'for'
 doNotation1.lean:37:2-37:10: error: invalid 'do' element, it must be inside 'for'
 doNotation1.lean:40:0-40:9: error: must be last element in a 'do' sequence
@@ -25,12 +25,12 @@ fun (x : Nat) => IO.println x
 doNotation1.lean:51:0-51:13: error: type mismatch
   IO.mkRef true
 has type
-  EIO IO.Error (IO.Ref Bool)
+  EIO IO.Error (IO.Ref Bool) : Type
 but is expected to have type
-  EIO IO.Error Unit
+  EIO IO.Error Unit : Type
 doNotation1.lean:58:2-58:20: error: type mismatch, result value has type
-  Unit
+  Unit : Type
 but is expected to have type
-  Bool
+  Bool : Type
 doNotation1.lean:66:0-66:18: error: 'do' element is unreachable
 doNotation1.lean:70:0-70:32: error: 'do' element is unreachable

tests/lean/elseifDoErrorPos.lean.expected.out

@@ -3,6 +3,6 @@ elseifDoErrorPos.lean:4:7-7:14: error: application type mismatch
 argument
   x
 has type
-  Nat
+  Nat : Type
 but is expected to have type
-  Prop
+  Prop : Type

tests/lean/evalSorry.lean.expected.out

@@ -4,8 +4,8 @@ evalSorry.lean:5:31-5:34: error: application type mismatch
 argument
   x
 has type
-  String
+  String : Type
 but is expected to have type
-  Nat
+  Nat : Type
 evalSorry.lean:7:0-7:15: error: cannot evaluate code because it uses 'sorry' and/or contains errors
 evalSorry.lean:11:0-11:15: error: cannot evaluate code because it uses 'sorry' and/or contains errors

tests/lean/inductive1.lean.expected.out

@@ -8,9 +8,9 @@ inductive1.lean:22:0-22:37: error: invalid mutually inductive types, resulting u
 expected type
   Type u
 inductive1.lean:31:0-31:41: error: invalid mutually inductive types, parameter 'x' has type
-  Bool
+  Bool : Type
 but is expected to have type
-  Nat
+  Nat : Type
 inductive1.lean:40:0-40:30: error: invalid inductive type, number of parameters mismatch in mutually inductive datatypes
 inductive1.lean:49:0-49:40: error: invalid mutually inductive types, binder annotation mismatch at parameter 'x'
 inductive1.lean:59:0-59:45: error: invalid inductive type, universe parameters mismatch in mutually inductive datatypes

tests/lean/isDefEqOffsetBug.lean.expected.out

@@ -1,6 +1,6 @@
 isDefEqOffsetBug.lean:27:2-27:5: error: type mismatch
   rfl
 has type
-  0 + 0 = 0 + 0
+  0 + 0 = 0 + 0 : Prop
 but is expected to have type
-  0 + 0 = 0
+  0 + 0 = 0 : Prop

tests/lean/matchErrorLocation.lean.expected.out

@@ -1,6 +1,6 @@
 matchErrorLocation.lean:5:10-5:14: error: type mismatch
   h he
 has type
-  False
+  False : Prop
 but is expected to have type
-  α
+  α : Type ?u

tests/lean/modBug.lean.expected.out

@@ -3,6 +3,6 @@ modBug.lean:1:32-1:62: error: application type mismatch
 argument
   Nat.mod_zero 1
 has type
-  1 % 0 = 1
+  1 % 0 = 1 : Prop
 but is expected to have type
-  0 = 1
+  0 = 1 : Prop

tests/lean/namedHoles.lean.expected.out

@@ -3,9 +3,9 @@ namedHoles.lean:9:7-9:14: error: application type mismatch
 argument
   ?m
 has type
-  Nat
+  Nat : Type
 but is expected to have type
-  Bool
+  Bool : Type
 g ?m ?m : Nat
 20
 foo (fun (x : Nat) => ?m x) ?m : Nat

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -3,8 +3,8 @@ phashmap_inst_coherence.lean:12:6-12:56: error: application type mismatch
 argument
   m
 has type
-  @PersistentHashMap Nat Nat instBEq instHashableNat
+  @PersistentHashMap Nat Nat instBEq instHashableNat : Type
 but is expected to have type
-  @PersistentHashMap Nat Nat instBEq natDiffHash
+  @PersistentHashMap Nat Nat instBEq natDiffHash : Type
 phashmap_inst_coherence.lean:12:0-12:56: error: failed to synthesize
   Lean.Eval ?m

tests/lean/pureCoeIssue.lean.expected.out

@@ -1,12 +1,12 @@
 pureCoeIssue.lean:6:2-6:4: error: type mismatch
   f1
 has type
-  Nat → IO Unit
+  Nat → IO Unit : Type
 but is expected to have type
-  EIO IO.Error PUnit
+  EIO IO.Error PUnit : Type
 pureCoeIssue.lean:14:2-14:7: error: type mismatch
   f2 10
 has type
-  Nat → IO Unit
+  Nat → IO Unit : Type
 but is expected to have type
-  EIO IO.Error PUnit
+  EIO IO.Error PUnit : Type

tests/lean/scopedunifhint.lean.expected.out

@@ -3,25 +3,25 @@ scopedunifhint.lean:28:7-28:14: error: application type mismatch
 argument
   x
 has type
-  Nat
+  Nat : Type
 but is expected to have type
-  ?m.α
+  ?m.α : Type ?u
 scopedunifhint.lean:29:7-29:24: error: application type mismatch
   mul ?m (x, x)
 argument
   (x, x)
 has type
-  Nat × Nat
+  Nat × Nat : Type
 but is expected to have type
-  ?m.α
+  ?m.α : Type ?u
 scopedunifhint.lean:33:7-33:10: error: application type mismatch
   ?m*x
 argument
   x
 has type
-  Nat
+  Nat : Type
 but is expected to have type
-  ?m.α
+  ?m.α : Type ?u
 x*x : Nat.Magma.α
 x*x : Nat.Magma.α
 scopedunifhint.lean:39:7-39:24: error: application type mismatch
@@ -29,15 +29,15 @@ scopedunifhint.lean:39:7-39:24: error: application type mismatch
 argument
   (x, x)
 has type
-  Nat × Nat
+  Nat × Nat : Type
 but is expected to have type
-  ?m.α
+  ?m.α : Type ?u
 (x, x)*(x, x) : (Prod.Magma Nat.Magma Nat.Magma).α
 scopedunifhint.lean:56:7-56:22: error: application type mismatch
   ?m*(x, x)
 argument
   (x, x)
 has type
-  Nat × Nat
+  Nat × Nat : Type
 but is expected to have type
-  ?m.α
+  ?m.α : Type ?u

tests/lean/server/content_diag.json

@@ -2,58 +2,40 @@
  {"version": 1,
   "uri": "file:///test.lean",
   "diagnostics":
-  [{"tags": null,
-    "source": "Lean 4 server",
+  [{"source": "Lean 4 server",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 4, "character": 0}, "end": {"line": 4, "character": 6}},
-    "message": "n : Nat",
-    "code": null},
-   {"tags": null,
-    "source": "Lean 4 server",
+    "message": "n : Nat"},
+   {"source": "Lean 4 server",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 8, "character": 0}, "end": {"line": 8, "character": 6}},
-    "message": "s : String",
-    "code": null},
-   {"tags": null,
-    "source": "Lean 4 server",
+    "message": "s : String"},
+   {"source": "Lean 4 server",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 12, "character": 0},
      "end": {"line": 12, "character": 5}},
-    "message": "Hello world!\n",
-    "code": null},
-   {"tags": null,
-    "source": "Lean 4 server",
+    "message": "Hello world!\n"},
+   {"source": "Lean 4 server",
     "severity": 1,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 14, "character": 31},
      "end": {"line": 14, "character": 40}},
     "message":
-    "type mismatch\n  \"NotANat\"\nhas type\n  String\nbut is expected to have type\n  Nat",
-    "code": null},
-   {"tags": null,
-    "source": "Lean 4 server",
+    "type mismatch\n  \"NotANat\"\nhas type\n  String : Type\nbut is expected to have type\n  Nat : Type"},
+   {"source": "Lean 4 server",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 22, "character": 0},
      "end": {"line": 22, "character": 6}},
-    "message": "MyNs.u : Unit",
-    "code": null},
-   {"tags": null,
-    "source": "Lean 4 server",
+    "message": "MyNs.u : Unit"},
+   {"source": "Lean 4 server",
     "severity": 3,
-    "relatedInformation": null,
     "range":
     {"start": {"line": 24, "character": 0},
      "end": {"line": 24, "character": 6}},
-    "message": "def MyNs.u : Unit :=\nUnit.unit",
-    "code": null}]},
+    "message": "def MyNs.u : Unit :=\nUnit.unit"}]},
  "method": "textDocument/publishDiagnostics",
  "jsonrpc": "2.0"}

tests/lean/shadow.lean.expected.out

@@ -1,15 +1,15 @@
 shadow.lean:6:0-6:1: error: type mismatch
   h
 has type
-  x✝ = x✝
+  x✝ = x✝ : Prop
 but is expected to have type
-  x = x
+  x = x : Prop
 shadow.lean:10:0-10:1: error: type mismatch
   h
 has type
-  x = x
+  x = x : Prop
 but is expected to have type
-  x = x
+  x = x : Prop
 shadow.lean:13:0-13:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1

tests/lean/sorryAtError.lean.expected.out

@@ -3,6 +3,6 @@ sorryAtError.lean:13:40-13:47: error: application type mismatch
 argument
   Γ
 has type
-  x.ty.ctx
+  x.ty.ctx : Type
 but is expected to have type
-  ty.ctx
+  ty.ctx : Type

tests/lean/struct1.lean.expected.out

@@ -9,16 +9,16 @@ struct1.lean:32:1-32:2: error: field 'x' has been declared in parent structure
 struct1.lean:35:6-35:10: error: type mismatch
   true
 has type
-  Bool
+  Bool : Type
 but is expected to have type
-  Nat
+  Nat : Type
 struct1.lean:38:5-38:9: error: omit field 'x' type to set default value
 struct1.lean:41:12-41:16: error: type mismatch
   true
 has type
-  Bool
+  Bool : Type
 but is expected to have type
-  Nat
+  Nat : Type
 struct1.lean:44:0-44:13: error: invalid 'private' constructor in a 'private' structure
 struct1.lean:47:0-47:15: error: invalid 'protected' constructor in a 'private' structure
 struct1.lean:50:0-50:19: error: invalid 'protected' field in a 'private' structure

tests/lean/structDefault.lean.expected.out

@@ -1,6 +1,6 @@
 structDefault.lean:11:11-11:15: error: type mismatch
   true
 has type
-  Bool
+  Bool : Type
 but is expected to have type
-  Nat
+  Nat : Type

tests/lean/typeIncorrectPat.lean.expected.out

@@ -1,6 +1,6 @@
 typeIncorrectPat.lean:2:1-2:17: error: pattern
   true
 has type
-  Bool
+  Bool : Type
 but is expected to have type
-  fst✝
+  fst✝ : Type

tests/lean/typeMismatch.lean.expected.out

@@ -1,12 +1,12 @@
 typeMismatch.lean:7:0-7:13: error: type mismatch
   IO.println ""
 has type
-  IO Unit
+  IO Unit : Type
 but is expected to have type
-  IO Nat
+  IO Nat : Type
 typeMismatch.lean:12:0-12:16: error: type mismatch
   Meta.isDefEq x x
 has type
-  MetaM Bool
+  MetaM Bool : Type
 but is expected to have type
-  MetaM Unit
+  MetaM Unit : Type

tests/lean/typeOf.lean.expected.out

@@ -4,10 +4,10 @@ typeOf.lean:12:0-12:5: error: failed to synthesize instance
   HAdd Bool Nat Nat
 typeOf.lean:10:4-10:6: error: (kernel) declaration has metavariables 'f2'
 typeOf.lean:20:54-20:60: error: invalid reassignment, term has type
-  Bool
+  Bool : Type
 but is expected to have type
-  Nat
+  Nat : Type
 typeOf.lean:29:53-29:57: error: natural number expected, value has type
-  Bool
+  Bool : Type
 but is expected to have type
-  Nat
+  Nat : Type