diff --git a/tests/Main.idr b/tests/Main.idr index 5ca2c90..c910b1f 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -11,7 +11,7 @@ ttimpTests "eta001", "eta002", "nest001", "nest002", "perf001", "perf002", "perf003", - "qtt001", "qtt002"] + "qtt001", "qtt002", "qtt003"] chdir : String -> IO Bool chdir dir diff --git a/tests/ttimp/qtt003/QTTEq.yaff b/tests/ttimp/qtt003/QTTEq.yaff new file mode 100644 index 0000000..ce32966 --- /dev/null +++ b/tests/ttimp/qtt003/QTTEq.yaff @@ -0,0 +1,8 @@ +data Eq : $a -> $b -> Type where + Refl : Eq $x $x + +okay : {p : $a -> $b} -> (1 x : $a) -> (1 y : $a) -> (1 prf : Eq x y) -> + p x -> p y +-- Should fail on the LHS, before even getting to the RHS, because +-- after elaboration 'x' appears twice even though it is linearly bound. +okay _ $x Refl $q = q diff --git a/tests/ttimp/qtt003/expected b/tests/ttimp/qtt003/expected new file mode 100644 index 0000000..31ffa52 --- /dev/null +++ b/tests/ttimp/qtt003/expected @@ -0,0 +1,3 @@ +Processing as TTImp +QTTEq.yaff:8:1--9:1:There are 2 uses of linear name x +Yaffle> Yaffle> Yaffle> Yaffle> Yaffle> Bye for now! diff --git a/tests/ttimp/qtt003/input b/tests/ttimp/qtt003/input new file mode 100644 index 0000000..2d115ca --- /dev/null +++ b/tests/ttimp/qtt003/input @@ -0,0 +1,5 @@ +:t foo +:t bar +:t baz1 +:t baz2 +:q diff --git a/tests/ttimp/qtt003/run b/tests/ttimp/qtt003/run new file mode 100755 index 0000000..29975de --- /dev/null +++ b/tests/ttimp/qtt003/run @@ -0,0 +1,3 @@ +$1 QTTEq.yaff < input + +rm -rf build