higher rank polymorphism

Jan Christiansen jac at informatik.uni-kiel.de
Wed Nov 15 07:20:43 EST 2006

Hi,

I want to use a rank 2 data type and end up in typ problems that I
don't understand. I would really appreciate any hints to the
presented cases or pointers to interesting papers that address the
background of these problems.

I define the following datatype and a simple function that checks
whether the list is empty.

data Test = Test (forall a . [a -> a])

null1 :: Test -> Bool
null1 (Test []) = True
null1 (Test _) = False

null2 :: Test -> Bool
null2 (Test l) = null l

null3 :: Test -> Bool
null3 (Test l) =
case l of
[] -> True
_  -> False

For null1 ghc reports the following typeerror:
Couldn't match expected type `forall a. [a -> a]'
against inferred type `[a]'
In the pattern: []
In the pattern: Test []
In the definition of `null1': null1 (Test []) = True

while null2 and null3 don't cause errors. I don't understand why
there is a difference between these definitions of null.

cp1 :: Test -> Test
cp1 (Test l) =
case l of
[]     -> Test []
(x:xs) -> Test (x:xs)

cp2 :: Test -> Test
cp2 (Test l) =
if null l
then Test []
else Test (head l:tail l)

For cp1 ghc reports the following typeerror:
Inferred type is less polymorphic than expected
Quantified type variable `a' is mentioned in the environment:
xs :: [a -> a] (bound at UpDownTree.hs:36:10)
x :: a -> a (bound at UpDownTree.hs:36:8)
In the first argument of `Test', namely `(x : xs)'
In the expression: Test (x : xs)
In a case alternative: (x : xs) -> Test (x : xs)

while for cp2 ghc doesn't report an error. I guess there is a similar
reason for this error as for the error for null1.

I now want to restrict the polymorphic functions in the data type to
types for which there is an instance of the type class Eq.

data TestEq = TestEq (forall a . Eq a => [a -> a])

null4 :: TestEq -> Bool
null4 (TestEq l) = null l

For null4 ghc reports the following typeerror:
Ambiguous type variable `a' in the constraint:
`Eq a' arising from use of `l' at UpDownClass.hs:37:24
Probable fix: add a type signature that fixes these type variable
(s)

I obviously cannot add a constraint that constraints a type variable
that doesn't occur in the type of null4.

I will be very pleased for any hints.

Regards, Jan