Chapter 10: Typed Core and Core Lint

New files

• src/core_lint.rs
• src/core_type.rs

Changed files

• src/core.rs
• src/elaborate.rs
• src/typecheck.rs
• src/eval.rs
• src/lib.rs
• src/main.rs
• src/rename.rs
• src/renamed.rs

Motivation

The type checker has accepted our program. Excellent. Now the compiler gets to rewrite it, which gives us plenty of opportunities to introduce mistakes of our own. We might pass the wrong argument, forget a type instantiation, or reuse a variable identity. The source program being correct doesn’t help if we translate it incorrectly.

We’ll give Core explicit types and write a second checker for it. This checker has an easier job than inference. All the answers are already in the tree, so it only needs to verify that they fit together. When a transformation goes wrong, we can catch it close to where it happened. A compiler that checks its own homework is a rather useful thing to have.

The Language, Now

We can still write polymorphic functions without spelling out their type arguments.

id x = x

number = id 42

main = id True

In Core, the definition of id abstracts over a type variable. Its two uses apply it first to Int and then to Bool. Those applications are real IR nodes rather than comments on an untyped expression. The evaluator ignores their types, so this program still prints True.

Theory

The source expression id 42 hides a small decision. We’re using identity at Int. System F gives us a way to write that decision into the program. A type abstraction introduces a type parameter, and a type application chooses a type for it. Girard and Reynolds developed this explicit treatment of polymorphism [Girard (1972); Reynolds (1974)].

Think of the two new forms alongside ordinary lambdas and calls. An ordinary lambda waits for a value. A type abstraction abstracts over a type. This analogy helps us read the rules, although the type arguments will disappear before runtime.

$$\frac{\Gamma ,\alpha ⊢e:\tau \alpha \notin \mathsf{ftv}(\Gamma )}{\Gamma ⊢\Lambda \alpha .e:\forall \alpha .\tau }\text{(Type abstraction)}$$

$$\frac{\Gamma ⊢e:\forall \alpha .\tau \Gamma ⊢\sigma :\ast }{\Gamma ⊢e[\sigma ]:\tau [\sigma /\alpha ]}\text{(Type application)}$$

Every type binder has kind * in this chapter. Higher-kinded constructors will extend the kind judgment later. Ordinary application still requires an arrow type. A universally quantified function must first receive its type arguments.

Core supports full System F. Fun still exposes only HM polymorphism. Hand-built Core terms test that distinction without extending source syntax (Pierce 2002).

Implementation

The Core Datatypes

We can write the same language as a small grammar before looking at the Rust. Read each vertical bar as “or”. An expression $e$ is one of the forms below, and the right-hand column tells us what that form does.

$$\begin{array}{rlrl}e& =x& & \text{local variable}\\ & \mid g& & \text{global reference}\\ & \mid \ell & & \text{literal}\\ & \mid e_1{e}_2& & \text{application}\\ & \mid \lambda x:\tau .e& & \text{term abstraction}\\ & \mid \Lambda \alpha .e& & \text{type abstraction}\\ & \mid e[\tau ]& & \text{type application}\\ & \mid \text{let}b\text{in}e& & \text{binding group}\\ & \mid \text{if}{e}_1\text{then}{e}_2\text{else}{e}_3& & \text{conditional}\\ & \mid p[\overline{\tau }](\overline{e})& & \text{primitive operation}\end{array}$$

Here $x$ and $g$ name local and global values, $\ell$ is a literal, and $p$ is a primitive. An overbar means a sequence, so $\overline{e}$ stands for the primitive’s operands in evaluation order. We leave source spans out of the notation, though the Rust representation keeps them for diagnostics.

The types and binding groups have their own grammar.

