tests: add negative fixtures

base/src/test/resources/failure/holes/pi-dom-meta.aya

@@ -0,0 +1,5 @@
+data X : Set
+data infix = (a b : X) : Set
+
+data Test : Type
+| con (x : _) (y : X) (x = y)

base/src/test/resources/failure/holes/pi-dom-meta.aya.txt

@@ -0,0 +1,38 @@
+In file $FILE:5:19 ->
+
+  3 │   
+  4 │   data Test : Type
+  5 │   | con (x : _) (y : X) (x = y)
+    │                      ╰╯
+
+Error: The type
+         X
+       is in the domain of a function whose type is
+         Type 0
+
+In file $FILE:5:11 ->
+
+  3 │   
+  4 │   data Test : Type
+  5 │   | con (x : _) (y : X) (x = y)
+    │              ╰╯
+
+Error: The meta (denoted ? below) is supposed to satisfy:
+         ? → _ : Type 0
+       However, the solution below does not seem so:
+         X
+
+In file $FILE:5:23 ->
+
+  3 │   
+  4 │   data Test : Type
+  5 │   | con (x : _) (y : X) (x = y)
+    │                          ╰───╯
+
+Error: The type
+         x = y
+       is in the domain of a function whose type is
+         Type 0
+
+3 error(s), 0 warning(s).
+What are you doing?

base/src/test/resources/failure/holes/pi-dom.aya

@@ -0,0 +1,4 @@
+data X : Set
+
+data Test : Type
+| con X

base/src/test/resources/failure/holes/pi-dom.aya.txt

@@ -0,0 +1,14 @@
+In file $FILE:4:6 ->
+
+  2 │   
+  3 │   data Test : Type
+  4 │   | con X
+    │         ╰╯
+
+Error: The type
+         X
+       is in the domain of a function whose type is
+         Type 0
+
+1 error(s), 0 warning(s).
+What are you doing?