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