From d556ebbdc6544dfaccc3bd4701b2923d210ff2b6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 2 May 2021 20:04:41 -0700
Subject: [PATCH] test: add test for binder caching issue

---
 tests/lean/binderCacheIssue.lean              | 23 +++++++++++++++++++
 tests/lean/binderCacheIssue.lean.expected.out |  4 ++++
 2 files changed, 27 insertions(+)
 create mode 100644 tests/lean/binderCacheIssue.lean
 create mode 100644 tests/lean/binderCacheIssue.lean.expected.out

diff --git a/tests/lean/binderCacheIssue.lean b/tests/lean/binderCacheIssue.lean
new file mode 100644
index 0000000000..204d2550ce
--- /dev/null
+++ b/tests/lean/binderCacheIssue.lean
@@ -0,0 +1,23 @@
+universes u v w
+
+class Funtype (N : Sort u) (O : outParam (Sort v)) (T : outParam (Sort w)) :=
+  pack : O -> N
+  unpack : N -> O
+  apply : N -> T
+
+class LNot {P : Sort u} (L : P -> Prop) :=
+  toFun : (p : P) -> Not (L p)
+
+namespace LNot
+variable {P : Sort u} {L : P -> Prop}
+abbrev applyFun (K : LNot L) {p} := K.toFun p
+abbrev unpackFun (K : LNot L) := K.toFun
+instance isFuntype : Funtype (LNot L)
+  ((p : P) -> Not (L p)) ({p : P} -> Not (L p)) :=
+  {pack := mk, unpack := unpackFun, apply := applyFun}
+end LNot
+
+#check LNot.unpackFun
+#check LNot.isFuntype.unpack
+#check LNot.applyFun
+#check LNot.isFuntype.apply
diff --git a/tests/lean/binderCacheIssue.lean.expected.out b/tests/lean/binderCacheIssue.lean.expected.out
new file mode 100644
index 0000000000..37e7de1b64
--- /dev/null
+++ b/tests/lean/binderCacheIssue.lean.expected.out
@@ -0,0 +1,4 @@
+LNot.unpackFun : LNot ?m → ∀ (p : ?m), ¬?m p
+Funtype.unpack : LNot ?m → ∀ (p : ?m), ¬?m p
+LNot.applyFun : LNot ?m → ∀ {p : ?m}, ¬?m p
+Funtype.apply : LNot ?m → ∀ {p : ?m}, ¬?m p