Different delaboration in lazy context? oh well, fine with me

This reverts commit afaaa6ef4b.

src/Lean/Meta/Basic.lean

@@ -2545,6 +2545,38 @@ where
 
 end Meta
 
+open Meta
+
+namespace PPContext
+
+def runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
+  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace
+                        openDecls := ppCtx.openDecls
+                        fileName := "<PrettyPrinter>", fileMap := default
+                        diag     := getDiag ppCtx.opts }
+                      { env := ppCtx.env, ngen := { namePrefix := `_pp_uniq } }
+
+def runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
+  ppCtx.runCoreM <| x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
+
+end PPContext
+
+/--
+Turns a `MetaM MessageData` into a `MessageData.lazy` which will run the monadic value.
+The optional array of expressions is used to set the `hasSyntheticSorry` fields, and should
+comprise the expressions that are included in the message data.
+-/
+def MessageData.ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData :=
+  .lazy
+    (f := fun ppctxt => do
+      match (← ppctxt.runMetaM f |>.toBaseIO) with
+      | .ok fmt => return fmt
+      | .error ex => return m!"[Error pretty printing: {ex}]"
+      )
+    (hasSyntheticSorry := fun mvarctxt => es.any (fun a =>
+        instantiateMVarsCore mvarctxt a |>.1.hasSyntheticSorry
+    ))
+
 builtin_initialize
   registerTraceClass `Meta.isLevelDefEq.postponed
   registerTraceClass `Meta.realizeConst

src/Lean/Meta/Check.lean

@@ -191,18 +191,26 @@ def throwLetTypeMismatchMessage {α} (fvarId : FVarId) : MetaM α := do
   | _ => unreachable!
 
 /--
-  Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
+Return error message "has type{givenType}\nbut is expected to have type{expectedType}"
+Adds the type’s types unless they are defeq.
 -/
-def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) : MetaM MessageData := do
-  try
-    let givenTypeType ← inferType givenType
-    let expectedTypeType ← inferType expectedType
-    let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
-    let (givenTypeType, expectedTypeType) ← addPPExplicitToExposeDiff givenTypeType expectedTypeType
-    return m!"has type{indentD m!"{givenType} : {givenTypeType}"}\nbut is expected to have type{indentD m!"{expectedType} : {expectedTypeType}"}"
-  catch _ =>
-    let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
-    return m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
+def mkHasTypeButIsExpectedMsg (givenType expectedType : Expr) : MetaM MessageData :=
+  return MessageData.ofLazyM (es := #[givenType, expectedType]) do
+    try
+      let givenTypeType ← inferType givenType
+      let expectedTypeType ← inferType expectedType
+      if (← isDefEqGuarded givenTypeType expectedTypeType) then
+        let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
+        return m!"has type{indentExpr givenType}\n\
+          but is expected to have type{indentExpr expectedType}"
+      else
+        let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
+        let (givenTypeType, expectedTypeType) ← addPPExplicitToExposeDiff givenTypeType expectedTypeType
+        return m!"has type{indentExpr givenType}\nof sort{inlineExpr givenTypeType}\
+          but is expected to have type{indentExpr expectedType}\nof sort{inlineExprTrailing expectedTypeType}"
+    catch _ =>
+      let (givenType, expectedType) ← addPPExplicitToExposeDiff givenType expectedType
+      return m!"has type{indentExpr givenType}\nbut is expected to have type{indentExpr expectedType}"
 
 def throwAppTypeMismatch (f a : Expr) : MetaM α := do
   let (expectedType, binfo) ← getFunctionDomain f

src/Lean/PrettyPrinter.lean

@@ -11,19 +11,8 @@ import Lean.Parser.Module
 import Lean.ParserCompiler
 import Lean.Util.NumObjs
 import Lean.Util.ShareCommon
-namespace Lean
 
-def PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α :=
-  Prod.fst <$> x.toIO { options := ppCtx.opts, currNamespace := ppCtx.currNamespace
-                        openDecls := ppCtx.openDecls
-                        fileName := "<PrettyPrinter>", fileMap := default
-                        diag     := getDiag ppCtx.opts }
-                      { env := ppCtx.env, ngen := { namePrefix := `_pp_uniq } }
-
-def PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α :=
-  ppCtx.runCoreM <| x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx }
-
-namespace PrettyPrinter
+namespace Lean.PrettyPrinter
 
 def ppCategory (cat : Name) (stx : Syntax) : CoreM Format := do
   let opts ← getOptions
@@ -147,22 +136,6 @@ def ofFormatWithInfosM (fmt : MetaM FormatWithInfos) : MessageData :=
     | .ok fmt => return .ofFormatWithInfos fmt
     | .error ex => return m!"[Error pretty printing: {ex}]"
 
-/--
-Turns a `MetaM MessageData` into a `MessageData.lazy` which will run the monadic value.
-The optional array of expressions is used to set the `hasSyntheticSorry` fields, and should
-comprise the expressions that are included in the message data.
--/
-def ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData :=
-  .lazy
-    (f := fun ppctxt => do
-      match (← ppctxt.runMetaM f |>.toBaseIO) with
-      | .ok fmt => return fmt
-      | .error ex => return m!"[Error pretty printing: {ex}]"
-      )
-    (hasSyntheticSorry := fun mvarctxt => es.any (fun a =>
-        instantiateMVarsCore mvarctxt a |>.1.hasSyntheticSorry
-    ))
-
 /--
 Pretty print a const expression using `delabConst` and generate terminfo.
 This function avoids inserting `@` if the constant is for a function whose first

tests/lean/1057.lean.expected.out

@@ -1,4 +1,4 @@
 1057.lean:9:2-9:28: error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive t Int : Sort ?u
+  motive t Int
 but is expected to have type
-  motive t x✝ : Sort ?u
+  motive t x✝

tests/lean/1081.lean.expected.out

@@ -1,12 +1,12 @@
 1081.lean:7:2-7:5: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  ?m = ?m
 but is expected to have type
-  f 0 y = y : Prop
+  f 0 y = y
 1081.lean:23:4-23:9: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  ?m = ?m
 but is expected to have type
-  insert a ⟨0, ⋯⟩ v = cons a v : Prop
+  insert a ⟨0, ⋯⟩ v = cons a v

tests/lean/1433.lean.expected.out

@@ -1,6 +1,6 @@
 1433.lean:11:49-11:54: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  ?m = ?m
 but is expected to have type
-  dividend % divisor = wrongRem : Prop
+  dividend % divisor = wrongRem

