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