From 09de37e8e5f9fab3c4015972528ec6ec1df8fb36 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Feb 2021 09:30:05 -0800 Subject: [PATCH] chore: improve error message --- src/Lean/Elab/SyntheticMVars.lean | 2 +- tests/lean/297.lean.expected.out | 2 +- tests/lean/defaultInstance.lean.expected.out | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index dab641a8fa..0cb37f3ee1 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -211,7 +211,7 @@ private def reportStuckSyntheticMVars : TermElabM Unit := do withMVarContext mvarSyntheticDecl.mvarId do let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId unless (← get).messages.hasErrors do - logError <| "typeclass instance problem contains metavariables" ++ indentExpr mvarDecl.type + logError <| "typeclass instance problem is stuck, it is often due to metavariables" ++ indentExpr mvarDecl.type | SyntheticMVarKind.coe header expectedType eType e f? => withMVarContext mvarSyntheticDecl.mvarId do let mvarDecl ← getMVarDecl mvarSyntheticDecl.mvarId diff --git a/tests/lean/297.lean.expected.out b/tests/lean/297.lean.expected.out index e39619f634..071dad6cd8 100644 --- a/tests/lean/297.lean.expected.out +++ b/tests/lean/297.lean.expected.out @@ -1,4 +1,4 @@ -297.lean:1:10-1:11: error: typeclass instance problem contains metavariables +297.lean:1:10-1:11: error: typeclass instance problem is stuck, it is often due to metavariables OfNat (Sort ?u) 0 297.lean:2:0-2:1: error: failed to synthesize instance OfNat (Id PUnit) 0 diff --git a/tests/lean/defaultInstance.lean.expected.out b/tests/lean/defaultInstance.lean.expected.out index 37663e4b2d..786f08a893 100644 --- a/tests/lean/defaultInstance.lean.expected.out +++ b/tests/lean/defaultInstance.lean.expected.out @@ -1,4 +1,4 @@ defaultInstance.lean:20:20-20:23: error: failed to synthesize instance Foo Bool (?m x) -defaultInstance.lean:22:35-22:38: error: typeclass instance problem contains metavariables +defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck, it is often due to metavariables Foo Bool (?m x)