tests/lean/243.lean.expected.out

@@ -3,14 +3,14 @@
 the argument
   true
 has type
-  _root_.Bool : Type
+  _root_.Bool
 but is expected to have type
-  Bool : Type
+  Bool
 243.lean:13:7-13:8: error: Application type mismatch: In the application
   ⟨A, a⟩
 the argument
   a
 has type
-  Foo.A : Type
+  Foo.A
 but is expected to have type
-  A : Type
+  A

tests/lean/283.lean.expected.out

@@ -3,6 +3,7 @@
 the argument
   f
 has type
-  ?m : Sort ?u
-but is expected to have type
-  optParam (Sort ?u) t : Type ?u
+  ?m
+of sort `Sort ?u` but is expected to have type
+  optParam (Sort ?u) t
+of sort `Type ?u`

tests/lean/389.lean.expected.out

@@ -3,7 +3,7 @@
 the argument
   bar
 has type
-  Bar Nat : Type
+  Bar Nat
 but is expected to have type
-  Foo ?m : Type
+  Foo ?m
 getFoo bar.toFoo : Nat

tests/lean/423.lean.expected.out

@@ -3,30 +3,34 @@
 the argument
   a
 has type
-  T : Sort u
-but is expected to have type
-  Nat : Type
+  T
+of sort `Sort u` but is expected to have type
+  Nat
+of sort `Type`
 423.lean:5:37-5:38: error: Application type mismatch: In the application
   Add T
 the argument
   T
 has type
-  Sort u : Type u
-but is expected to have type
-  Type ?u : Type (?u + 1)
+  Sort u
+of sort `Type u` but is expected to have type
+  Type ?u
+of sort `Type (?u + 1)`
 423.lean:5:47-5:48: error: Application type mismatch: In the application
   OfNat T
 the argument
   T
 has type
-  Sort u : Type u
-but is expected to have type
-  Type ?u : Type (?u + 1)
+  Sort u
+of sort `Type u` but is expected to have type
+  Type ?u
+of sort `Type (?u + 1)`
 423.lean:5:55-5:60: error: Application type mismatch: In the application
   HAdd.hAdd a
 the argument
   a
 has type
-  T : Sort u
-but is expected to have type
-  Nat : Type
+  T
+of sort `Sort u` but is expected to have type
+  Nat
+of sort `Type`

tests/lean/755.lean.expected.out

@@ -1,24 +1,24 @@
 755.lean:7:44-7:47: error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  0 = 0 : Prop
+  0 = 0
 755.lean:26:2-26:5: error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  2 * 3 = 2 * 3 : Prop
+  2 * 3 = 2 * 3
 755.lean:29:2-29:5: error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  2 + 3 = 2 + 3 : Prop
+  2 + 3 = 2 + 3
 755.lean:32:2-32:5: error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  2 - 3 = 2 - 3 : Prop
+  2 - 3 = 2 - 3

tests/lean/autoPPExplicit.lean.expected.out

@@ -3,6 +3,7 @@ autoPPExplicit.lean:2:26-2:31: error: Application type mismatch: In the applicat
 the argument
   b = c
 has type
-  Prop : Type
-but is expected to have type
-  α : Sort u_1
+  Prop
+of sort `Type` but is expected to have type
+  α
+of sort `Sort u_1`

tests/lean/binrelTypeMismatch.lean.expected.out

@@ -1,20 +1,20 @@
 binrelTypeMismatch.lean:10:14-10:16: error: type mismatch
   ()
 has type
-  Unit : Type
+  Unit
 but is expected to have type
-  Bool : Type
+  Bool
 binrelTypeMismatch.lean:15:21-15:22: error: type mismatch
   p
 has type
-  Prop : Type
+  Prop
 but is expected to have type
-  Bool : Type
+  Bool
 Prop → sorry : Sort u_1
 binrelTypeMismatch.lean:20:27-20:28: error: type mismatch
   p
 has type
-  Prop : Type
+  Prop
 but is expected to have type
-  Bool : Type
+  Bool
 Prop → sorry : Sort u_1

tests/lean/calcErrors.lean.expected.out

@@ -1,9 +1,9 @@
 calcErrors.lean:7:30-7:33: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  ?m = ?m
 but is expected to have type
-  b + b = 0 + c + b : Prop
+  b + b = 0 + c + b
 calcErrors.lean:13:8-13:29: error: invalid 'calc' step, left-hand side is
   0 + c + b : Nat
 but previous right-hand side is

tests/lean/diamond1.lean.expected.out

@@ -1,7 +1,7 @@
 diamond1.lean:11:40-11:45: error: field type mismatch, field 'a' from parent 'Baz' has type
-  α → α : Type
+  α → α
 but is expected to have type
-  α : Type
+  α
 structure Foo (α : Type) : Type
 number of parameters: 1
 parents:

tests/lean/doErrorMsg.lean.expected.out

@@ -1,38 +1,38 @@
 doErrorMsg.lean:3:2-3:13: error: type mismatch
   IO.getStdin
 has type
-  BaseIO IO.FS.Stream : Type
+  BaseIO IO.FS.Stream
 but is expected to have type
-  IO PUnit : Type
+  IO PUnit
 doErrorMsg.lean:15:19-15:21: error: type mismatch
   f1
 has type
-  ExceptT String (StateT Nat Id) Nat : Type
+  ExceptT String (StateT Nat Id) Nat
 but is expected to have type
-  ExceptT String (StateT Nat Id) String : Type
+  ExceptT String (StateT Nat Id) String
 doErrorMsg.lean:19:19-19:24: error: type mismatch
   f2 10
 has type
-  ExceptT String (StateT Nat Id) Nat : Type
+  ExceptT String (StateT Nat Id) Nat
 but is expected to have type
-  ExceptT String (StateT Nat Id) String : Type
+  ExceptT String (StateT Nat Id) String
 doErrorMsg.lean:23:10-23:12: error: type mismatch
   f2
 has type
-  Nat → ExceptT String (StateT Nat Id) Nat : Type
+  Nat → ExceptT String (StateT Nat Id) Nat
 but is expected to have type
-  ExceptT String (StateT Nat Id) ?m : Type
+  ExceptT String (StateT Nat Id) ?m
 doErrorMsg.lean:24:2-24:4: error: type mismatch
   f1
 has type
-  ExceptT String (StateT Nat Id) Nat : Type
+  ExceptT String (StateT Nat Id) Nat
 but is expected to have type
