diff --git a/tests/idris2/operators/operators004/Test.idr b/tests/idris2/operators/operators004/Test.idr
new file mode 100644
index 0000000000..b9ac279e8a
--- /dev/null
+++ b/tests/idris2/operators/operators004/Test.idr
@@ -0,0 +1,9 @@
+import Data.Vect
+
+typebind
+Exists : (t : Type) -> (t -> Type) -> Type
+Exists = DPair
+
+val : Exists (n : Nat) | Vect n Nat
+val = (4 ** [0,1,2,3])
+
diff --git a/tests/idris2/operators/operators004/expected b/tests/idris2/operators/operators004/expected
new file mode 100644
index 0000000000..31e5db7f32
--- /dev/null
+++ b/tests/idris2/operators/operators004/expected
@@ -0,0 +1 @@
+1/1: Building Test (Test.idr)
diff --git a/tests/idris2/operators/operators004/run b/tests/idris2/operators/operators004/run
new file mode 100755
index 0000000000..d35387bb39
--- /dev/null
+++ b/tests/idris2/operators/operators004/run
@@ -0,0 +1,3 @@
+. ../../../testutils.sh
+
+check Test.idr