chore: improve for type mismatch error message

src/Lean/Elab/Do.lean

@@ -937,7 +937,7 @@ partial def doSeqToCode : List Syntax → M CodeBlock
       uvarsTuple ← liftMacroM $ mkTuple ref (uvars.map (mkIdentFrom ref));
       auxDo ← if isForInMap then do
         forInTerm ← `($(xs).forInMap $uvarsTuple fun $x $uvarsTuple => $forInBody);
-        `(do let r ← $forInTerm; $uvarsTuple:term := r.2; return r.1)
+        `(do let r ← $forInTerm; $uvarsTuple:term := r.2; return ensureExpectedType! "type mismatch, 'for'" r.1)
       else do {
         forInTerm ← `($(xs).forIn $uvarsTuple fun $x $uvarsTuple => $forInBody);
         `(do let r ← $forInTerm; $uvarsTuple:term := r)

src/Lean/Elab/Term.lean

@@ -526,7 +526,7 @@ def mkTypeMismatchError (header? : Option String) (e : Expr) (eType : Expr) (exp
 let header : MessageData := match header? with
   | some header => header ++ " has type"
   | none        => "type mismatch" ++ indentExpr e ++ Format.line ++ "has type";
-header ++ indentExpr eType ++ Format.line ++ "but it is expected to have type" ++ indentExpr expectedType
+header ++ indentExpr eType ++ Format.line ++ "but is expected to have type" ++ indentExpr expectedType
 
 def throwTypeMismatchError {α} (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr)
     (f? : Option Expr := none) (extraMsg? : Option MessageData := none) : TermElabM α :=

tests/lean/doNotation1.lean.expected.out

@@ -2,21 +2,17 @@ doNotation1.lean:4:0: error: 'y' cannot be reassigned
 doNotation1.lean:8:2: error: 'y' cannot be reassigned
 doNotation1.lean:20:7: error: invalid reassignment, value has type
   Vector Nat (n + 1)
-but it is expected to have type
+but is expected to have type
   Vector Nat n
 failed to synthesize instance
   CoeT (Vector Nat (n + 1)) (Vector.cons 1 v) (Vector Nat n)
 doNotation1.lean:25:7: error: invalid reassignment, value has type
   Bool
-but it is expected to have type
+but is expected to have type
   Nat
 failed to synthesize instance
   CoeT Bool true Nat
-doNotation1.lean:24:0: error: application type mismatch
-  pure r✝.fst
-argument
-  r✝.fst
-has type
+doNotation1.lean:24:0: error: type mismatch, 'for' has type
   List Nat
 but is expected to have type
   List Bool

tests/lean/typeOf.lean.expected.out

@@ -20,13 +20,13 @@ failed to synthesize instance
   CoeT Bool r Nat
 typeOf.lean:20:54: error: invalid reassignment, term has type
   Bool
-but it is expected to have type
+but is expected to have type
   Nat
 failed to synthesize instance
   CoeT Bool (y == 1) Nat
 typeOf.lean:29:53: error: natural number expected, value has type
   Bool
-but it is expected to have type
+but is expected to have type
   Nat
 failed to synthesize instance
   CoeT Bool true Nat