-  ExceptT String (StateT Nat Id) String : Type
+  ExceptT String (StateT Nat Id) String
 doErrorMsg.lean:28:13-28:18: error: Application type mismatch: In the application
   Prod.mk false
 the argument
   false
 has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat

tests/lean/doIssue.lean.expected.out

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

tests/lean/doNotation1.lean.expected.out

@@ -2,21 +2,21 @@ doNotation1.lean:4:0-4:6: error: `y` cannot be mutated, only variables declared
 doNotation1.lean:8:2-8:18: error: `y` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `y`, consider using `let y` instead
 doNotation1.lean:12:2-12:17: error: `p` cannot be mutated, only variables declared using `let mut` can be mutated. If you did not intend to mutate but define `p`, consider using `let p` instead
 doNotation1.lean:20:7-20:23: error: invalid reassignment, value has type
-  Vector' Nat (n + 1) : Type
+  Vector' Nat (n + 1)
 but is expected to have type
-  Vector' Nat n : Type
+  Vector' Nat n
 doNotation1.lean:25:7-25:11: error: invalid reassignment, value has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat
 doNotation1.lean:24:0-25:11: error: type mismatch, `for` has type
-  PUnit : Sort ?u
+  PUnit
 but is expected to have type
-  List Bool : Type
+  List Bool
 doNotation1.lean:28:0-29:14: error: type mismatch, `for` has type
-  PUnit : Sort ?u
+  PUnit
 but is expected to have type
-  List Nat : Type
+  List Nat
 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 => IO.println x
 doNotation1.lean:51:0-51:13: error: type mismatch
   IO.mkRef true
 has type
-  BaseIO (IO.Ref Bool) : Type
+  BaseIO (IO.Ref Bool)
 but is expected to have type
-  IO Unit : Type
+  IO Unit
 doNotation1.lean:58:2-58:20: error: type mismatch, result value has type
-  Unit : Type
+  Unit
 but is expected to have type
-  Bool : Type
+  Bool
 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,14 +3,14 @@ elseifDoErrorPos.lean:4:10-4:11: error: Application type mismatch: In the applic
 the argument
   x
 has type
-  Nat : Type
+  Nat
 but is expected to have type
-  Prop : Type
+  Prop
 elseifDoErrorPos.lean:7:11-7:14: error: Application type mismatch: In the application
   pure "a"
 the argument
   "a"
 has type
-  String : Type
+  String
 but is expected to have type
-  Nat : Type
+  Nat

tests/lean/etaStructIssue.lean.expected.out

@@ -1,6 +1,6 @@
 etaStructIssue.lean:20:2-20:7: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  ?m = ?m
 but is expected to have type
-  mkNat e x₁ = mkNat e.mk x₂ : Prop
+  mkNat e x₁ = mkNat e.mk x₂

tests/lean/evalSorry.lean.expected.out

@@ -4,9 +4,9 @@ evalSorry.lean:5:33-5:34: error: Application type mismatch: In the application
 the argument
   x
 has type
-  String : Type
+  String
 but is expected to have type
-  Nat : Type
+  Nat
 evalSorry.lean:7:0-7:5: error: aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
 
 To attempt to evaluate anyway despite the risks, use the '#eval!' command.

tests/lean/have.lean.expected.out

@@ -5,6 +5,6 @@ context:
 have.lean:7:2-7:3: error: type mismatch
   f
 has type
-  5 = 6 : Prop
+  5 = 6
 but is expected to have type
-  5 = 3 : Prop
+  5 = 3

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 : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat
 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:19:2-19:7: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  ?m = ?m
 but is expected to have type
-  0 + 0 = 0 : Prop
+  0 + 0 = 0

tests/lean/macroSwizzle.lean.expected.out

@@ -7,7 +7,7 @@ macroSwizzle.lean:6:7-6:10: error: Application type mismatch: In the application
 the argument
   "x"
 has type
-  String : Type
+  String
 but is expected to have type
-  Nat : Type
+  Nat
 sorry.succ : Nat

tests/lean/match1.lean.expected.out

@@ -11,9 +11,9 @@
 ---- inv
 10
 match1.lean:82:0-82:73: error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive 0 (Vec.cons head✝ Vec.nil) ⋯ : Prop
+  motive 0 (Vec.cons head✝ Vec.nil) ⋯
 but is expected to have type
-  motive x✝ (Vec.cons head✝ tail✝) ⋯ : Prop
+  motive x✝ (Vec.cons head✝ tail✝) ⋯
 [false, true, true]
 match1.lean:119:0-119:41: error: Dependent match elimination failed: Expected a constructor, but found the inaccessible pattern
   .(j + j)

tests/lean/matchErrorLocation.lean.expected.out

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

tests/lean/modBug.lean.expected.out

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

tests/lean/motiveNotTypeCorect.lean.expected.out

@@ -5,9 +5,9 @@ Error: Application type mismatch: In the application
 the argument
   d
 has type
-  D (f t) : Type
+  D (f t)
 but is expected to have type
-  D _a : Type
+  D _a
 
 Explanation: The rewrite tactic rewrites an expression 'e' using an equality 'a = b' by the following process. First, it looks for all 'a' in 'e'. Second, it tries to abstract these occurrences of 'a' to create a function 'm := fun _a => ...', called the *motive*, with the property that 'm a' is definitionally equal to 'e'. Third, we observe that 'congrArg' implies that 'm a = m b', which can be used with lemmas such as 'Eq.mpr' to change the goal. However, if 'e' depends on specific properties of 'a', then the motive 'm' might not typecheck.
 

tests/lean/mulcommErrorMessage.lean.expected.out

@@ -1,9 +1,9 @@
 mulcommErrorMessage.lean:8:13-13:25: error: type mismatch
   fun a b => ?m
 has type
