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..

If arg2c can accept an [Int] -> [Int] function as its first argument, then it can certainly accept the forall a. [a] -> [a] function that g is going to give to it, simply by subsequently choosing a ~ Int. (This should give a high-level intuition, but doesn't get into the details of unification that you're asking for, so not really an answer.) — Daniel Wagner
Roughly put, a doubly-contravariant position is a covariant position since the "double negative" cancels out, which can also be seen as a consequence of the subtype relation being flipped twice. Indeed, in your g arg2c the type a can be instantiated as Int, since if we compute the needed subtype checks, we end up with ([Int] -> [Int]) -> Int <: (forall a. [a] -> [a]) -> Int and then, flipping the relation, with forall a. [a] -> [a] <: [Int] -> [Int] which follows by instantiation. — chi
@chi I get the relation forall a. [a] -> [a] <: [Int] -> [Int], but the quantifier is still hanging around. However, now it isn't in contravariant position anymore, right? If a isn't rank-1+n but rank-1 after the subtype checks, than a can be instantiated with Int, of course, because a is a flexible type variable that can be instantiated with a type constant. So simply put, the process of subtype checks changes the nesting and thus the rank of the involved quantifiers. Is this about right? — Iven Marquardt
@scriptum Yes in the last <: the forall is at the top-level, so it's covariant. In the process the rank changes since we move from a larger type to its components. IMO, thinking about the rank does not help much understanding this. The last <: is simply a case of the general rule (forall a.T) <: T{U/a} where {U/a} denotes the substitution of type variable a with type U. This rule and (a->b) <: (a'->b') iff b<:b' and a'<:a is all you need for type checking your examples. — chi

chi chi · Accepted Answer · 2021-02-16T14:35:09

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]

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

1 Answers