How can I specialize a type in a Frege QuickCheck?

Question

I'd like to run the classical test for reversing a list. To this end, I have to specialize the list to a list of "Arbitrary" (sic!) types, e.g. [Int].

What works is

module ListCheck where

import Test.QuickCheck

myReverse :: [Int] -> [Int]
myReverse = reverse

reverse_of_reverse_is_original = property (\xs -> myReverse(myReverse xs) == xs)

or factoring out the invariant like

reverse_invariant :: [Int] -> Bool
reverse_invariant xs = reverse(reverse xs) == xs
reverse_of_reverse_is_original = property reverse_invariant

but I would rather want to not wrap the original function but use it directly. The usual Haskell trick of forcing a specialization through adding

... where types = xs :: [Int]

does not work here.

Is there a less verbose solution?

Answer 1

It is unfortunately the case that the

where types = xs :: [Int]

gets removed by the let expression simplification and canonicalization pass, which comes before type checking even. This is, so to speak, a side effect of dependency analysis, where it is seen that types is totally useless.

You can write:

p_rev = property rev
    where rev (xs::[Int]) = (reverse . reverse) xs == xs

or even:

p_rev = forAll (arbitrary :: Gen [Int])
          (\xs -> (reverse . reverse) xs == xs)

Since one could write nonsense like

where types = 1:true:"foo" + Just []

and it would still get removed, it would arguably be better to remove unused lets only after typechecking.