-  (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
+  (a : ?m) → (b : ?m a) → ?m a b
 but is expected to have type
-  a✝ * b✝ = b✝ * a✝ : Prop
+  a✝ * b✝ = b✝ * a✝
 the following variables have been introduced by the implicit lambda feature
   a✝ : Bool
   b✝ : Bool
@@ -11,15 +11,15 @@ you can disable implicit lambdas using `@` or writing a lambda expression with `
 mulcommErrorMessage.lean:12:22-12:25: error: type mismatch
   rfl
 has type
-  ?m = ?m : Prop
+  ?m = ?m
 but is expected to have type
-  false = true : Prop
+  false = true
 mulcommErrorMessage.lean:16:3-17:47: error: type mismatch
   fun a b => ?m
 has type
-  (a : ?m) → (b : ?m a) → ?m a b : Sort (imax ?u ?u ?u)
+  (a : ?m) → (b : ?m a) → ?m a b
 but is expected to have type
-  a✝ * b✝ = b✝ * a✝ : Prop
+  a✝ * b✝ = b✝ * a✝
 the following variables have been introduced by the implicit lambda feature
   a✝ : Bool
   b✝ : Bool

tests/lean/nameArgErrorIssue.lean.expected.out

@@ -4,17 +4,17 @@ nameArgErrorIssue.lean:5:20-5:24: error: Application type mismatch: In the appli
 the argument
   "hi"
 has type
-  String : Type
+  String
 but is expected to have type
-  Nat : Type
+  Nat
 bla sorry 5 : Nat
 nameArgErrorIssue.lean:6:20-6:24: error: Application type mismatch: In the application
   bla "hi"
 the argument
   "hi"
 has type
-  String : Type
+  String
 but is expected to have type
-  Nat : Type
+  Nat
 nameArgErrorIssue.lean:6:11-6:19: error: invalid argument name 'z' for function 'bla'
 nameArgErrorIssue.lean:7:11-7:19: error: invalid argument name 'z' for function 'bla'

tests/lean/namedHoles.lean.expected.out

@@ -3,9 +3,9 @@ namedHoles.lean:9:12-9:14: error: Application type mismatch: In the application
 the last
   ?x
 argument has type
-  Nat : Type
+  Nat
 but is expected to have type
-  Bool : Type
+  Bool
 f ?x sorry : Nat
 g ?x ?x : Nat
 20

tests/lean/phashmap_inst_coherence.lean.expected.out

@@ -3,6 +3,6 @@ phashmap_inst_coherence.lean:12:53-12:54: error: Application type mismatch: In t
 the argument
   m
 has type
-  @PersistentHashMap Nat Nat instBEqOfDecidableEq instHashableNat : Type
+  @PersistentHashMap Nat Nat instBEqOfDecidableEq instHashableNat
 but is expected to have type
-  @PersistentHashMap Nat Nat ?m natDiffHash : Type
+  @PersistentHashMap Nat Nat ?m natDiffHash

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 : Type
+  Nat → IO Unit
 but is expected to have type
-  IO PUnit : Type
+  IO PUnit
 pureCoeIssue.lean:14:2-14:7: error: type mismatch
   f2 10
 has type
-  Nat → IO Unit : Type
+  Nat → IO Unit
 but is expected to have type
-  IO PUnit : Type
+  IO PUnit

tests/lean/run/1870.lean

@@ -4,9 +4,9 @@ set_option pp.mvars false
 error: type mismatch
   congrArg ?_ (congrArg ?_ ?_)
 has type
-  ?_ (?_ ?_) = ?_ (?_ ?_) : Prop
+  ?_ (?_ ?_) = ?_ (?_ ?_)
 but is expected to have type
-  OfNat.ofNat 0 = OfNat.ofNat 1 : Prop
+  OfNat.ofNat 0 = OfNat.ofNat 1
 -/
 #guard_msgs in
 theorem ex1 : (@OfNat.ofNat Nat 0 Zero.toOfNat0) = @OfNat.ofNat Nat 1 One.toOfNat1 := by

tests/lean/run/2283.lean

@@ -35,9 +35,9 @@ set_option pp.mvars false
 error: type mismatch
   limit.π sorry sorry
 has type
-  sorry : Sort _
+  sorry
 but is expected to have type
-  limit f → sorry : Sort (imax (max (u + 1) (v + 1)) _)
+  limit f → sorry
 -/
 #guard_msgs in
 theorem pi_lift_π_apply {C : Type v} [Category.{v} C] (f : Functor' C (Type max v u)) :

tests/lean/run/4101.lean

@@ -8,9 +8,9 @@ Updated error message to show the elaborated term rather than `h✝`
 error: type mismatch, term
   hp
 after simplification has type
-  p : Prop
+  p
 but is expected to have type
-  p ∧ q : Prop
+  p ∧ q
 -/
 #guard_msgs in
 example (p q : Prop) (hp : p ∧ True) : p ∧ q ∧ True := by
@@ -20,9 +20,9 @@ example (p q : Prop) (hp : p ∧ True) : p ∧ q ∧ True := by
 error: type mismatch, term
   fun x => x
 after simplification has type
-  True : Prop
+  True
 but is expected to have type
-  False : Prop
+  False
 -/
 #guard_msgs in
 example : False := by

tests/lean/run/4318.lean

@@ -34,9 +34,9 @@ example (n : Nat) : 0 = 1 :=
 
 /--
 error: 'calc' expression has type
-  0 = 1 : Prop
+  0 = 1
 but is expected to have type
-  0 < 1 : Prop
+  0 < 1
 -/
 #guard_msgs in
 example : 0 < 1 :=
@@ -71,9 +71,9 @@ Tactic mode `calc`. Calc extension fails due to expected type mismatch, so repor
 -/
 /--
 error: 'calc' expression has type
-  0 < n - n : Prop
+  0 < n - n
 but is expected to have type
-  0 ≤ 1 : Prop
+  0 ≤ 1
 -/
 #guard_msgs in
 example (n : Nat) : 0 ≤ 1 := by

tests/lean/run/439.lean

@@ -53,9 +53,9 @@ error: Application type mismatch: In the application
 the argument
   p
 has type
-  P : Sort u
+  P
 but is expected to have type
-  Bar.fn ?_ : Sort _
+  Bar.fn ?_
 -/
 #guard_msgs in
 #check fn' p

tests/lean/run/4405.lean

@@ -8,9 +8,9 @@ error: Application type mismatch: In the application
 the argument
   Fin.is_lt ?_
 has type
-  ↑?_ < ?_ : Prop
+  ↑?_ < ?_
 but is expected to have type
-  ?_ n < ?_ n : Prop
+  ?_ n < ?_ n
 -/
 #guard_msgs in
 def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩
@@ -19,9 +19,9 @@ def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩
 error: type mismatch
   Fin.is_lt ?_
 has type
-  ↑?_ < ?_ : Prop
+  ↑?_ < ?_
 but is expected to have type
-  ?_ < ?_ : Prop
+  ?_ < ?_
 ---
 error: unsolved goals
 case a

tests/lean/run/4413.lean

@@ -18,9 +18,9 @@ theorem Note.self_containsNote_lowerSemitone_self (n : Note) :
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  n = n - 1 : Prop
+  n = n - 1
 -/
 #guard_msgs in
 set_option maxRecDepth 100 in

tests/lean/run/4670.lean

@@ -16,9 +16,9 @@ error: Application type mismatch: In the application
 the argument
   true
 has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Foo : Type
+  Foo
 ---
 info: sorry.out : Nat
 -/
@@ -34,9 +34,9 @@ error: Application type mismatch: In the application
 the argument
   true
 has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Foo : Type
+  Foo
 ---
 info: sorry.out' : Nat
 -/

tests/lean/run/4888.lean

@@ -10,9 +10,9 @@ error: Application type mismatch: In the application
 the argument
   True
 has type
-  Prop : Type
+  Prop
 but is expected to have type
-  Nat : Type
+  Nat
 -/
 #guard_msgs in
 theorem bug: True := by

tests/lean/run/4920.lean

@@ -11,16 +11,17 @@ set_option pp.mvars false
 error: type mismatch
   xm[i]
 has type
-  Vect m A : outParam (Type _)
+  Vect m A
 but is expected to have type
-  A : outParam (Type _)
+  A
 ---
 error: type mismatch, term
   ih
 after simplification has type
-  i < as.length : Prop
-but is expected to have type
-  ?_ : Type _
+  i < as.length
+of sort `Prop` but is expected to have type
+  ?_
+of sort `Type _`
 ---
 error: failed to prove index is valid, possible solutions:
   - Use `have`-expressions to prove the index is valid

tests/lean/run/7170.lean

@@ -73,9 +73,9 @@ def tooMany₃ : Foo → Foo → Prop
 error: type mismatch
   True
 has type
-  Prop : Type
+  Prop
 but is expected to have type
-  Foo → Prop : Type
+  Foo → Prop
 -/
 #guard_msgs in
 def tooFew₁ : Foo → Foo → Prop
@@ -196,9 +196,9 @@ error: Not enough patterns in match alternative: Expected 2, but found 1:
 error: type mismatch
   fun b => True
 has type
-  ?_ → Prop : Sort (max 1 _)
+  ?_ → Prop
 but is expected to have type
-  Prop : Type
+  Prop
 -/
 #guard_msgs in
 def matchTooFewFn : Foo → Foo → Prop := fun a b =>

tests/lean/run/DVec.lean

@@ -45,9 +45,10 @@ error: Application type mismatch: In the application
 the argument
   v
 has type
-  Vec Nat 1 : Type
-but is expected to have type
-  TypeVec (?_ + 1) : Type (_ + 1)
+  Vec Nat 1
+of sort `Type` but is expected to have type
+  TypeVec (?_ + 1)
+of sort `Type (_ + 1)`
 -/
 #guard_msgs in set_option pp.mvars false in
 example (v : Vec Nat 1) : Nat :=

tests/lean/run/addPPExplicitToExposeDiff.lean

@@ -10,9 +10,9 @@ Basic example.
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  1 = 2 : Prop
+  1 = 2
 -/
 #guard_msgs in example : 1 = 2 := by
   exact rfl
@@ -39,9 +39,9 @@ theorem test {f g : Nat → Nat} (n : Nat) (hfg : ∀ a, f (g a) = a) :
 error: type mismatch
   test n2 ?_
 has type
-  ?_ (?_ n2) = n2 : Prop
+  ?_ (?_ n2) = n2
 but is expected to have type
-  (fun x => x * 2) (g2 n2) = n2 : Prop
+  (fun x => x * 2) (g2 n2) = n2
 -/
 #guard_msgs in
 example {g2 : Nat → Nat} (n2 : Nat) : (fun x => x * 2) (g2 n2) = n2 := by
@@ -56,9 +56,9 @@ def f {a : Nat} (b : Nat) : Prop := a + b = 0
 error: type mismatch
   sorry
 has type
-  @f 0 ?_ : Prop
+  @f 0 ?_
 but is expected to have type
-  @f 1 2 : Prop
+  @f 1 2
 -/
 #guard_msgs in
 example : @f 1 2 := by
@@ -71,9 +71,9 @@ Add type ascriptions for numerals if they have different types.
 error: type mismatch
   Eq.refl 0
 has type
-  (0 : Int) = 0 : Prop
+  (0 : Int) = 0
 but is expected to have type
-  (0 : Nat) = 0 : Prop
+  (0 : Nat) = 0
 -/
 #guard_msgs in example : 0 = (0 : Nat) := by
   exact Eq.refl (0 : Int)
@@ -83,9 +83,9 @@ but is expected to have type
 error: type mismatch
   Eq.refl 1
 has type
-  (1 : Int) = 1 : Prop
+  (1 : Int) = 1
 but is expected to have type
-  (0 : Nat) = 0 : Prop
+  (0 : Nat) = 0
 -/
 #guard_msgs in example : 0 = (0 : Nat) := by
   exact Eq.refl (1 : Int)
@@ -98,9 +98,9 @@ local instance {α : Type _} [OfNat β n] : OfNat (α → β) n where
 error: type mismatch
   Eq.refl (0 1)
 has type
-  (0 : Nat → Int) 1 = 0 1 : Prop
+  (0 : Nat → Int) 1 = 0 1
 but is expected to have type
-  (0 : Nat → Nat) 1 = 0 1 : Prop
+  (0 : Nat → Nat) 1 = 0 1
 -/
 #guard_msgs in example : (0 : Nat → Nat) 1 = (0 : Nat → Nat) 1 := by
   exact Eq.refl ((0 : Nat → Int) 1)
@@ -113,9 +113,9 @@ Exposes differences in pi type domains
 error: type mismatch
   fun h => trivial
 has type
-  (1 : Int) = 1 → True : Prop
+  (1 : Int) = 1 → True
 but is expected to have type
-  (1 : Nat) = 1 → True : Prop
+  (1 : Nat) = 1 → True
 -/
 #guard_msgs in example : (1 : Nat) = 1 → True :=
   fun (h : (1 : Int) = 1) => trivial
@@ -127,9 +127,9 @@ Exposes differences in pi type codomains
 error: type mismatch
   fun h => rfl
 has type
-  True → (1 : Int) = 1 : Prop
+  True → (1 : Int) = 1
 but is expected to have type
-  True → (1 : Nat) = 1 : Prop
+  True → (1 : Nat) = 1
 -/
 #guard_msgs in example : True → (1 : Nat) = 1 :=
   (fun h => rfl : True → (1 : Int) = 1)
@@ -141,9 +141,9 @@ Exposes differences in fun domains
 error: type mismatch
   sorry
 has type
-  { x : Int // x > 0 } : Type
+  { x : Int // x > 0 }
 but is expected to have type
-  { x : Nat // x > 0 } : Type
+  { x : Nat // x > 0 }
 -/
 #guard_msgs in example : {x : Nat // x > 0} :=
   (sorry : {x : Int // x > 0})
@@ -155,9 +155,9 @@ Exposes differences in fun values
 error: type mismatch
   sorry
 has type
-  { x // @decide (p x) (d2 x) = true } : Type
+  { x // @decide (p x) (d2 x) = true }
 but is expected to have type
-  { x // @decide (p x) (d1 x) = true } : Type
+  { x // @decide (p x) (d1 x) = true }
 -/
 #guard_msgs in example (p : Nat → Prop) (d1 d2 : DecidablePred p) :
     {x : Nat // @decide _ (d1 x) = true} :=

tests/lean/run/allGoals.lean

@@ -39,16 +39,16 @@ There is no "unsolved goals" error.
 error: type mismatch
   Eq.refl 3
 has type
-  3 = 3 : Prop
+  3 = 3
 but is expected to have type
-  false = false : Prop
+  false = false
 ---
 error: type mismatch
   Eq.refl 3
 has type
-  3 = 3 : Prop
+  3 = 3
 but is expected to have type
-  true = true : Prop
+  true = true
 -/
 #guard_msgs in
 example (b : Bool) : b = b := by
@@ -64,9 +64,9 @@ Even if at least one succeeds, the entire tactic fails if any fails, stopping th
 error: type mismatch
   Eq.refl true
 has type
-  true = true : Prop
+  true = true
 but is expected to have type
-  false = false : Prop
+  false = false
 -/
 #guard_msgs in
 example (b : Bool) : b = b := by
@@ -120,9 +120,9 @@ On error, failing goals are admitted. There is one `sorry` in the proof term cor
 error: type mismatch
   Eq.refl true
 has type
-  true = true : Prop
+  true = true
 but is expected to have type
-  false = false : Prop
+  false = false
 ---
 info: Try this: Bool.casesOn (motive := fun t => b = t → b = b) b (fun h => Eq.symm h ▸ sorry)
   (fun h => Eq.symm h ▸ Eq.refl true) (Eq.refl b)
@@ -184,9 +184,9 @@ elab "without_recover " tac:tactic : tactic => do
 error: type mismatch
   Eq.refl 3
 has type
-  3 = 3 : Prop
+  3 = 3
 but is expected to have type
-  false = false : Prop
+  false = false
 -/
 #guard_msgs in
 example (b : Bool) : b = b := by

tests/lean/run/autoLift.lean

@@ -22,9 +22,9 @@ set_option pp.mvars false in
 info: type mismatch
   f
 has type
-  IO Nat : Type
+  IO Nat
 but is expected to have type
-  M ?_ : Type
+  M ?_
 ---
 info: id do
   let a ← sorry

tests/lean/run/check.lean

@@ -38,9 +38,10 @@ error: Application type mismatch: In the application
 the argument
   Nat
 has type
-  Type : Type 1
-but is expected to have type
-  Prop : Type
+  Type
+of sort `Type 1` but is expected to have type
+  Prop
+of sort `Type`
 -/
 #guard_msgs in #check elab_1eq1
 
@@ -50,9 +51,10 @@ error: Application type mismatch: In the application
 the argument
   Nat
 has type
-  Type : Type 1
-but is expected to have type
-  Prop : Type
+  Type
+of sort `Type 1` but is expected to have type
+  Prop
+of sort `Type`
 -/
 #guard_msgs in #reduce elab_1eq1
 end

tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean

@@ -5,9 +5,9 @@ error: Application type mismatch: In the application
 the last
   true
 argument has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat
 -/
 #guard_msgs in
 #eval foo 1 true true 1

tests/lean/run/elabLet.lean

@@ -120,9 +120,9 @@ example (p : Nat × Nat) : True :=
 error: type mismatch
   jp ()
 has type
-  IO (IO.Ref Bool) : Type
+  IO (IO.Ref Bool)
 but is expected to have type
-  IO Unit : Type
+  IO Unit
 -/
 #guard_msgs in
 def f (x : Nat) : IO Unit :=
@@ -138,9 +138,9 @@ def f (x : Nat) : IO Unit :=
 error: type mismatch
   IO.mkRef true
 has type
-  BaseIO (IO.Ref Bool) : Type
+  BaseIO (IO.Ref Bool)
 but is expected to have type
-  IO Unit : Type
+  IO Unit
 -/
 #guard_msgs in
 def f' (x : Nat) : IO Unit :=

tests/lean/run/exposeDiff.lean

@@ -14,9 +14,10 @@ example (x : PUnit.{1}) : PUnit.{0} := by
 error: type mismatch
   x
 has type
-  PUnit.{1} : Type
-but is expected to have type
-  PUnit.{0} : Prop
+  PUnit.{1}
+of sort `Type` but is expected to have type
+  PUnit.{0}
+of sort `Prop`
 -/
 #guard_msgs in
 example (x : PUnit.{1}) : PUnit.{0} :=

tests/lean/run/fin_coercions.lean

@@ -7,9 +7,9 @@ set_option pp.mvars false
 error: type mismatch
   n
 has type
-  Nat : Type
+  Nat
 but is expected to have type
-  Fin 3 : Type
+  Fin 3
 ---
 info: fun n => sorry : (n : Nat) → ?_ n
 -/

tests/lean/run/haveTactic.lean

@@ -9,9 +9,9 @@ If the body of a `have` fails to elaborate, the tactic completes with a `sorry`
 error: type mismatch
   False.elim
 has type
-  False → ?m.6 : Sort ?u.5
+  False → ?m.6
 but is expected to have type
-  True : Prop
+  True
 ---
 trace: h : True
 ⊢ True

tests/lean/run/issue8213.lean

@@ -21,9 +21,9 @@ error: Failed to realize constant myTest.fun_cases:
       the argument
         h_1
       has type
-        (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
+        (a : α) → (dc : List α) → x = a :: dc → mmotive (a :: dc)
       but is expected to have type
-        (a : α) → (dc : List α) → x✝ = a :: dc → mmotive (a :: dc) : Sort (imax (u_1 + 1) (u_1 + 1) v)
+        (a : α) → (dc : List α) → x✝ = a :: dc → mmotive (a :: dc)
 ---
 error: unknown identifier 'myTest.fun_cases'
 -/

tests/lean/run/mergeSort.lean

@@ -52,9 +52,9 @@ error: could not synthesize default value for parameter 'le' using tactics
 error: type mismatch
   a ≤ b
 has type
-  Prop : Type
+  Prop
 but is expected to have type
-  Bool : Type
+  Bool
 -/
 #guard_msgs in
 example : mergeSort [UndecidableLE.mk] = [UndecidableLE.mk] := sorry

tests/lean/run/partial_fixpoint_explicit.lean

@@ -31,9 +31,10 @@ partial_fixpoint monotonicity fun _ _ a _ => a _
 error: type mismatch
   ()
 has type
-  Unit : Type
-but is expected to have type
-  Lean.Order.monotone fun f x => f (x + 1) : Prop
+  Unit
+of sort `Type` but is expected to have type
+  Lean.Order.monotone fun f x => f (x + 1)
+of sort `Prop`
 -/
 #guard_msgs in
 def nullary2 (x : Nat) : Option Unit := nullary2 (x + 1)

tests/lean/run/premise_selection.lean

@@ -4,9 +4,10 @@ import Lean.PremiseSelection
 error: type mismatch
   Nat
 has type
-  Type : Type 1
-but is expected to have type
-  Lean.PremiseSelection.Selector : Type
+  Type
+of sort `Type 1` but is expected to have type
+  Lean.PremiseSelection.Selector
+of sort `Type`
 ---
 error: Failed to elaborate Nat as a `MVarId → Config → MetaM (Array Suggestion)`.
 -/

tests/lean/run/proofAsSorry.lean

@@ -5,9 +5,9 @@ set_option pp.mvars false
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  2 + 2 = 5 : Prop
+  2 + 2 = 5
 -/
 #guard_msgs in
 example : 2 + 2 = 5 := rfl -- This is not a theorem

tests/lean/run/scopedLocalReducibility.lean

@@ -5,9 +5,9 @@ set_option pp.mvars false
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  f x = x + 1 : Prop
+  f x = x + 1
 -/
 #guard_msgs in
 example : f x = x + 1 :=
@@ -23,9 +23,9 @@ end
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  f x = x + 1 : Prop
+  f x = x + 1
 -/
 #guard_msgs in
 example : f x = x + 1 :=
@@ -39,9 +39,9 @@ end Boo
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  f x = x + 1 : Prop
+  f x = x + 1
 -/
 #guard_msgs in
 example : f x = x + 1 :=
@@ -55,9 +55,9 @@ example : f x = x + 1 :=
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  f x = x + 1 : Prop
+  f x = x + 1
 -/
 #guard_msgs in
 example : f x = x + 1 :=

tests/lean/run/scopedunifhint.lean

@@ -33,9 +33,9 @@ error: Application type mismatch: In the application
 the argument
   x
 has type
-  Nat : Type
+  Nat
 but is expected to have type
-  Magma.α ?_ : Type _
+  Magma.α ?_
 -/
 #guard_msgs in
 #check mul x x           -- Error: unification hint is not active
@@ -46,9 +46,9 @@ error: Application type mismatch: In the application
 the argument
   (x, x)
 has type
-  Nat × Nat : Type
+  Nat × Nat
 but is expected to have type
-  Magma.α ?_ : Type _
+  Magma.α ?_
 -/
 #guard_msgs in
 #check mul (x, x) (x, x) -- Error: no unification hint
@@ -61,9 +61,9 @@ error: Application type mismatch: In the application
 the argument
   x
 has type
-  Nat : Type
+  Nat
 but is expected to have type
-  Magma.α ?_ : Type _
+  Magma.α ?_
 -/
 #guard_msgs in
 #check x*x -- Error: unification hint is not active
@@ -79,9 +79,9 @@ error: Application type mismatch: In the application
 the argument
   (x, x)
 has type
-  Nat × Nat : Type
+  Nat × Nat
 but is expected to have type
-  Magma.α ?_ : Type _
+  Magma.α ?_
 -/
 #guard_msgs in
 #check mul (x, x) (x, x) -- still error
@@ -107,9 +107,9 @@ error: Application type mismatch: In the application
 the argument
   (x, x)
 has type
-  Nat × Nat : Type
+  Nat × Nat
 but is expected to have type
-  Magma.α ?_ : Type _
+  Magma.α ?_
 -/
 #guard_msgs in
 #check (x, x) * (x, x) -- error, local hint is not active after end of section anymore

tests/lean/run/sealCommand.lean

@@ -8,9 +8,9 @@ example : f x = x + 1 := rfl
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  f x = x + 1 : Prop
+  f x = x + 1
 -/
 #guard_msgs in
 seal f in
@@ -24,9 +24,9 @@ seal f
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  f x = x + 1 : Prop
+  f x = x + 1
 -/
 #guard_msgs in
 example : f x = x + 1 := rfl

tests/lean/run/sorry.lean

@@ -50,9 +50,9 @@ If `sorry` is used for a function type, then one gets a family of unique `sorry`
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  f 0 1 = f 0 0 : Prop
+  f 0 1 = f 0 0
 -/
 #guard_msgs in example : f 0 1 = f 0 0 := rfl
 
@@ -70,9 +70,9 @@ Showing source position when surfacing differences.
 error: type mismatch
   sorry
 has type
-  sorry `«sorry:77:43» : Sort _
+  sorry `«sorry:77:43»
 but is expected to have type
-  sorry `«sorry:77:25» : Sort _
+  sorry `«sorry:77:25»
 -/
 #guard_msgs in example : sorry := (sorry : sorry)
 

tests/lean/run/tactic_config.lean

@@ -197,9 +197,9 @@ Elaboration errors cause the tactic to use the default configuration.
 error: type mismatch
   false
 has type
-  Bool : Type
+  Bool
 but is expected to have type
-  B : Type
+  B
 ---
 info: config is { b := { toA := { x := true } } }
 ---
@@ -239,9 +239,9 @@ elab "my_command" cfg:Parser.Tactic.optConfig : command => do
 error: type mismatch
   true
 has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat
 ---
 info: config is { x := 0, y := false }
 -/

tests/lean/run/variable.lean

@@ -143,9 +143,10 @@ error: Application type mismatch: In the application
 the argument
   True
 has type
-  Prop : Type
-but is expected to have type
-  Type _ : Type (_ + 1)
+  Prop
+of sort `Type` but is expected to have type
+  Type _
+of sort `Type (_ + 1)`
 -/
 #guard_msgs in
 omit [ToString True]

tests/lean/run/wfirred.lean

@@ -13,9 +13,9 @@ termination_by n => n
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  foo 0 = 0 : Prop
+  foo 0 = 0
 -/
 #guard_msgs in
 example : foo 0 = 0 := rfl
@@ -24,9 +24,9 @@ example : foo 0 = 0 := rfl
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  foo (n + 1) = foo n : Prop
+  foo (n + 1) = foo n
 -/
 #guard_msgs in
 example : foo (n+1) = foo n := rfl
@@ -64,9 +64,9 @@ unseal foo
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  foo 0 = 0 : Prop
+  foo 0 = 0
 -/
 #guard_msgs in
 example : foo 0 = 0 := rfl
@@ -75,9 +75,9 @@ example : foo 0 = 0 := rfl
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  foo (n + 1) = foo n : Prop
+  foo (n + 1) = foo n
 -/
 #guard_msgs in
 example : foo (n+1) = foo n := rfl
@@ -90,9 +90,9 @@ end Unsealed
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  foo 0 = 0 : Prop
+  foo 0 = 0
 -/
 #guard_msgs in
 example : foo 0 = 0 := rfl
@@ -110,9 +110,9 @@ termination_by n => n
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  foo = bar : Prop
+  foo = bar
 -/
 #guard_msgs in
 example : foo = bar := rfl
@@ -134,9 +134,9 @@ seal baz in
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  baz 0 = 0 : Prop
+  baz 0 = 0
 -/
 #guard_msgs in
 example : baz 0 = 0 := rfl
@@ -156,9 +156,9 @@ seal quux in
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  quux 0 = 0 : Prop
+  quux 0 = 0
 -/
 #guard_msgs in
 example : quux 0 = 0 := rfl

tests/lean/server/content_diag.json

@@ -31,7 +31,7 @@
     {"start": {"line": 14, "character": 31},
      "end": {"line": 14, "character": 40}},
     "message":
-    "type mismatch\n  \"NotANat\"\nhas type\n  String : Type\nbut is expected to have type\n  Nat : Type",
+    "type mismatch\n  \"NotANat\"\nhas type\n  String\nbut is expected to have type\n  Nat",
     "fullRange":
     {"start": {"line": 14, "character": 31},
      "end": {"line": 14, "character": 40}}},
@@ -54,4 +54,4 @@
     {"start": {"line": 24, "character": 0},
      "end": {"line": 24, "character": 6}}}]},
  "method": "textDocument/publishDiagnostics",
- "jsonrpc": "2.0"}
+ "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✝ : Prop
+  x✝ = x✝
 but is expected to have type
-  x = x : Prop
+  x = x
 shadow.lean:10:0-10:1: error: type mismatch
   h
 has type
-  x = x : Prop
+  x = x
 but is expected to have type
-  x = x : Prop
+  x = x
 shadow.lean:13:0-13:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1

tests/lean/simpArgTypeMismatch.lean.expected.out

@@ -3,6 +3,7 @@ simpArgTypeMismatch.lean:3:29-3:33: error: Application type mismatch: In the app
 the argument
   Unit
 has type
-  Type : Type 1
-but is expected to have type
-  ¬?m : Prop
+  Type
+of sort `Type 1` but is expected to have type
+  ¬?m
+of sort `Prop`

tests/lean/sorryAtError.lean.expected.out

@@ -3,6 +3,6 @@ sorryAtError.lean:13:46-13:47: error: Application type mismatch: In the applicat
 the argument
   Γ
 has type
-  x.ty.ctx : Type
+  x.ty.ctx
 but is expected to have type
-  ty.ctx : Type
+  ty.ctx

tests/lean/struct1.lean.expected.out

@@ -8,24 +8,24 @@ struct1.lean:15:28-15:33: warning: field 'x' from 'B' has already been declared
 struct1.lean:16:1-16:2: error: field 'x' has been declared in parent structure
 struct1.lean:17:30-17:35: warning: duplicate parent structure 'A', skipping
 struct1.lean:19:27-19:33: error: field type mismatch, field 'x' from parent 'B' has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat
 struct1.lean:30:1-30:2: error: field 'x' has already been declared
 struct1.lean:33:1-33:2: error: field 'x' has been declared in parent structure
 struct1.lean:36:6-36:10: error: type mismatch
   true
 has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat
 struct1.lean:39:5-39:9: error: omit field 'x' type to set default value
 struct1.lean:42:12-42:16: error: type mismatch
   true
 has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat
 struct1.lean:45:0-45:13: error: invalid 'private' constructor in a 'private' structure
 struct1.lean:48:0-48:15: error: invalid 'protected' constructor in a 'private' structure
 struct1.lean:51:0-51: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 : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat

tests/lean/typeIncorrectPat.lean.expected.out

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

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 : Type
+  IO Unit
 but is expected to have type
-  IO Nat : Type
+  IO Nat
 typeMismatch.lean:12:0-12:16: error: type mismatch
   Meta.isDefEq x x
 has type
-  MetaM Bool : Type
+  MetaM Bool
 but is expected to have type
-  MetaM Unit : Type
+  MetaM Unit

tests/lean/typeOf.lean.expected.out

@@ -7,10 +7,10 @@ typeOf.lean:12:0-12:5: error: failed to synthesize
 
 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat
 typeOf.lean:29:55-29:59: error: natural number expected, value has type
-  Bool : Type
+  Bool
 but is expected to have type
-  Nat : Type
+  Nat

tests/pkg/builtin_attr/UserAttr/Tst.lean

@@ -10,9 +10,9 @@ set_option pp.mvars false
 error: type mismatch
   rfl
 has type
-  ?_ = ?_ : Prop
+  ?_ = ?_
 but is expected to have type
-  myFun x = x + 1 : Prop
+  myFun x = x + 1
 -/
 #guard_msgs in
 example : myFun x = x + 1 :=

tests/pkg/module/Module/Basic.lean

@@ -20,9 +20,9 @@ public theorem t : f = 1 := testSorry
 error: type mismatch
   y
 has type
-  Vector Unit 1 : Type
+  Vector Unit 1
 but is expected to have type
-  Vector Unit f : Type
+  Vector Unit f
 -/
 #guard_msgs in
 public theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := testSorry

tests/pkg/module/Module/ImportedAll.lean

@@ -16,9 +16,9 @@ testSorry
 error: type mismatch
   y
 has type
-  Vector Unit 1 : Type
+  Vector Unit 1
 but is expected to have type
-  Vector Unit f : Type
+  Vector Unit f
 -/
 #guard_msgs in
 public theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := sorry