How to apply polymorphic function to a concrete type?

Question

Below is a distilled version of a problem I encountered while learning Haskell:

data A = A
data B = B

data Test = TestA A
          | TestB B

test :: (a -> a) -> (Test -> Test)
test op t =
  case t of
    TestA a -> TestA $ op a
    TestB b -> TestB $ op b

testA = test id (TestA A)
testB = test id (TestB B)

Trying to compile this gives the following error:

Couldn't match expected type ‘B’ with actual type ‘a’

‘a’ is a rigid type variable bound by the type signature for test :: (a -> a) -> Test -> Test

What's going on? I thought that when I pass in a polymorphic function, I should be able to apply it to values of different concrete types.

@AlexisKing: for this function, Rank2Types is enough. Currently, GHC implements Rank2Types via RankNTypes but theoretically there is a possibility to do more type inference if you only use rank-2 types; getting into the habit of using the right language extension should be more future-proof in case GHC gets type inference of rank-2 types at some point. — Cactus
@Cactus The official GHC documentation considers Rank2Types to be nothing short of deprecated, so I see no reason to believe there is any intention to make the sort of change you suggest. — Alexis King

Alexis King Alexis King · Accepted Answer · 2016-07-11T18:55:57

The basic problem here is how Haskell infers quantification from free variables in type signatures. Given the following type signature...

test :: (a -> a) -> (Test -> Test)

...the type variable a is unbound. Haskell automatically converts unbound type variables into universal quantification constraints, so the above type is actually interpreted like this:

test :: forall a. (a -> a) -> (Test -> Test)

Now the error you are getting might make a little bit more sense—the type variable a can only unify with one type per invocation of test, which is decided by the caller. Therefore, the (a -> a) function could be String -> String or Int -> Int or any other type, but it can never be a function that works on both A and B.

Obviously, though, you had a different intent when you wrote that type signature. You wanted the (a -> a) function to be a type signature like the one for id: a function that truly works for any value, not some particular function for some particular choice of a. To specify this, you must make the forall explicit so that the compiler knows precisely how that type variable should be quantified:

test :: (forall a. a -> a) -> (Test -> Test)

However, the above type is actually not valid in standard Haskell. It is supported by GHC, though, by using the Rank2Types or RankNTypes extension, which permits “higher rank” polymorphism like the type signature above.

How to apply polymorphic function to a concrete type?

1 Answers