From 0b4590bd6904fe82ed48d9a0d428c0b785ee2ecc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Sep 2022 05:29:42 -0700
Subject: [PATCH] test: add `erased.lean`

---
 tests/lean/run/erased.lean       | 22 ++++++++++++++++++++++
 tests/lean/run/fieldTypeBug.lean |  4 +++-
 2 files changed, 25 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/erased.lean

diff --git a/tests/lean/run/erased.lean b/tests/lean/run/erased.lean
new file mode 100644
index 0000000000..a051082018
--- /dev/null
+++ b/tests/lean/run/erased.lean
@@ -0,0 +1,22 @@
+import Lean
+
+/-- `erased α` is the same as `α`, except that the elements
+  of `erased α` are erased in the VM in the same way as types
+  and proofs. This can be used to track data without storing it
+  literally. -/
+def Erased (α : Sort u) : Sort max 1 u :=
+  Σ's : α → Prop, ∃ a, (fun b => a = b) = s
+
+namespace Erased
+
+/-- Erase a value. -/
+@[inline]
+def mk {α} (a : α) : Erased α :=
+  ⟨fun b => a = b, a, rfl⟩
+
+open Lean.Compiler
+set_option pp.explicit true
+set_option pp.funBinderTypes true
+set_option pp.letVarTypes true
+set_option trace.Compiler.result true
+#eval Lean.Compiler.compile #[``Erased.mk]
diff --git a/tests/lean/run/fieldTypeBug.lean b/tests/lean/run/fieldTypeBug.lean
index 574dd78bf9..51da442627 100644
--- a/tests/lean/run/fieldTypeBug.lean
+++ b/tests/lean/run/fieldTypeBug.lean
@@ -12,5 +12,7 @@ def HList.set {αs : List (Type u)} (as : HList αs) (i : Fin αs.length) (v : 
   | [],     nil,       _,               _ => nil
 
 open Lean.Compiler
-set_option trace.Compiler true
+set_option pp.funBinderTypes true
+set_option pp.letVarTypes true
+set_option trace.Compiler.result true
 #eval compile #[``HList.set]