From adae6fdb40386cb1caa6532b8a71e0e300ad8ff4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 29 Apr 2021 21:29:05 -0700
Subject: [PATCH] fix: tolerate type incorrect terms

This bug was producing a type error when I was using `set_option trace.Elab true`
---
 src/Lean/Elab/InfoTree.lean        | 5 ++++-
 tests/lean/run/traceElabIssue.lean | 4 ++++
 2 files changed, 8 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/traceElabIssue.lean

diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 6ab8d0166e..02107ab1cd 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -156,7 +156,10 @@ def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO
 
 def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
   info.runMetaM ctx do
-    return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange ctx info.stx}"
+    try
+      return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange ctx info.stx}"
+    catch _ =>
+      return f!"{← Meta.ppExpr info.expr} : <failed-to-infer-type> @ {formatStxRange ctx info.stx}"
 
 def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
   match info with
diff --git a/tests/lean/run/traceElabIssue.lean b/tests/lean/run/traceElabIssue.lean
new file mode 100644
index 0000000000..2ddc8a5cad
--- /dev/null
+++ b/tests/lean/run/traceElabIssue.lean
@@ -0,0 +1,4 @@
+set_option trace.Elab true
+inductive Vec (α : Type u) : Nat → Type u
+| nil      : Vec α Nat.zero
+| cons {n : Nat} : (head : α) → (tail : Vec α n) → Vec α (Nat.succ n)