From 6de225e4be73fdf2bc0184dc6a189a5127529b2e Mon Sep 17 00:00:00 2001
From: Csaba Hruska <csaba.hruska@gmail.com>
Date: Sat, 20 Jun 2020 23:39:03 +0200
Subject: [PATCH] add unit test for constructor duplicate

---
 tests/Main.idr                                 | 1 +
 tests/idris2/error011/ConstructorDuplicate.idr | 5 +++++
 tests/idris2/error011/expected                 | 3 +++
 tests/idris2/error011/run                      | 3 +++
 4 files changed, 12 insertions(+)
 create mode 100644 tests/idris2/error011/ConstructorDuplicate.idr
 create mode 100644 tests/idris2/error011/expected
 create mode 100755 tests/idris2/error011/run

diff --git a/tests/Main.idr b/tests/Main.idr
index 179152c50..5ced475cc 100644
--- a/tests/Main.idr
+++ b/tests/Main.idr
@@ -47,6 +47,7 @@ idrisTests
        -- Error messages
        "error001", "error002", "error003", "error004", "error005",
        "error006", "error007", "error008", "error009", "error010",
+       "error011",
        -- Modules and imports
        "import001", "import002", "import003", "import004",
        -- Interactive editing support
diff --git a/tests/idris2/error011/ConstructorDuplicate.idr b/tests/idris2/error011/ConstructorDuplicate.idr
new file mode 100644
index 000000000..3bc72a9b5
--- /dev/null
+++ b/tests/idris2/error011/ConstructorDuplicate.idr
@@ -0,0 +1,5 @@
+data A = B | B
+
+data C : Type -> Type where
+  D : C Int
+  D : C String
diff --git a/tests/idris2/error011/expected b/tests/idris2/error011/expected
new file mode 100644
index 000000000..e2ca12a14
--- /dev/null
+++ b/tests/idris2/error011/expected
@@ -0,0 +1,3 @@
+1/1: Building ConstructorDuplicate (ConstructorDuplicate.idr)
+ConstructorDuplicate.idr:1:14--3:1:Main.B is already defined
+ConstructorDuplicate.idr:5:3--5:15:Main.D is already defined
diff --git a/tests/idris2/error011/run b/tests/idris2/error011/run
new file mode 100755
index 000000000..a39439a82
--- /dev/null
+++ b/tests/idris2/error011/run
@@ -0,0 +1,3 @@
+$1 ConstructorDuplicate.idr --check
+
+rm -rf build