As an exercise, I am trying to quickCheck the applicative's homomorphism property:
pure f <*> pure x = pure (f x)
When I try to write the property in a general way using phantom types, I seem to run into endless 'Could not deduce' errors. At this point I have added many type annotations to my code, and still am getting these errors.
My code is:
{-# LANGUAGE ViewPatterns #-}
import Test.QuickCheck (quickCheck)
import Test.QuickCheck.Function (Fun, apply)
-- | phantom type
data T a = T
-- | pure f <*> pure x = pure (f x)
prop_homomorphism :: (Applicative f, Eq b, Eq (f b)) => (T a) -> (T (f b)) -> Fun a b -> a -> Bool
prop_homomorphism T T (apply -> g) x = (pure (g :: a -> b) <*> pure x :: (Applicative f, Eq (f b)) => f b) == (pure (g x) :: (A
pplicative f, Eq (f b)) => f b)
prop_maybeint :: IO ()
prop_maybeint = do
quickCheck (prop_homomorphism (T :: T Int) (T :: T (Maybe Int)))
main = do
prop_maybeint
And the errors this gives are:
applicativehomomorphism.hs:11:40: error:
• Could not deduce (Eq (f0 b0)) arising from a use of ‘==’
from the context: (Applicative f, Eq b, Eq (f b))
bound by the type signature for:
prop_homomorphism :: (Applicative f, Eq b, Eq (f b)) =>
T a -> T (f b) -> Fun a b -> a -> Bool
at applicativehomomorphism.hs:10:1-98
The type variables ‘f0’, ‘b0’ are ambiguous
These potential instances exist:
instance Eq a => Eq (Maybe a) -- Defined in ‘GHC.Base’
instance (Eq a, Eq b) => Eq (a, b) -- Defined in ‘GHC.Classes’
instance (Eq a, Eq b, Eq c) => Eq (a, b, c)
-- Defined in ‘GHC.Classes’
...plus 13 others
...plus one instance involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the expression:
(pure (g :: a -> b) <*> pure x :: (Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
In an equation for ‘prop_homomorphism’:
prop_homomorphism T T (apply -> g) x
= (pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
applicativehomomorphism.hs:11:41: error:
• Could not deduce (Applicative f0)
arising from an expression type signature
from the context: (Applicative f, Eq b, Eq (f b))
bound by the type signature for:
prop_homomorphism :: (Applicative f, Eq b, Eq (f b)) =>
T a -> T (f b) -> Fun a b -> a -> Bool
at applicativehomomorphism.hs:10:1-98
The type variable ‘f0’ is ambiguous
These potential instances exist:
instance Applicative IO -- Defined in ‘GHC.Base’
instance Applicative Maybe -- Defined in ‘GHC.Base’
instance Applicative ((->) a) -- Defined in ‘GHC.Base’
...plus two others
...plus two instances involving out-of-scope types
(use -fprint-potential-instances to see them all)
• In the first argument of ‘(==)’, namely
‘(pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)’
In the expression:
(pure (g :: a -> b) <*> pure x :: (Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
In an equation for ‘prop_homomorphism’:
prop_homomorphism T T (apply -> g) x
= (pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
applicativehomomorphism.hs:11:47: error:
• Couldn't match type ‘b’ with ‘b2’
‘b’ is a rigid type variable bound by
the type signature for:
prop_homomorphism :: forall (f :: * -> *) b a.
(Applicative f, Eq b, Eq (f b)) =>
T a -> T (f b) -> Fun a b -> a -> Bool
at applicativehomomorphism.hs:10:22
‘b2’ is a rigid type variable bound by
an expression type signature:
forall a1 b2. a1 -> b2
at applicativehomomorphism.hs:11:52
Expected type: a1 -> b2
Actual type: a -> b
• In the first argument of ‘pure’, namely ‘(g :: a -> b)’
In the first argument of ‘(<*>)’, namely ‘pure (g :: a -> b)’
In the first argument of ‘(==)’, namely
‘(pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)’
• Relevant bindings include
g :: a -> b (bound at applicativehomomorphism.hs:11:33)
prop_homomorphism :: T a -> T (f b) -> Fun a b -> a -> Bool
(bound at applicativehomomorphism.hs:11:1)
applicativehomomorphism.hs:11:112: error:
• Couldn't match type ‘b’ with ‘b1’
‘b’ is a rigid type variable bound by
the type signature for:
prop_homomorphism :: forall (f :: * -> *) b a.
(Applicative f, Eq b, Eq (f b)) =>
T a -> T (f b) -> Fun a b -> a -> Bool
at applicativehomomorphism.hs:10:22
‘b1’ is a rigid type variable bound by
an expression type signature:
forall (f1 :: * -> *) b1. (Applicative f1, Eq (f1 b1)) => f1 b1
at applicativehomomorphism.hs:11:126
Expected type: f1 b1
Actual type: f1 b
• In the second argument of ‘(==)’, namely
‘(pure (g x) :: (Applicative f, Eq (f b)) => f b)’
In the expression:
(pure (g :: a -> b) <*> pure x :: (Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
In an equation for ‘prop_homomorphism’:
prop_homomorphism T T (apply -> g) x
= (pure (g :: a -> b) <*> pure x ::
(Applicative f, Eq (f b)) => f b)
== (pure (g x) :: (Applicative f, Eq (f b)) => f b)
• Relevant bindings include
g :: a -> b (bound at applicativehomomorphism.hs:11:33)
prop_homomorphism :: T a -> T (f b) -> Fun a b -> a -> Bool
(bound at applicativehomomorphism.hs:11:1)
I've been fighting with this for a while and am pretty stuck. What is my problem?
luqui's suggestion solved this for me.
The problem was I needed to use ScopedTypeVariables and forall in order to refer to type parameters outside their type signature in the function body's type annotations.
Some relevant resources on ScopedTypeVariables I came across: