From 299bc54af064c7c11b9c84bf86d844ced5ef28e5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 1 Oct 2020 18:47:22 -0700
Subject: [PATCH] chore: improve error message

---
 src/Lean/Elab/SyntheticMVars.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index ba6726fdf7..ae2b3bb0e1 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -151,7 +151,8 @@ newSyntheticMVars ← s.syntheticMVars.filterM $ fun mvarDecl =>
       val ← instantiateMVars (mkMVar mvarDecl.mvarId);
       when val.getAppFn.isMVar $
         unlessM (isDefEq val defaultVal) $
-          throwError "failed to assign default value to metavariable"; -- TODO: better error message
+          -- TODO: better error message
+          throwError ("failed to assign default value to metavariable" ++ indentExpr val ++ Format.line ++ "default value" ++ indentExpr defaultVal) ;
       pure false
   | _ => pure true;
 modify $ fun s => { s with syntheticMVars := newSyntheticMVars };