Lesson 7.8 — Beyond rank 1: higher-rank polymorphism and impredicativity (overview)¶

Techniques: higher-rank polymorphism — ∀ to the left of an arrow, checked with annotations by bidirectional subsumption (Odersky & Läufer 1996 [OL96]; Peyton Jones, Vytiniotis, Weirich & Shields 2007 [PJVWS07]; Dunfield & Krishnaswami 2013 [DK13]); impredicativity — instantiating a type variable with a polymorphic type, made practical by GHC's Quick Look (Serrano, Hage, Peyton Jones & Vytiniotis 2020 [SHPJV20]); the limit: type inference for System F is undecidable (Wells 1999 [Wel99]) · Pebble implements: none · Drills: — (see §9) · Prerequisites: Lessons 7.2, 7.4; Lesson 6.4 · Time: 3 hours

Hindley–Milner keeps inference complete by allowing ∀ only at the top of a let-bound type (Lesson 7.2). Two useful programs fall outside: a function that receives a polymorphic function and uses it at two types (both f = (f 1, f True), rank 2), and a data structure that stores polymorphic values ([forall a. a -> a], impredicative). Full System F allows both but its inference problem is undecidable, so every language that supports them asks for annotations and uses them bidirectionally. This lesson is an overview: the definitions, the key algorithmic idea for each, and the results that bound what is possible.

1. Problem and motivation¶

Higher-rank polymorphism¶

The problem. Proposition 7.2.10 showed that fun f -> (f 1, f true) is untypable in HM: a λ-bound variable is monomorphic. Some abstractions need exactly this — runST :: (forall s. ST s a) -> a uses a rank-2 type to keep a state thread from escaping; encodings of existentials and church-encoded data need it too. Odersky and Läufer [OL96] showed that if the programmer annotates the λ's parameter with its polymorphic type, inference for the rest stays HM-like: the annotation is propagated inward by the checking mode of bidirectional typing (Lesson 6.4), and applications are checked by a subsumption relation "is at least as polymorphic as". Peyton Jones et al. [PJVWS07] turned this into GHC's RankNTypes; Dunfield and Krishnaswami [DK13] gave a compact, complete algorithm.

Impredicativity¶

The problem. In predicative systems (HM, RankNTypes) a type variable ranges over monotypes: head :: [a] -> a can be used at a := Int -> Int but not at a := forall b. b -> b. So head ids with ids :: [forall a. a -> a] is rejected, although it is perfectly sound. Allowing it — impredicative instantiation — breaks the guessing that inference relies on: when unifying a with something, the checker cannot know whether a should be a polymorphic type. Years of proposals (MLF, HMF, FPH, Boxy Types) traded predictability for power; GHC 9.2 adopted Quick Look [SHPJV20]: before type-checking the arguments of an application, look at them quickly to find instantiations that are forced to be polymorphic, and otherwise stay predicative.

2. Definitions and algorithms¶

Definition 7.8.1 (Rank; predicative and impredicative instantiation)

The rank of a type: monotypes have rank 0; \(\forall\vec\alpha.\,\tau\) with \(\tau\) of rank 0 has rank 1; \(\sigma_1 \to \sigma_2\) has rank \(\max(\mathrm{rank}(\sigma_1) + 1, \mathrm{rank}(\sigma_2))\) when \(\sigma_1\) is polymorphic (a ∀ to the left of \(k\) arrows raises the rank by \(k\)). A type system is predicative if type variables are instantiated only with monotypes, impredicative if they may be instantiated with polymorphic types. System F is impredicative and of arbitrary rank.

Definition 7.8.2 (Subsumption)

\(\sigma_1 \le \sigma_2\) ("\(\sigma_1\) is at least as polymorphic as \(\sigma_2\)") holds if every instance of \(\sigma_2\) is an instance of \(\sigma_1\); for rank-1 schemes, \(\forall\vec\alpha.\,\tau_1 \le \forall\vec\beta.\,\tau_2\) iff \(\tau_2 = [\vec\tau/\vec\alpha]\tau_1\) for some \(\vec\tau\) (with \(\vec\beta\) treated as rigid). For higher-rank types the relation is contravariant in argument positions and covariant in results (deep skolemization, [PJVWS07, §4.6]; GHC 9 uses the simpler, shallow version).

Higher-rank polymorphism¶

Algorithm 7.8.3 (Checking an application against a higher-rank parameter)