$$\begin{array}{rlrl}\tau & =\text{Int}\mid \text{Bool}\mid \text{Char}\mid \text{String}& & \text{base types}\\ & \mid \alpha & & \text{type variable}\\ & \mid {\tau }_1\to {\tau }_2& & \text{function type}\\ & \mid \forall \alpha .\tau & & \text{universal type}\\ b& =x:\tau =e& & \text{nonrecursive binding}\\ & \mid \text{rec}\{\overline{x:\tau =e}\}& & \text{recursive group}\end{array}$$

A recursive group’s names are in scope throughout its right-hand sides. Lint also checks that those right-hand sides describe functions, possibly wrapped in type abstractions. In a nonrecursive binding, the new name is available only in the body of the let.

Notice the two different lambdas. In $\Lambda \alpha .\lambda x:\alpha .x$, the capital $\Lambda$ chooses no value at all. It introduces the type parameter used by the ordinary $\lambda$. Applying this identity to a type and then a value gives $(\Lambda \alpha .\lambda x:\alpha .x)[\mathsf{Int}]42$. That’s the explicit version of the source-level id 42 we started with.

A Core expression is a Rust enum. Each variable and term binder carries an Id with its type, so lint can check the tree without rerunning inference.

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
}

The expression constructors distinguish term-level functions (Lam, App) from type-level abstraction and instantiation (TyLam, TyApp). Let keeps the recursive components produced by the renamer. Prim carries explicit type arguments, evaluated operands, and a source span for failures.

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
}

Binding groups hold typed names and right-hand sides. A program is an ordered list of these groups together with the entry point:

#![allow(unused)]
fn main() {
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
pub use crate::core_type::Type;
use crate::{ast::Op, source::Span};
/// A Core identifier carries its independently checkable type.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct Id {
    pub name: crate::names::Id,
    pub ty: Type,
}
impl std::fmt::Display for Id {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} : {}", self.name, self.ty)
    }
}
#[derive(Clone, Debug, PartialEq, Eq)]
/// Immediate source values; strings are primitive UTF-8 values, not character lists.
pub enum Lit {
    Int(i64),
    Bool(bool),
    Char(char),
    String(String),
}
#[derive(Clone, Debug)]
/// System F Core makes type abstraction and instantiation explicit.
pub enum Expr {
    Var(Id),
    Global(Id),
    TyLam(u32, Box<Expr>),
    TyApp(Box<Expr>, Type),
    Lit(Lit),
    Lam(Id, Box<Expr>),
    App(Box<Expr>, Box<Expr>),
    Let(BindGroup, Box<Expr>),
    If(Box<Expr>, Box<Expr>, Box<Expr>),
    Prim(Op, Vec<Type>, Vec<Expr>, Span),
}
#[derive(Clone, Debug)]
/// A recursive binding is guaranteed to have a lambda right-hand side.
pub struct Bind {
    pub name: Id,
    pub rhs: Box<Expr>,
}
#[derive(Clone, Debug)]
/// An ordered component; recursive members are in scope in every right-hand side.
pub struct BindGroup {
    pub recursive: bool,
    pub binds: Vec<Bind>,
}
impl std::fmt::Display for Expr {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Var(n) => write!(f, "{}", n.name),
            Self::Global(n) => write!(f, "@{}", n.name),
            Self::TyLam(v, b) => write!(f, "(type-lambda t{v} {b})"),
            Self::TyApp(a, t) => write!(f, "(type-app {a} {t})"),
            Self::Lit(l) => write!(f, "{l}"),
            Self::Lam(n, b) => write!(f, "(lambda {n} {b})"),
            Self::App(a, b) => write!(f, "(app {a} {b})"),
            Self::Let(group, body) => write!(f, "(let {group} in {body})"),
            Self::If(c, a, b) => write!(f, "(if {c} {a} {b})"),
            Self::Prim(op, _, args, _) => {
                write!(f, "(prim {}", op.text())?;
                for a in args {
                    write!(f, " {a}")?;
                }
                write!(f, ")")
            }
        }
    }
}
impl std::fmt::Display for Lit {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => {
                write!(f, "{}", if *b { "True" } else { "False" })
            }
            Self::Char(c) => {
                write!(f, "{}", crate::ast::quote(&c.to_string(), '\''))
            }
            Self::String(s) => write!(f, "{}", crate::ast::quote(s, '"')),
        }
    }
}
impl std::fmt::Display for BindGroup {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "{} {{", if self.recursive { "rec" } else { "nonrec" })?;
        for b in &self.binds {
            write!(f, " {} = {};", b.name, b.rhs)?;
        }
        write!(f, " }}")
    }
}
/// Independently typecheck System F Core after each Core-producing pass.
pub fn lint(program: &Program) -> Result<(), String> {
    crate::core_lint::lint(program)
}
impl Id {
    pub fn unique(&self) -> u32 {
        self.name.name.unique
    }
}
#[derive(Clone, Debug)]
/// Globals are initialized in dependency order, with explicit recursive components.
pub struct Program {
    pub groups: Vec<BindGroup>,
    pub main: Id,
}
}

