From 6467c1d9adba20cfc2d482e90bdb99b7a5dea953 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 07:26:51 +0000
Subject: [PATCH] tests: add negative fixtures

---
 .../resources/failure/holes/pi-dom-meta.aya   |  5 +++
 .../failure/holes/pi-dom-meta.aya.txt         | 38 +++++++++++++++++++
 .../test/resources/failure/holes/pi-dom.aya   |  4 ++
 .../resources/failure/holes/pi-dom.aya.txt    | 14 +++++++
 4 files changed, 61 insertions(+)
 create mode 100644 base/src/test/resources/failure/holes/pi-dom-meta.aya
 create mode 100644 base/src/test/resources/failure/holes/pi-dom-meta.aya.txt
 create mode 100644 base/src/test/resources/failure/holes/pi-dom.aya
 create mode 100644 base/src/test/resources/failure/holes/pi-dom.aya.txt

diff --git a/base/src/test/resources/failure/holes/pi-dom-meta.aya b/base/src/test/resources/failure/holes/pi-dom-meta.aya
new file mode 100644
index 0000000000..bf0d608de6
--- /dev/null
+++ b/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)
diff --git a/base/src/test/resources/failure/holes/pi-dom-meta.aya.txt b/base/src/test/resources/failure/holes/pi-dom-meta.aya.txt
new file mode 100644
index 0000000000..71fd4af59a
--- /dev/null
+++ b/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?
diff --git a/base/src/test/resources/failure/holes/pi-dom.aya b/base/src/test/resources/failure/holes/pi-dom.aya
new file mode 100644
index 0000000000..b8e825fb99
--- /dev/null
+++ b/base/src/test/resources/failure/holes/pi-dom.aya
@@ -0,0 +1,4 @@
+data X : Set
+
+data Test : Type
+| con X
diff --git a/base/src/test/resources/failure/holes/pi-dom.aya.txt b/base/src/test/resources/failure/holes/pi-dom.aya.txt
new file mode 100644
index 0000000000..36f7ef888b
--- /dev/null
+++ b/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?