Input: a function \(f\) whose (annotated) type is \((\forall\vec a.\,\sigma) \to \rho\), an argument \(e\).
Output: the result type \(\rho\), or a failure at \(e\).
Precondition: \(f\)'s type is known (a signature); unannotated λ-bound variables are monomorphic, as in HM.
Postcondition: \(e\) is checked to be at least as polymorphic as \(\forall\vec a.\,\sigma\) (Theorem 7.8.5).
Invariant: skolems (rigid variables) introduced for \(\vec a\) never escape: no unification variable created outside may be bound to a type mentioning them (the level discipline of Lesson 7.3).

function CheckArgAgainstPoly(e, ∀ā. σ):
    ā' ← fresh skolem constants at a new, deeper level      # "for an arbitrary a"
    Check(e, [ā'/ā]σ)                                        # bidirectional checking mode
    if some unification variable of a shallower level was bound to a type with ā':
        fail "rigid type variable would escape its scope"
function Check(e, τ) for e = λx. e1 and τ = σ1 → σ2:
    bind x : σ1   (σ1 may itself be polymorphic: x can be used at several types)
    Check(e1, σ2)

Impredicativity¶

Algorithm 7.8.4 (Quick Look instantiation, simplified from [SHPJV20])

Input: an application \(h\ e_1 \dots e_n\) whose head \(h\) has a type \(\forall\vec\alpha.\ \tau_1 \to \dots \to \tau_n \to \tau\); the expected result type if known.
Output: an instantiation of \(\vec\alpha\), possibly with polymorphic types, then ordinary checking of the arguments.
Precondition: the arguments' guarded types (the type of a variable, of an application headed by a variable with a known type) are available without full checking.
Postcondition: a variable is instantiated with a polymorphic type only if the application's own arguments or result force it; otherwise instantiation is predicative (Theorem 7.8.7).
Invariant: Quick Look never binds a variable that ordinary (predicative) inference would bind differently; it only fills variables that inference would otherwise fail on.

function QuickLook(h, args, expected):
    instantiate ᾱ with fresh "instantiation variables" κ̄
    for each argument e_i with parameter type τ_i[κ̄]:
        if e_i is guarded (a variable x, or an application x …) with known type σ_i:
            match τ_i[κ̄] against σ_i, binding κ's to (possibly polymorphic) types
    if expected is known: match τ[κ̄] against it
    replace every κ still unbound by an ordinary monomorphic unification variable
    check the arguments against τ_i with the κ's substituted (Algorithm 7.8.3 when polymorphic)

3. Worked examples¶

Higher-rank polymorphism¶

both :: (forall a. a -> a) -> (Int, Bool); both f = (f 1, f True). Checking the body: f : forall a. a -> a is in scope (the annotation), so f 1 instantiates it at Int and f True at Bool. Checking the call both id: Algorithm 7.8.3 skolemizes a to a rigid a' and checks id against a' -> a' — id : forall b. b -> b instantiates b := a': accepted. both not: check not : Bool -> Bool against a' -> a': unify a' = Bool — a' is rigid: rejected ("Couldn't match type a with Bool", §7). Without the annotation, bothInferred f = (f (1 :: Int), f True) is ordinary HM and fails at True.

Impredicativity¶

firstId = head ids with head :: forall b. [b] -> b and ids :: [forall a. a -> a]. Quick Look instantiates b with an instantiation variable \(\kappa\); the argument ids is a variable with known type, so matching [κ] against [forall a. a -> a] binds \(\kappa := \forall a.\,a \to a\) — impredicatively. The result type is then forall a. a -> a, matching the signature. Without ImpredicativeTypes, even the signature ids :: [forall a. a -> a] is rejected (§7).

4. Invariants and correctness¶

Higher-rank polymorphism¶

Theorem 7.8.5 (Predicative higher-rank checking with annotations is sound, complete and decidable)

For the predicative, arbitrary-rank type system of [PJVWS07] (equivalently [DK13]), the bidirectional algorithm terminates and accepts exactly the programs typable with the given annotations, where every λ-bound variable used polymorphically is annotated; HM programs need no annotation.

Proof sketch (full proofs: [DK13, §5–7]; [PJVWS07, §6])

Soundness by induction on the algorithmic derivation, each rule mapping to a declarative rule; the skolem-escape check corresponds to the side condition of \(\forall\)-introduction. Completeness relative to annotated programs: every place where the declarative system guesses a polymorphic type is either annotated (so checking mode supplies it) or is an instantiation, which predicativity restricts to monotypes that unification can find — the same argument as W's completeness (Theorem 7.2.11). Decidability: every rule is syntax-directed on the term or the type, and instantiations are monotypes, so the measure (term size, type size) decreases.

Proposition 7.8.6 (Rank 2 cannot be inferred without annotations by HM's method)

fun f -> (f 1, f true) has the System F types \((\forall a.\,a \to a) \to \mathsf{int} \times \mathsf{bool}\) and \((\forall a.\,a \to \mathsf{int}) \to \mathsf{int} \times \mathsf{int}\), and no most general one among rank-2 types in which the others are instances by HM's instance relation.

Proof

Both types are derivable in System F by annotating \(f\) accordingly. A common generalization would have to assign \(f\) a type from which both \(\forall a.\,a \to a\) and \(\forall a.\,a \to \mathsf{int}\) arise by instantiating free variables of the function's type (the only instantiation HM performs); but these two parameter types differ in whether the result is the argument type or constant, which no substitution of free variables can change inside the bound \(\forall a\). Hence no principal type exists in HM's sense, and an algorithm must be told which one is meant.

Impredicativity¶

Theorem 7.8.7 (Quick Look is sound and conservative; full inference is undecidable)

(a) Every program Quick Look accepts is typable in System F, and every program accepted by GHC's predicative checker is accepted with the same types. (b) Type inference (and even type checking with only λ-annotations missing) for System F is undecidable.

Proof sketch (full proofs: (a) [SHPJV20, §5]; (b) [Wel99])

(a) Quick Look only adds bindings for instantiation variables that the predicative checker would leave as unification variables and then fail on or leave unconstrained, and each binding is justified by an argument's known type, so the elaborated System F term types. (b) Wells reduces the semi-unification problem, proven undecidable by Kfoury, Tiuryn and Urzyczyn, to typability in System F: a term can be built whose typability encodes a given semi-unification instance. Every practical impredicative system therefore restricts where polymorphic instantiations may be guessed — Quick Look to what is visible in one application.

5. Complexity¶

Technique	Time (worst)	Time (typical)	Space	Variables
Higher-rank (predicative, annotated)	as HM (DEXPTIME-complete) plus a subsumption check per argument	near-linear	skolems per polymorphic argument	\(n\) program size
Quick Look	one extra pass over each application's arguments: linear in the application	negligible	instantiation variables	\(k\) arguments per application
System F inference	undecidable (Theorem 7.8.7b)	—	—	—

Justification. Subsumption checks are syntax-directed on types; Quick Look inspects each argument's head once. Pathological family: stacking higher-rank arguments does not blow up checking (annotations are given); the blow-ups are HM's (Lesson 7.3 §5), unchanged.

Higher-rank polymorphism¶

Deep vs shallow subsumption [PJVWS07]: GHC 9 dropped deep skolemization and co/contravariance of arrows in subsumption ("simplify subsumption"), requiring η-expansion in a few programs. Trade-off: simpler, preserves semantics under laziness; some old programs need \x -> f x.
Polymorphic record fields / first-class modules (OCaml): rank-2 via explicitly polymorphic record fields and methods. Trade-off: no new inference; annotations at the field.

Impredicativity¶

MLF (Le Botlan & Rémy): types with flexible and rigid bounds give principal types for impredicative programs. Trade-off: complete, but the types are unfamiliar and the implementation complex.
HMF, FPH, Boxy types: earlier impredicative extensions of GHC-style inference. Trade-off: each was hard to predict; Quick Look replaced them because it is local and simple [SHPJV20].

7. In real compilers¶

Higher-rank polymorphism¶

GHC: RankNTypes; application checking in tcApp (compiler/GHC/Tc/Gen/App.hs) with skolemization in GHC.Tc.Utils.Unify [GHC-App, GHC-Unify]. The user's guide section "Arbitrary-rank polymorphism" describes the rules [GHC-RankN]. OCaml offers rank 2 through polymorphic record fields; Scala 3 through polymorphic function types.

Rank-2 arguments in GHC 9.4: skolems and the unannotated case

Reproduce (GHC 9.4.7):

mkdir -p hs && cat > hs/Rank.hs <<'EOF'
{-# LANGUAGE RankNTypes #-}
module Rank where

both :: (forall a. a -> a) -> (Int, Bool)
both f = (f 1, f True)

ok :: (Int, Bool)
ok = both id

notPoly :: (Int, Bool)
notPoly = both not

bothInferred f = (f (1 :: Int), f True)
EOF
LC_ALL=C ghc -fno-code hs/Rank.hs

Output (the [1 of 1] Compiling line removed):

hs/Rank.hs:11:16: error:
    * Couldn't match type `a' with `Bool'
      Expected: a -> a
        Actual: Bool -> Bool
      `a' is a rigid type variable bound by
        a type expected by the context:
          forall a. a -> a
        at hs/Rank.hs:11:16-18
    * In the first argument of `both', namely `not'
      In the expression: both not
      In an equation for `notPoly': notPoly = both not
   |
11 | notPoly = both not
   |                ^^^

hs/Rank.hs:13:35: error:
    * Couldn't match expected type `Int' with actual type `Bool'
    * In the first argument of `f', namely `True'
      In the expression: f True
      In the expression: (f (1 :: Int), f True)
   |
13 | bothInferred f = (f (1 :: Int), f True)
   |                                   ^^^^

What to notice: both's body and both id are accepted (no error on lines 5 and 8). both not fails because a became a rigid skolem (Algorithm 7.8.3). Without the annotation, f is HM-monomorphic and the second use fails — Proposition 7.8.6 in practice.

Impredicativity¶

GHC ≥ 9.2: ImpredicativeTypes enables Quick Look, implemented by quickLookArg in compiler/GHC/Tc/Gen/App.hs [GHC-App]; the user's guide section "Impredicative polymorphism" states the rules [GHC-Impred].

Quick Look in GHC 9.4: a list of polymorphic functions

Reproduce (GHC 9.4.7):

mkdir -p hs && cat > hs/Impred.hs <<'EOF'
{-# LANGUAGE ImpredicativeTypes #-}
module Impred where

ids :: [forall a. a -> a]
ids = [id, \x -> x]

firstId :: forall a. a -> a
firstId = head ids

applyAll :: (Int, Bool)
applyAll = case ids of (f : _) -> (f 1, f True)
EOF
LC_ALL=C ghc -fno-code hs/Impred.hs && echo "Impred.hs: accepted"
sed 's/ImpredicativeTypes/RankNTypes/; s/module Impred/module Pred/' hs/Impred.hs > hs/Pred.hs
LC_ALL=C ghc -fno-code hs/Pred.hs

Output (the [1 of 1] Compiling lines removed):

Impred.hs: accepted
hs/Pred.hs:4:8: error:
    * Illegal polymorphic type: forall a. a -> a
    * In the type signature: ids :: [forall a. a -> a]
    Suggested fix: Perhaps you intended to use ImpredicativeTypes
  |
4 | ids :: [forall a. a -> a]
  |        ^^^^^^^^^^^^^^^^^^

What to notice: with Quick Look, head ids instantiates head's b with the polymorphic forall a. a -> a (§3), and the pattern-bound f is used at two types. The predicative checker refuses even to form the type [forall a. a -> a] — a type variable of the list constructor may not stand for a polymorphic type.

8. Comparison¶

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
Higher-rank polymorphism	Arbitrary rank with annotations; complete and decidable for predicative instantiation (Theorem 7.8.5); no principal types without annotations (Proposition 7.8.6)	as HM · negligible overhead	Rigid/skolem-escape errors; clear once annotated	Medium: skolems, subsumption, levels	GHC `RankNTypes`, `runST`, Scala 3, OCaml record fields
Impredicativity	Polymorphic instantiation where one application forces it (Theorem 7.8.7a); full System F undecidable (Theorem 7.8.7b)	linear extra pass · negligible	Fails predictably: only local evidence is used	Medium (Quick Look) to very high (MLF)	GHC `ImpredicativeTypes`; research languages

Choose rank-N types with annotations when an API must take polymorphic arguments; keep everything else HM. Choose Quick Look-style impredicativity only when data structures must hold polymorphic values; prefer a wrapper type (newtype Id = Id (forall a. a -> a)) when portability or predictability matters.

9. Assessment¶

Technique	Quiz ids	Drill	Flashcard tag	Exercises
Higher-rank polymorphism	`rank-of-type`, `rank2-check`	— (an overview topic; the quiz computes ranks and checking verdicts)	`higher-rank`	—
Impredicativity	`impredicative-instantiation`, `system-f-undecidable`	— (as above)	`impredicativity`	—

References¶

See the chapter references.

Lesson 7.8 — Beyond rank 1: higher-rank polymorphism and impredicativity (overview)¶

1. Problem and motivation¶

Higher-rank polymorphism¶

Impredicativity¶

2. Definitions and algorithms¶

Higher-rank polymorphism¶

Impredicativity¶

3. Worked examples¶

Higher-rank polymorphism¶

Impredicativity¶

4. Invariants and correctness¶

Higher-rank polymorphism¶

Impredicativity¶

5. Complexity¶

6. Variants and refinements¶

Higher-rank polymorphism¶

Impredicativity¶

7. In real compilers¶

Higher-rank polymorphism¶

Impredicativity¶

8. Comparison¶

9. Assessment¶

References¶