This chapter still has If. Datatype constructors and pattern matches arrive in Chapter 11, and flat cases and join points arrive in Chapter 16. The smaller enum here lets us establish typed elaboration and lint before adding those forms.

Recording inference results

Renamed expressions now have stable node numbers. The checker records the fresh type arguments used at each variable occurrence, the scheme of each binding, and the monotype of each lambda parameter. Before returning, it zonks all these types, so elaboration never needs access to the mutable metavariable store.

A variable occurrence inferred inside a recursive group initially sees a provisional monotype. Once the component is generalized, elaboration instantiates its recursive Core references at the corresponding generalized variables. Ordinary occurrences use the fresh arguments recorded during inference.

Elaborating polymorphism

Each generalized metavariable receives a fresh Core type identity. Binder types wrap the converted monotype in Forall. Right-hand sides wrap their terms in the matching TyLams. Local schemes can still mention type variables bound by an outer function’s abstraction.

#![allow(unused)]
fn main() {
fn group(
    &mut self,
    group: &renamed::BindGroup,
    outer: &BTreeMap<u32, u32>,
    global: bool,
) -> BindGroup {
    for binding in &group.binds {
        self.binder(
            binding.id.clone(),
            &self.typed.schemes[&binding.id],
            outer,
            global,
        );
    }
    let binds = group
        .binds
        .iter()
        .map(|binding| {
            let binder = self.binders[&binding.id].clone();
            let mut variables = outer.clone();
            variables.extend(binder.quantifiers.iter().copied());
            let mut rhs = self.expression(&binding.rhs, &variables);
            for (_, variable) in binder.quantifiers.iter().rev() {
                rhs = Expr::TyLam(*variable, Box::new(rhs));
            }
            Bind {
                name: binder.id,
                rhs: Box::new(rhs),
            }
        })
        .collect();
    BindGroup {
        recursive: group.recursive,
        binds,
    }
}
}

Occurrences gain TyApps, and lambda parameters carry their converted types. Core distinguishes global references from local variables. Its binder annotations are checked against the declared environment, so attaching a plausible-looking type to an otherwise wrong occurrence cannot evade lint.

An internal variable absent from every enclosing scheme needs a closed witness: (\f -> 42) (\x -> x) is an example. We use Int for these erased annotations. This does not default source expressions or resolve ambiguous class constraints.

Independent lint

The checker maintains term and type scopes, plus sets of binder identities already used. It checks arrow applications, primitive saturation, conditional branches, recursive function groups, and binder annotations. These are the explicit type abstraction and application rules:

