From f39586a237d1e798a552e5cee99a1211c0fc3ac2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 10 Feb 2020 22:22:42 -0800
Subject: [PATCH] test: expose problem at `isDefEq`

---
 tests/lean/run/meta2.lean | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 89b9ca0cf6..d217c87952 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -585,3 +585,23 @@ withLocalDecl `α type BinderInfo.default $ fun α => do
   pure ()
 
 #eval tst35
+#check @Id
+
+
+def tst36 : MetaM Unit := do
+print "----- tst36 -----";
+let type := mkSort levelOne;
+m1 ← mkFreshExprMVar (mkArrow type type);
+withLocalDecl `α type BinderInfo.default $ fun α => do
+  m2 ← mkFreshExprMVar type;
+  t  ← mkAppM `Id #[m2];
+  check $ approxDefEq $ isDefEq (mkApp m1 α) t;
+  check $ approxDefEq $ isDefEq m1 (mkConst `Id [levelZero]);
+  pure ()
+
+set_option pp.all true
+set_option trace.Meta.isDefEq.step true
+set_option trace.Meta.isDefEq.delta true
+set_option trace.Meta.isDefEq.assign true
+
+-- #eval tst36