Compile-time QuickCheck as a type provider in Idris

Prov.idr

import QuickCheck

import Providers

%language TypeProviders

prop_RevRev : Eq a => List a -> Bool
prop_RevRev xs = reverse (reverse xs) == xs

stupid : List a -> List a
stupid [] = []
stupid [w,x,y,z] = []
stupid (x::xs) = reverse xs ++ [x]

prop_stupid : Eq a => List a -> Bool
prop_stupid xs = stupid (stupid xs) == xs


provTest : Testable TFGen a => a -> IO (Provider ())
provTest prop = if !(quickCheck prop)
                  then return (Provide ())
                  else return (Error "Test failed")


%provide (x : the Type ()) with provTest prop_RevRev
%provide (y : the Type ()) with provTest prop_stupid

Output from type checker:

Type checking ./Prov.idr
0
1
2
3
4
5
6
7
8
9
OK, passed 10 tests.
0
1
2
3
Falsifiable, after 3 tests:
[(), (), (), ()]
Prov.idr:14:28:Type provider error: Test failed