#![allow(unused)]
fn main() {
Expr::TyLam(variable, body) => {
    if !self.seen_types.insert(*variable) {
        return Err(format!(
            "duplicate Core type binder t{variable}"
        ));
    }
    self.types.insert(*variable);
    let body = self.expression(body)?;
    self.types.remove(variable);
    Ok(Type::Forall(*variable, Box::new(body)))
}
Expr::TyApp(fun, argument) => {
    self.well_formed(argument)?;
    let function = self.expression(fun)?;
    let Type::Forall(variable, body) = function else {
        return Err(format!(
            "Core type application of non-polymorphic type {function}"
        ));
    };
    Ok(body.substitute(variable, argument))
}
}

Type application substitutes into the quantified body. Substitution must avoid capturing a free type variable in the argument, even for Core terms constructed outside our elaborator. The implementation freshens a conflicting binder:

#![allow(unused)]
fn main() {
pub fn substitute(&self, variable: u32, replacement: &Type) -> Type {
    match self {
        Self::Var(v) if *v == variable => replacement.clone(),
        Self::Arrow(a, b) => Self::arrow(
            a.substitute(variable, replacement),
            b.substitute(variable, replacement),
        ),
        Self::Forall(v, _) if *v == variable => self.clone(),
        Self::Forall(v, body) => {
            let (v, body) = if replacement.free().contains(v) {
                let fresh = self
                    .largest()
                    .max(replacement.largest())
                    .max(variable)
                    .checked_add(1)
                    .expect("type variable supply exhausted");
                (fresh, body.substitute(*v, &Self::Var(fresh)))
            } else {
                (*v, *body.clone())
            };
            Self::Forall(
                v,
                Box::new(body.substitute(variable, replacement)),
            )
        }
        _ => self.clone(),
    }
}
}

Type equality is alpha equivalence, so two forall types may use different fresh identities and still denote the same type. In contrast, a free type variable must refer to the same enclosing binder.

#![allow(unused)]
fn main() {
pub fn lint(program: &Program) -> Result<(), String> {
    let mut checker = Checker::default();
    for group in &program.groups {
        checker.group(group, true)?;
    }
    checker.expression(&Expr::Global(program.main.clone()))?;
    Ok(())
}
}

Aside. A compiler bug that drops TyApp from an application of polymorphic identity produces Core application of non-function type forall t0. t0 -> t0. The source program may be valid. The generated Core is not. The malformed-Core tests check this failure directly, without rerunning source inference.

Erasure and strict execution

TyLam and TyApp do not allocate runtime objects. The interpreter steps through them without substituting runtime values. This is erasure, rather than a separate runtime evaluation strategy for System F.

In particular, a type abstraction does not delay a strict initializer. The unused polymorphic binding below still fails before main is selected:

unused = (\x -> \y -> y) (div 1 0)

main = 42

Chapter 18 introduces an explicit erased IR. Corpus runs already enable --lint.

Running It

$ cd crates/ch10_core
$ cargo run -q -- run tests/programs/core/self-instantiation.fun --lint
42
$ cargo run -q -- dump --pass=core --no-prelude tests/programs/layout/signature.fun
nonrec { id#0 : forall t0. t0 -> t0 = (type-lambda t0 (lambda x#2 : t0 x#2)); }
nonrec { main#1 : Int = (app (type-app @id#0 Int) 42); }
$ cargo test -p ch10_core --test system_f

For a useful experiment, remove a type application from a small Core term and run lint. The source checker has no role in this test. We’re deliberately feeding the second checker a mistake that only the compiler could have made. It should reject the term before evaluation.

Exercises

1. Introductory. identify every type abstraction and type application in the Core dump for id id 42.
2. Intermediate. Explain why a captured outer type variable remains free in a local binding’s scheme but is bound in the complete Core program.
3. Intermediate. Construct a malformed Core primitive call with the right number of arguments but the wrong operand type.
4. Advanced. Demonstrate a capture bug in type substitution if freshening is removed, then explain why alpha equivalence alone does not repair it.

Further Reading

Girard’s thesis and Reynolds’s paper are the original sources for explicit polymorphism [Girard (1972); Reynolds (1974)]. Pierce develops System F’s typing and substitution rules (Pierce 2002).