diff --git a/tests/idris2/coverage012/Issue484.idr b/tests/idris2/coverage012/Issue484.idr new file mode 100644 index 000000000..236524568 --- /dev/null +++ b/tests/idris2/coverage012/Issue484.idr @@ -0,0 +1,12 @@ +%default covering + +data Three = Vrai | Faux | Indef + +getType : Three -> Type +getType Vrai = Unit +getType Faux = Unit +getType Indef = Void + +swap : (t : Three) -> getType t -> Three +swap Indef _ impossible +swap Vrai () = Faux diff --git a/tests/idris2/coverage012/expected b/tests/idris2/coverage012/expected index 577df0f48..409b36e75 100644 --- a/tests/idris2/coverage012/expected +++ b/tests/idris2/coverage012/expected @@ -10,3 +10,17 @@ Issue899.idr:3:1--3:46 Missing cases: zeroImpossible 0 _ +1/1: Building Issue484 (Issue484.idr) +Error: swap is not covering. + +Issue484.idr:10:1--10:41 + 06 | getType Vrai = Unit + 07 | getType Faux = Unit + 08 | getType Indef = Void + 09 | + 10 | swap : (t : Three) -> getType t -> Three + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Missing cases: + swap Faux _ + diff --git a/tests/idris2/coverage012/run b/tests/idris2/coverage012/run index 475966ef9..af70b37e0 100755 --- a/tests/idris2/coverage012/run +++ b/tests/idris2/coverage012/run @@ -1,3 +1,4 @@ $1 --no-color --console-width 0 --check Issue899.idr +$1 --no-color --console-width 0 --check Issue484.idr rm -rf build