From 1f8370c67d0146556fe2c36b2efe0dd11bada067 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Oct 2019 13:26:19 -0700
Subject: [PATCH] test: issue reported by Reid

---
 tests/elabissues/Reid1.lean | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/elabissues/Reid1.lean

diff --git a/tests/elabissues/Reid1.lean b/tests/elabissues/Reid1.lean
new file mode 100644
index 0000000000..3569d73bdc
--- /dev/null
+++ b/tests/elabissues/Reid1.lean
@@ -0,0 +1,24 @@
+structure constantFunction (α β : Type) :=
+(f : α → β)
+(h : ∀ a₁ a₂, f a₁ = f a₂)
+
+instance {α β : Type} : HasCoeToFun (constantFunction α β) :=
+⟨_, constantFunction.f⟩
+
+def myFun {α : Type} : constantFunction α (Option α) :=
+{ f := fun a => none,
+  h := fun a₁ a₂ => rfl }
+
+def myFun' (α : Type) : constantFunction α (Option α) :=
+{ f := fun a => none,
+  h := fun a₁ a₂ => rfl }
+
+#check myFun 3
+#check @myFun Nat 3            -- works
+
+#check myFun' _ 3
+#check myFun' Nat 3            -- works
+
+#check ⇑myFun 3
+#check ⇑(myFun' _) 3
+#check ⇑(myFun' Nat) 3