How does instantiation of higher-rank types and subsumption interact during unification?

Question

A function type is higher-rank if a quantifier appears in contravariant position: f :: (forall a. [a] -> b) -> Bool

Regarding the unification of such a type the type variable a is more rigid than b, because the following instantiation rules apply:

• a can be instantiated with a flexible type variable, provided this doesn't allow a to escape its scope
• or with another rigid type variable
• but not with a non-abstract type, because not the caller of foo but foo itself decides what a is, while b is already determined by the caller

However, things get more complicated as soon as subsumption comes into play:

{-# LANGUAGE RankNTypes #-}

f :: (forall a. [a] -> [a]) -> Int -- rank-2
f _ = undefined

arg1a :: a -> a
arg1a x = x

arg1b :: [Int] -> [Int]
arg1b x = x

f arg1a -- type checks
f arg1b -- rejected

g :: ((forall a. [a] -> [a]) -> Int) -> Int -- rank-3
g _ = undefined

arg2a :: (a -> a) -> Int
arg2a _ = 1

arg2b :: (forall a. a -> a) -> Int
arg2b _ = 1

arg2c :: ([Int] -> [Int]) -> Int
arg2c _ = 1

g arg2a -- type checks
g arg2b -- rejected
g arg2c -- type checks

h :: (((forall a. [a] -> [a]) -> Int) -> Int) -> Int -- rank-4
h _ = undefined

arg3a :: ((a -> a) -> Int) -> Int
arg3a _ = 1

arg3b :: ((forall a. a -> a) -> Int) -> Int
arg3b _ = 1

arg3c :: (([Int] -> [Int]) -> Int) -> Int
arg3c _ = 1

h arg3a -- rejected
h arg3b -- type checks
h arg3c -- rejected

What immediately catches the eye is the subtype relation, which gets flipped for each additional contravariant position. The application g arg2b is rejected, because (forall a. a -> a) is more polymorphic than (forall a. [a] -> [a]) and thus (forall a. a -> a) -> Int is less polymorphic than (forall a. [a] -> [a]) -> Int.

The first thing I don't understand is why g arg2a is accepted. Does subsumption only kick in if both terms are higher-rank?

However, the fact that g arg2c type checks puzzles me even more. Doesn't this clearly violate the rule that the rigid type variable a must not be instantiated with a monotype like Int?

Maybe someone can lay out the unification process for both applications..

Answer 1

We have

g :: ((forall a. [a] -> [a]) -> Int) -> Int
arg2c :: ([Int] -> [Int]) -> Int

which are applied in g arg2c.

To type check this, it suffices to verify that the type of the argument is a subtype of the function domain type. I.e. that we have

([Int] -> [Int]) -> Int <: ((forall a. [a] -> [a]) -> Int)

According to the subtyping rules, we have (a->b) <: (a'->b') if and only if b<:b' and a'<:a. So the above is equivalent to

Int <: Int
forall a. [a] -> [a] <: [Int] -> [Int]

The first inequality is trivial. The second one holds because a foall type is a subtype of each one if its instances. Formally, (forall a. T) <: T{U/a} where {U/a} denotes the substitution of type variable a with type U. Hence,

forall a. [a] -> [a] <: ([a] -> [a]){Int/a} = [Int] -> [Int]