The typechecker doesn’t know when to apply the subsumption rule.
You can tell it when with the following function.
Prelude> let u :: ((f a -> f a) -> c) -> ((forall b. f b -> f b) -> c); u f n = f n
This says, given a function from a transformation for a specific type, we can make a function from a natural transformation forall b. f b -> f b
.
We can then try it successfully on the second example.
Prelude> :t g (u k2)
g (u k2) :: Int
The first example now gives a more informative error as well.
Prelude> :t g (u k1)
Couldn't match type `forall a. a -> a' with `[a0] -> [a0]'
Expected type: ([a0] -> [a0]) -> Int
Actual type: (forall a. a -> a) -> Int
In the first argument of `u', namely `k1'
In the first argument of `g', namely `(u k1)'
I don’t know if we can write a more general version of u
; we’d need a constraint-level notion of less polymorphic to write something like let s :: (a :<: b) => (a -> c) -> (b -> c); s f x = f x