I'm trying to use QuickCheck to test properties about length-indexed lists (a.k.a vectors) in Haskell. My trouble is that GHC is complaining about an ambiguous variable appearing on a Show constraint on main function.
I've defined vectors in a standard way
data Nat = Z | S Nat
data Vec :: Nat -> * -> * where
Nil :: Vec 'Z a
(:>) :: a -> Vec n a -> Vec ('S n) a
vlength :: Vec n a -> Int
vlength Nil = 0
vlength (_ :> xs) = 1 + vlength xs
and I have defined a function that converts it to a list
toList :: Vec n a -> [a]
toList Nil = []
toList (x :> xs) = x : (toList xs)
such conversion function should preserve length, that has an immediate encoding as a property:
toList_correct :: Show a => Vec n a -> Bool
toList_correct v = vlength v == length (toList v)
I've defined Arbitrary instances for Vec as:
instance (Show a, Arbitrary a) => Arbitrary (Vec 'Z a) where
arbitrary = return Nil
instance (Show a, Arbitrary a, Arbitrary (Vec n a)) => Arbitrary (Vec ('S n) a) where
arbitrary
= (:>) <$> arbitrary <*> arbitrary
The trouble happens when I call the quickCheck function on main:
main :: IO ()
main = quickCheck toList_correct
and GHC gives me the following message:
Ambiguous type variable ‘a0’ arising from a use of ‘quickCheck’
prevents the constraint ‘(Show a0)’ from being solved.
Probable fix: use a type annotation to specify what ‘a0’ should be.
These potential instances exist:
instance [safe] Show Args -- Defined in ‘Test.QuickCheck.Test’
instance [safe] Show Result -- Defined in ‘Test.QuickCheck.Test’
instance (Show a, Show b) => Show (Either a b)
-- Defined in ‘Data.Either’
...plus 27 others
...plus 65 instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the expression: quickCheck toList_correct
In an equation for ‘main’: main = quickCheck toList_correct
I have no idea on how could I fix this error. Any tip is highly welcome.
The complete code is available here.
There are two instances of the same problems here. The first instance is the one causing the error message. The second instance shows up only after you solve the first problem, and will be much harder to solve.
The error message comes from a common problem when your types are too general. A simpler example of the same error is the function:
-- Ambiguous type variable ‘a0’ arising from a use of ‘read’
showRead :: String -> String
showRead = show . read
In a nutshell, GHC knows that there is an intermediate value of some type a you will create (with read :: Read a => String -> a) which you then immediately convert back to a String (with show :: Show a => a -> String). The problem is that to run this, GHC does need to know what is the type of the thing you are reading and showing - yet it has no way of figuring that out.
a is ambiguousGHC is telling you it has no way of telling vectors of what type you want quickCheck to be testing against when it uses toList_correct. One fix is to add a type annotation (or use TypeApplications) and tell GHC what type of vector you want:
quickCheck (toList_correct :: Vec n () -> Bool)
n is ambiguousHowever, not only is a ambiguous, so is n! Because you are encoding into the type of the vector its length, you will only be able to quickcheck your property for vectors of a particular length. The easy fix is to settle on a particular length (or several lengths).
quickCheck (toList_correct :: Vec Z () -> Bool)
quickCheck (toList_correct :: Vec (S Z) () -> Bool)
quickCheck (toList_correct :: Vec (S (S Z)) () -> Bool)
That said, this feels (and so it should) a bit pointless - you want to test vectors of any length. The solution to this is to make an existential type BoxVector around your vector:
data BoxVector a where
box :: Vec n a -> BoxVector a
deriving instance Show a => Show (BoxVector a)
Now that we have this existential type, we can make an Arbitrary instance of it which is arbitrary even over the length of the vector:
instance (Show a, Arbitrary a) => Arbitrary (BoxVector a) where
arbitrary = fromList <$> arbitrary
where
fromList :: [a] -> BoxVector a
fromList = foldr (\e (Box es) -> Box (e :> es)) (Box Nil)
We can compare this arbitrary instance with your previous one (which we won't be needing) at GHCi:
ghci> sample (arbitrary :: Gen (Vec (S (S Z)) Int)) -- must specify length
(:>) 0 ((:>) 0 Nil)
(:>) 1 ((:>) 1 Nil)
(:>) 0 ((:>) (-2) Nil)
(:>) (-4) ((:>) (-6) Nil)
(:>) (-1) ((:>) 2 Nil)
(:>) (-8) ((:>) (-5) Nil)
(:>) (-11) ((:>) 4 Nil)
(:>) (-8) ((:>) 2 Nil)
(:>) (-8) ((:>) (-16) Nil)
(:>) (-16) ((:>) (-11) Nil)
(:>) 19 ((:>) (-6) Nil)
ghci> sample (arbitrary :: Gen (BoxVector Int)) -- all lengths generated
Box Nil
Box ((:>) (-2) ((:>) 0 Nil))
Box ((:>) (-4) Nil)
Box ((:>) 0 ((:>) (-2) ((:>) (-6) ((:>) (-3) ((:>) (-6) Nil)))))
Box ((:>) 8 Nil)
Box ((:>) 6 ((:>) (-6) ((:>) 9 Nil)))
Box ((:>) 5 ((:>) 4 ((:>) 4 ((:>) (-6) ((:>) (-6) ((:>) (-4) Nil))))))
Box ((:>) (-4) ((:>) 10 ((:>) (-10) ((:>) 2 ((:>) 6 ((:>) 3 ((:>) 4 ((:>) 1 ((:>) 3 Nil)))))))))
Box ((:>) 10 ((:>) (-16) ((:>) (-14) ((:>) 15 ((:>) 4 ((:>) (-7) ((:>) (-5) ((:>) 5 ((:>) 6 ((:>) (-1) ((:>) 1 ((:>) (-14) ((:>) (-4) ((:>) 15 Nil))))))))))))))
Box ((:>) (-2) ((:>) 9 ((:>) 0 ((:>) 7 ((:>) 5 ((:>) 17 Nil))))))
Box ((:>) (-19) ((:>) (-7) ((:>) (-17) ((:>) (-8) ((:>) (-16) ((:>) 16 ((:>) (-4) ((:>) 16 ((:>) 13 ((:>) (-7) ((:>) (-3) ((:>) 4 ((:>) (-6) ((:>) (-8) ((:>) (-14) Nil)))))))))))))))
Now, we are finally ready to make your test run. Since we want the test to run for all possible lengths, we need to change it to take a BoxVector instead of Vec.
toList_correct :: Show a => BoxVector a -> Bool
toList_correct (Box v) = vlength v == length (toList v)
Finally, we will still need to specify what our vectors will contain for the test. For this test, since we don't care about distinguishing elements of the vector from each other, might as well make them vectors of ().
main :: IO ()
main = quickCheck (toList_correct :: BoxVector () -> Bool)