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