From 8424ddbb3edf4c3b440d0c4e1216e3ebf19bdaf4 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 1 Jul 2025 09:50:53 +0200 Subject: [PATCH] feat: prettier expected type mismatch error message (#9099) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR improves the “expected type mismatch” error message by omitting the type's types when they are defeq, and putting them into separate lines when not. I found it rather tediuos to parse the error message when the expected type is long, because I had to find the `:` in the middle of a large expression somewhere. Also, when both are of sort `Prop` or `Type` it doesn't add much value to print the sort (and it’s only one hover away anyways). --- src/Lean/Meta/Basic.lean | 32 +++++++++++++++ src/Lean/Meta/Check.lean | 30 +++++++++----- src/Lean/PrettyPrinter.lean | 29 +------------- tests/lean/1057.lean.expected.out | 4 +- tests/lean/1081.lean.expected.out | 8 ++-- tests/lean/1433.lean.expected.out | 4 +- tests/lean/243.lean.expected.out | 8 ++-- tests/lean/283.lean.expected.out | 7 ++-- tests/lean/389.lean.expected.out | 4 +- tests/lean/423.lean.expected.out | 28 +++++++------ tests/lean/755.lean.expected.out | 16 ++++---- tests/lean/autoPPExplicit.lean.expected.out | 7 ++-- .../lean/binrelTypeMismatch.lean.expected.out | 12 +++--- tests/lean/calcErrors.lean.expected.out | 4 +- tests/lean/diamond1.lean.expected.out | 4 +- tests/lean/doErrorMsg.lean.expected.out | 24 +++++------ tests/lean/doIssue.lean.expected.out | 12 +++--- tests/lean/doNotation1.lean.expected.out | 24 +++++------ tests/lean/elseifDoErrorPos.lean.expected.out | 8 ++-- tests/lean/etaStructIssue.lean.expected.out | 4 +- tests/lean/evalSorry.lean.expected.out | 4 +- tests/lean/have.lean.expected.out | 4 +- tests/lean/inductive1.lean.expected.out | 4 +- tests/lean/isDefEqOffsetBug.lean.expected.out | 4 +- tests/lean/macroSwizzle.lean.expected.out | 4 +- tests/lean/match1.lean.expected.out | 4 +- .../lean/matchErrorLocation.lean.expected.out | 7 ++-- tests/lean/modBug.lean.expected.out | 4 +- .../motiveNotTypeCorect.lean.expected.out | 4 +- .../mulcommErrorMessage.lean.expected.out | 12 +++--- .../lean/nameArgErrorIssue.lean.expected.out | 8 ++-- tests/lean/namedHoles.lean.expected.out | 4 +- .../phashmap_inst_coherence.lean.expected.out | 4 +- tests/lean/pureCoeIssue.lean.expected.out | 8 ++-- tests/lean/run/1870.lean | 4 +- tests/lean/run/2283.lean | 4 +- tests/lean/run/4101.lean | 8 ++-- tests/lean/run/4318.lean | 8 ++-- tests/lean/run/439.lean | 4 +- tests/lean/run/4405.lean | 8 ++-- tests/lean/run/4413.lean | 4 +- tests/lean/run/4670.lean | 8 ++-- tests/lean/run/4888.lean | 4 +- tests/lean/run/4920.lean | 11 ++--- tests/lean/run/7170.lean | 8 ++-- tests/lean/run/DVec.lean | 7 ++-- tests/lean/run/addPPExplicitToExposeDiff.lean | 40 +++++++++---------- tests/lean/run/allGoals.lean | 20 +++++----- tests/lean/run/autoLift.lean | 4 +- tests/lean/run/check.lean | 14 ++++--- ...icatedArgumentApplicationTypeMismatch.lean | 4 +- tests/lean/run/elabLet.lean | 8 ++-- tests/lean/run/exposeDiff.lean | 7 ++-- tests/lean/run/fin_coercions.lean | 4 +- tests/lean/run/haveTactic.lean | 4 +- tests/lean/run/issue8213.lean | 4 +- tests/lean/run/mergeSort.lean | 4 +- tests/lean/run/partial_fixpoint_explicit.lean | 7 ++-- tests/lean/run/premise_selection.lean | 7 ++-- tests/lean/run/proofAsSorry.lean | 4 +- tests/lean/run/scopedLocalReducibility.lean | 16 ++++---- tests/lean/run/scopedunifhint.lean | 20 +++++----- tests/lean/run/sealCommand.lean | 8 ++-- tests/lean/run/sorry.lean | 8 ++-- tests/lean/run/tactic_config.lean | 8 ++-- tests/lean/run/variable.lean | 7 ++-- tests/lean/run/wfirred.lean | 32 +++++++-------- tests/lean/server/content_diag.json | 4 +- tests/lean/shadow.lean.expected.out | 8 ++-- .../simpArgTypeMismatch.lean.expected.out | 7 ++-- tests/lean/sorryAtError.lean.expected.out | 4 +- tests/lean/struct1.lean.expected.out | 12 +++--- tests/lean/structDefault.lean.expected.out | 4 +- tests/lean/typeIncorrectPat.lean.expected.out | 4 +- tests/lean/typeMismatch.lean.expected.out | 8 ++-- tests/lean/typeOf.lean.expected.out | 8 ++-- tests/pkg/builtin_attr/UserAttr/Tst.lean | 4 +- tests/pkg/module/Module/Basic.lean | 4 +- tests/pkg/module/Module/ImportedAll.lean | 4 +- 79 files changed, 376 insertions(+), 347 deletions(-) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 57406a4242..a86e48f923 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 := "", 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 diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean index a5c1b6937b..1d76954880 100644 --- a/src/Lean/Meta/Check.lean +++ b/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 diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index e975626230..b33fc44fe5 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/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 := "", 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 diff --git a/tests/lean/1057.lean.expected.out b/tests/lean/1057.lean.expected.out index 8845b294b4..451e074ae8 100644 --- a/tests/lean/1057.lean.expected.out +++ b/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✝ diff --git a/tests/lean/1081.lean.expected.out b/tests/lean/1081.lean.expected.out index 4afda1a68a..f726a7e398 100644 --- a/tests/lean/1081.lean.expected.out +++ b/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 diff --git a/tests/lean/1433.lean.expected.out b/tests/lean/1433.lean.expected.out index cfe2d65032..a4e26bd325 100644 --- a/tests/lean/1433.lean.expected.out +++ b/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 diff --git a/tests/lean/243.lean.expected.out b/tests/lean/243.lean.expected.out index 68c3dff208..91a312f473 100644 --- a/tests/lean/243.lean.expected.out +++ b/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 diff --git a/tests/lean/283.lean.expected.out b/tests/lean/283.lean.expected.out index d8b534b351..950e241514 100644 --- a/tests/lean/283.lean.expected.out +++ b/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` diff --git a/tests/lean/389.lean.expected.out b/tests/lean/389.lean.expected.out index 11368e25f3..17310eb6b3 100644 --- a/tests/lean/389.lean.expected.out +++ b/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 diff --git a/tests/lean/423.lean.expected.out b/tests/lean/423.lean.expected.out index c40e75e03e..90a7c76d8a 100644 --- a/tests/lean/423.lean.expected.out +++ b/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` diff --git a/tests/lean/755.lean.expected.out b/tests/lean/755.lean.expected.out index 3239108018..f78d9d9401 100644 --- a/tests/lean/755.lean.expected.out +++ b/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 diff --git a/tests/lean/autoPPExplicit.lean.expected.out b/tests/lean/autoPPExplicit.lean.expected.out index 42f0d7836f..9194a19a71 100644 --- a/tests/lean/autoPPExplicit.lean.expected.out +++ b/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` diff --git a/tests/lean/binrelTypeMismatch.lean.expected.out b/tests/lean/binrelTypeMismatch.lean.expected.out index 793bbfdaea..859e7ced42 100644 --- a/tests/lean/binrelTypeMismatch.lean.expected.out +++ b/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 diff --git a/tests/lean/calcErrors.lean.expected.out b/tests/lean/calcErrors.lean.expected.out index 5eb86903c7..4d59e690f0 100644 --- a/tests/lean/calcErrors.lean.expected.out +++ b/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 diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out index f9c0e4d3a3..e4f5da1028 100644 --- a/tests/lean/diamond1.lean.expected.out +++ b/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: diff --git a/tests/lean/doErrorMsg.lean.expected.out b/tests/lean/doErrorMsg.lean.expected.out index 78835753d3..93b3a8ec20 100644 --- a/tests/lean/doErrorMsg.lean.expected.out +++ b/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 diff --git a/tests/lean/doIssue.lean.expected.out b/tests/lean/doIssue.lean.expected.out index 73cc58de9f..e1bf7c0a29 100644 --- a/tests/lean/doIssue.lean.expected.out +++ b/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 diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out index f4a19e87bf..8787eeafa0 100644 --- a/tests/lean/doNotation1.lean.expected.out +++ b/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 diff --git a/tests/lean/elseifDoErrorPos.lean.expected.out b/tests/lean/elseifDoErrorPos.lean.expected.out index c85affabed..2757c136e1 100644 --- a/tests/lean/elseifDoErrorPos.lean.expected.out +++ b/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 diff --git a/tests/lean/etaStructIssue.lean.expected.out b/tests/lean/etaStructIssue.lean.expected.out index 450aa6e48d..3f47a5559d 100644 --- a/tests/lean/etaStructIssue.lean.expected.out +++ b/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₂ diff --git a/tests/lean/evalSorry.lean.expected.out b/tests/lean/evalSorry.lean.expected.out index 403b7e91d7..0d5a2088f3 100644 --- a/tests/lean/evalSorry.lean.expected.out +++ b/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. diff --git a/tests/lean/have.lean.expected.out b/tests/lean/have.lean.expected.out index bf1f9f98a4..9c657e3398 100644 --- a/tests/lean/have.lean.expected.out +++ b/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 diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out index f57eadef73..f05dbe1f27 100644 --- a/tests/lean/inductive1.lean.expected.out +++ b/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 diff --git a/tests/lean/isDefEqOffsetBug.lean.expected.out b/tests/lean/isDefEqOffsetBug.lean.expected.out index 66016501e9..6d7291fb55 100644 --- a/tests/lean/isDefEqOffsetBug.lean.expected.out +++ b/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 diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out index b399775303..0fc34dd699 100644 --- a/tests/lean/macroSwizzle.lean.expected.out +++ b/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 diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out index 8c86f83615..8334f1a283 100644 --- a/tests/lean/match1.lean.expected.out +++ b/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) diff --git a/tests/lean/matchErrorLocation.lean.expected.out b/tests/lean/matchErrorLocation.lean.expected.out index bd96fc0c49..72a21329b2 100644 --- a/tests/lean/matchErrorLocation.lean.expected.out +++ b/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` diff --git a/tests/lean/modBug.lean.expected.out b/tests/lean/modBug.lean.expected.out index 59dc8d648c..a0e5aacdde 100644 --- a/tests/lean/modBug.lean.expected.out +++ b/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 diff --git a/tests/lean/motiveNotTypeCorect.lean.expected.out b/tests/lean/motiveNotTypeCorect.lean.expected.out index 17346b81c8..5ad40f219a 100644 --- a/tests/lean/motiveNotTypeCorect.lean.expected.out +++ b/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. diff --git a/tests/lean/mulcommErrorMessage.lean.expected.out b/tests/lean/mulcommErrorMessage.lean.expected.out index 35ba3fa7d2..8b1800e9c0 100644 --- a/tests/lean/mulcommErrorMessage.lean.expected.out +++ b/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 diff --git a/tests/lean/nameArgErrorIssue.lean.expected.out b/tests/lean/nameArgErrorIssue.lean.expected.out index d8e8eabc97..bc894ade81 100644 --- a/tests/lean/nameArgErrorIssue.lean.expected.out +++ b/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' diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out index 4e3f66b468..e9bf382860 100644 --- a/tests/lean/namedHoles.lean.expected.out +++ b/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 diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out index c07a90156a..4c2b8d2696 100644 --- a/tests/lean/phashmap_inst_coherence.lean.expected.out +++ b/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 diff --git a/tests/lean/pureCoeIssue.lean.expected.out b/tests/lean/pureCoeIssue.lean.expected.out index 65337b027a..08f5e00d23 100644 --- a/tests/lean/pureCoeIssue.lean.expected.out +++ b/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 diff --git a/tests/lean/run/1870.lean b/tests/lean/run/1870.lean index 60ec2d2e12..439b691ef5 100644 --- a/tests/lean/run/1870.lean +++ b/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 diff --git a/tests/lean/run/2283.lean b/tests/lean/run/2283.lean index 6b31a0e3e5..ec0381a8e9 100644 --- a/tests/lean/run/2283.lean +++ b/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)) : diff --git a/tests/lean/run/4101.lean b/tests/lean/run/4101.lean index 4df97ce7c1..4a3454cfe0 100644 --- a/tests/lean/run/4101.lean +++ b/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 diff --git a/tests/lean/run/4318.lean b/tests/lean/run/4318.lean index f67d57979d..648411f339 100644 --- a/tests/lean/run/4318.lean +++ b/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 diff --git a/tests/lean/run/439.lean b/tests/lean/run/439.lean index a5a2894f86..e53b2e7ed5 100644 --- a/tests/lean/run/439.lean +++ b/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 diff --git a/tests/lean/run/4405.lean b/tests/lean/run/4405.lean index 6178bba1f8..eb52f12a45 100644 --- a/tests/lean/run/4405.lean +++ b/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 diff --git a/tests/lean/run/4413.lean b/tests/lean/run/4413.lean index 8690181126..911ac848d2 100644 --- a/tests/lean/run/4413.lean +++ b/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 diff --git a/tests/lean/run/4670.lean b/tests/lean/run/4670.lean index e78e788e9f..3ee0d58b7c 100644 --- a/tests/lean/run/4670.lean +++ b/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 -/ diff --git a/tests/lean/run/4888.lean b/tests/lean/run/4888.lean index 3a34394da7..10f6e0c01b 100644 --- a/tests/lean/run/4888.lean +++ b/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 diff --git a/tests/lean/run/4920.lean b/tests/lean/run/4920.lean index a6faee7512..9b491b811e 100644 --- a/tests/lean/run/4920.lean +++ b/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 diff --git a/tests/lean/run/7170.lean b/tests/lean/run/7170.lean index ad3b0ca4cc..55d8b3c6c7 100644 --- a/tests/lean/run/7170.lean +++ b/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 => diff --git a/tests/lean/run/DVec.lean b/tests/lean/run/DVec.lean index fcc1a1673d..b542733a67 100644 --- a/tests/lean/run/DVec.lean +++ 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 := diff --git a/tests/lean/run/addPPExplicitToExposeDiff.lean b/tests/lean/run/addPPExplicitToExposeDiff.lean index 328ca3d68e..5559d2a194 100644 --- a/tests/lean/run/addPPExplicitToExposeDiff.lean +++ b/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} := diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean index e22071c184..102d142b9b 100644 --- a/tests/lean/run/allGoals.lean +++ b/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 diff --git a/tests/lean/run/autoLift.lean b/tests/lean/run/autoLift.lean index a054b2c6d8..68cbc41a7f 100644 --- a/tests/lean/run/autoLift.lean +++ b/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 diff --git a/tests/lean/run/check.lean b/tests/lean/run/check.lean index 8c9b58643e..755f44d20b 100644 --- a/tests/lean/run/check.lean +++ b/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 diff --git a/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean b/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean index af0b39f639..e12e83eb7b 100644 --- a/tests/lean/run/duplicatedArgumentApplicationTypeMismatch.lean +++ b/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 diff --git a/tests/lean/run/elabLet.lean b/tests/lean/run/elabLet.lean index 96dbd7318a..054aca3d08 100644 --- a/tests/lean/run/elabLet.lean +++ b/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 := diff --git a/tests/lean/run/exposeDiff.lean b/tests/lean/run/exposeDiff.lean index 0444168aba..e002a9ccb6 100644 --- a/tests/lean/run/exposeDiff.lean +++ b/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} := diff --git a/tests/lean/run/fin_coercions.lean b/tests/lean/run/fin_coercions.lean index 549a7000d3..7d0ef9274b 100644 --- a/tests/lean/run/fin_coercions.lean +++ b/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 -/ diff --git a/tests/lean/run/haveTactic.lean b/tests/lean/run/haveTactic.lean index 821b35d66c..aae618fe02 100644 --- a/tests/lean/run/haveTactic.lean +++ b/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 diff --git a/tests/lean/run/issue8213.lean b/tests/lean/run/issue8213.lean index 9cd63f764e..ed5b8146df 100644 --- a/tests/lean/run/issue8213.lean +++ b/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' -/ diff --git a/tests/lean/run/mergeSort.lean b/tests/lean/run/mergeSort.lean index a7c079f699..8fa970819f 100644 --- a/tests/lean/run/mergeSort.lean +++ b/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 diff --git a/tests/lean/run/partial_fixpoint_explicit.lean b/tests/lean/run/partial_fixpoint_explicit.lean index a45c715c70..8fe188e101 100644 --- a/tests/lean/run/partial_fixpoint_explicit.lean +++ b/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) diff --git a/tests/lean/run/premise_selection.lean b/tests/lean/run/premise_selection.lean index da0f006e2a..bdf46898bf 100644 --- a/tests/lean/run/premise_selection.lean +++ b/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)`. -/ diff --git a/tests/lean/run/proofAsSorry.lean b/tests/lean/run/proofAsSorry.lean index d93b7473aa..1e265d6f11 100644 --- a/tests/lean/run/proofAsSorry.lean +++ b/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 diff --git a/tests/lean/run/scopedLocalReducibility.lean b/tests/lean/run/scopedLocalReducibility.lean index b6ca268ad7..49360e0932 100644 --- a/tests/lean/run/scopedLocalReducibility.lean +++ b/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 := diff --git a/tests/lean/run/scopedunifhint.lean b/tests/lean/run/scopedunifhint.lean index 72764c3200..92ba475921 100644 --- a/tests/lean/run/scopedunifhint.lean +++ b/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 diff --git a/tests/lean/run/sealCommand.lean b/tests/lean/run/sealCommand.lean index 03172a197a..07a34aa21c 100644 --- a/tests/lean/run/sealCommand.lean +++ b/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 diff --git a/tests/lean/run/sorry.lean b/tests/lean/run/sorry.lean index 8d66421ab8..5cc7ee2fba 100644 --- a/tests/lean/run/sorry.lean +++ b/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) diff --git a/tests/lean/run/tactic_config.lean b/tests/lean/run/tactic_config.lean index b2ce2ed7e3..84a4f3a540 100644 --- a/tests/lean/run/tactic_config.lean +++ b/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 } -/ diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean index 9d89a32f47..d200f3feb9 100644 --- a/tests/lean/run/variable.lean +++ b/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] diff --git a/tests/lean/run/wfirred.lean b/tests/lean/run/wfirred.lean index adc1e0d80e..e8ec61c20d 100644 --- a/tests/lean/run/wfirred.lean +++ b/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 diff --git a/tests/lean/server/content_diag.json b/tests/lean/server/content_diag.json index cb737d16bb..cd171fd2c2 100644 --- a/tests/lean/server/content_diag.json +++ b/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"} \ No newline at end of file diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out index c5fa1de371..527db1c847 100644 --- a/tests/lean/shadow.lean.expected.out +++ b/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 diff --git a/tests/lean/simpArgTypeMismatch.lean.expected.out b/tests/lean/simpArgTypeMismatch.lean.expected.out index 883faffb77..b1529dfd57 100644 --- a/tests/lean/simpArgTypeMismatch.lean.expected.out +++ b/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` diff --git a/tests/lean/sorryAtError.lean.expected.out b/tests/lean/sorryAtError.lean.expected.out index 30fcbce94f..05d3e58198 100644 --- a/tests/lean/sorryAtError.lean.expected.out +++ b/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 diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out index c1d81bedd4..5fd3cd75f0 100644 --- a/tests/lean/struct1.lean.expected.out +++ b/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 diff --git a/tests/lean/structDefault.lean.expected.out b/tests/lean/structDefault.lean.expected.out index 3549d7d485..eaf80b5189 100644 --- a/tests/lean/structDefault.lean.expected.out +++ b/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 diff --git a/tests/lean/typeIncorrectPat.lean.expected.out b/tests/lean/typeIncorrectPat.lean.expected.out index 3d71526eff..8f108bb78a 100644 --- a/tests/lean/typeIncorrectPat.lean.expected.out +++ b/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✝ diff --git a/tests/lean/typeMismatch.lean.expected.out b/tests/lean/typeMismatch.lean.expected.out index 79b873a387..dbf7faba23 100644 --- a/tests/lean/typeMismatch.lean.expected.out +++ b/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 diff --git a/tests/lean/typeOf.lean.expected.out b/tests/lean/typeOf.lean.expected.out index 9c314b42bb..dcce4906b2 100644 --- a/tests/lean/typeOf.lean.expected.out +++ b/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 diff --git a/tests/pkg/builtin_attr/UserAttr/Tst.lean b/tests/pkg/builtin_attr/UserAttr/Tst.lean index f026980a11..873e313eec 100644 --- a/tests/pkg/builtin_attr/UserAttr/Tst.lean +++ b/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 := diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 0b029fb9f6..d7a930f61c 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/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 diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index 1b76c403fd..abce682460 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/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