diff --git a/crates/core/src/inference.rs b/crates/core/src/inference.rs
new file mode 100644
index 0000000..be11976
--- /dev/null
+++ b/crates/core/src/inference.rs
@@ -0,0 +1,19 @@
+//! Hindley-Milner style inference core.
+//!
+//! This module contains the reusable pieces needed by the type checker to move
+//! from annotation checking to constraint-based inference. It deliberately keeps
+//! inference variables separate from named generic parameters: named generics are
+//! source-level `a`/`value` parameters, while inference variables are solver
+//! placeholders created by the checker.
+
+pub mod constraints;
+pub mod generics;
+pub mod interfaces;
+pub mod substitutions;
+pub mod unification;
+
+pub use constraints::{Constraint, ConstraintSet};
+pub use generics::{Environment, Scheme, TypeVarSupply};
+pub use interfaces::InferenceInterface;
+pub use substitutions::{Field, InferenceVariable, Substitutions, TypeTerm};
+pub use unification::{UnificationError, Unifier};
diff --git a/crates/core/src/inference/constraints.rs b/crates/core/src/inference/constraints.rs
new file mode 100644
index 0000000..f9893a6
--- /dev/null
+++ b/crates/core/src/inference/constraints.rs
@@ -0,0 +1,56 @@
+use crate::source::Span;
+
+use super::{TypeTerm, Unifier, substitutions::Substitutions, unification::UnificationError};
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Constraint {
+    pub expected: TypeTerm,
+    pub actual: TypeTerm,
+    pub span: Span,
+}
+
+impl Constraint {
+    pub fn new(expected: TypeTerm, actual: TypeTerm, span: Span) -> Self {
+        Self { expected, actual, span }
+    }
+}
+
+#[derive(Debug, Clone, Default, PartialEq, Eq)]
+pub struct ConstraintSet {
+    constraints: Vec<Constraint>,
+}
+
+impl ConstraintSet {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn push(&mut self, expected: TypeTerm, actual: TypeTerm, span: Span) {
+        self.constraints.push(Constraint { expected, actual, span });
+    }
+
+    pub fn iter(&self) -> impl Iterator<Item = &Constraint> {
+        self.constraints.iter()
+    }
+
+    pub fn is_empty(&self) -> bool {
+        self.constraints.is_empty()
+    }
+
+    pub fn solve(&self) -> Result<Substitutions, UnificationError> {
+        let mut unifier = Unifier::new();
+        for constraint in &self.constraints {
+            unifier.unify(&constraint.expected, &constraint.actual, Some(constraint.span))?;
+        }
+        Ok(unifier.into_substitutions())
+    }
+}
+
+impl IntoIterator for ConstraintSet {
+    type Item = Constraint;
+    type IntoIter = std::vec::IntoIter<Constraint>;
+
+    fn into_iter(self) -> Self::IntoIter {
+        self.constraints.into_iter()
+    }
+}
diff --git a/crates/core/src/inference/generics.rs b/crates/core/src/inference/generics.rs
new file mode 100644
index 0000000..191e9dd
--- /dev/null
+++ b/crates/core/src/inference/generics.rs
@@ -0,0 +1,180 @@
+use std::collections::{BTreeSet, HashMap};
+
+use super::{InferenceVariable, Substitutions, TypeTerm};
+
+#[derive(Debug, Clone, Default)]
+pub struct TypeVarSupply {
+    next: u64,
+}
+
+impl TypeVarSupply {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn fresh(&mut self) -> InferenceVariable {
+        let variable = InferenceVariable(self.next);
+        self.next += 1;
+        variable
+    }
+
+    pub fn fresh_type(&mut self) -> TypeTerm {
+        TypeTerm::Variable(self.fresh())
+    }
+}
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Scheme {
+    pub variables: Vec<InferenceVariable>,
+    pub type_: TypeTerm,
+}
+
+impl Scheme {
+    pub fn monomorphic(type_: TypeTerm) -> Self {
+        Self { variables: Vec::new(), type_ }
+    }
+
+    pub fn generalize(type_: &TypeTerm, environment: &Environment, substitutions: &Substitutions) -> Self {
+        let type_ = substitutions.walk(type_);
+        let environment_variables = environment.free_variables(substitutions);
+        let variables = type_
+            .free_variables()
+            .difference(&environment_variables)
+            .copied()
+            .collect();
+        Self { variables, type_ }
+    }
+
+    pub fn instantiate(&self, supply: &mut TypeVarSupply) -> TypeTerm {
+        let replacements = self
+            .variables
+            .iter()
+            .map(|variable| (*variable, supply.fresh_type()))
+            .collect::<HashMap<_, _>>();
+        replace_variables(&self.type_, &replacements)
+    }
+
+    /// Replace source-level named generics with fresh inference variables.
+    pub fn instantiate_named_generics(type_: &TypeTerm, supply: &mut TypeVarSupply) -> TypeTerm {
+        let mut replacements = HashMap::new();
+        replace_named_generics(type_, supply, &mut replacements)
+    }
+}
+
+#[derive(Debug, Clone, Default, PartialEq, Eq)]
+pub struct Environment {
+    values: HashMap<String, Scheme>,
+}
+
+impl Environment {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn insert(&mut self, name: impl Into<String>, scheme: Scheme) {
+        self.values.insert(name.into(), scheme);
+    }
+
+    pub fn get(&self, name: &str) -> Option<&Scheme> {
+        self.values.get(name)
+    }
+
+    pub fn free_variables(&self, substitutions: &Substitutions) -> BTreeSet<InferenceVariable> {
+        let mut variables = BTreeSet::new();
+        for scheme in self.values.values() {
+            let quantified = scheme.variables.iter().copied().collect::<BTreeSet<_>>();
+            for variable in substitutions.walk(&scheme.type_).free_variables() {
+                if !quantified.contains(&variable) {
+                    variables.insert(variable);
+                }
+            }
+        }
+        variables
+    }
+}
+
+fn replace_variables(type_: &TypeTerm, replacements: &HashMap<InferenceVariable, TypeTerm>) -> TypeTerm {
+    match type_ {
+        TypeTerm::Variable(variable) => replacements.get(variable).cloned().unwrap_or_else(|| type_.clone()),
+        TypeTerm::Tuple(items) => {
+            TypeTerm::Tuple(items.iter().map(|item| replace_variables(item, replacements)).collect())
+        }
+        TypeTerm::List(item) => TypeTerm::List(Box::new(replace_variables(item, replacements))),
+        TypeTerm::Record { name, fields } => TypeTerm::Record {
+            name: name.clone(),
+            fields: fields
+                .iter()
+                .map(|field| super::Field {
+                    name: field.name.clone(),
+                    type_: replace_variables(&field.type_, replacements),
+                })
+                .collect(),
+        },
+        TypeTerm::Custom { name, args } => TypeTerm::Custom {
+            name: name.clone(),
+            args: args.iter().map(|arg| replace_variables(arg, replacements)).collect(),
+        },
+        TypeTerm::Opaque { name, args } => TypeTerm::Opaque {
+            name: name.clone(),
+            args: args.iter().map(|arg| replace_variables(arg, replacements)).collect(),
+        },
+        TypeTerm::Function { params, return_type } => TypeTerm::Function {
+            params: params
+                .iter()
+                .map(|param| replace_variables(param, replacements))
+                .collect(),
+            return_type: Box::new(replace_variables(return_type, replacements)),
+        },
+        _ => type_.clone(),
+    }
+}
+
+fn replace_named_generics(
+    type_: &TypeTerm, supply: &mut TypeVarSupply, replacements: &mut HashMap<String, TypeTerm>,
+) -> TypeTerm {
+    match type_ {
+        TypeTerm::Generic(name) => replacements
+            .entry(name.clone())
+            .or_insert_with(|| supply.fresh_type())
+            .clone(),
+        TypeTerm::Tuple(items) => TypeTerm::Tuple(
+            items
+                .iter()
+                .map(|item| replace_named_generics(item, supply, replacements))
+                .collect(),
+        ),
+        TypeTerm::List(item) => TypeTerm::List(Box::new(replace_named_generics(item, supply, replacements))),
+        TypeTerm::Record { name, fields } => TypeTerm::Record {
+            name: name.clone(),
+            fields: fields
+                .iter()
+                .map(|field| super::Field {
+                    name: field.name.clone(),
+                    type_: replace_named_generics(&field.type_, supply, replacements),
+                })
+                .collect(),
+        },
+        TypeTerm::Custom { name, args } => TypeTerm::Custom {
+            name: name.clone(),
+            args: args
+                .iter()
+                .map(|arg| replace_named_generics(arg, supply, replacements))
+                .collect(),
+        },
+        TypeTerm::Opaque { name, args } => TypeTerm::Opaque {
+            name: name.clone(),
+            args: args
+                .iter()
+                .map(|arg| replace_named_generics(arg, supply, replacements))
+                .collect(),
+        },
+        TypeTerm::Function { params, return_type } => TypeTerm::Function {
+            params: params
+                .iter()
+                .map(|param| replace_named_generics(param, supply, replacements))
+                .collect(),
+            return_type: Box::new(replace_named_generics(return_type, supply, replacements)),
+        },
+        _ => type_.clone(),
+    }
+}
diff --git a/crates/core/src/inference/interfaces.rs b/crates/core/src/inference/interfaces.rs
new file mode 100644
index 0000000..3faccbb
--- /dev/null
+++ b/crates/core/src/inference/interfaces.rs
@@ -0,0 +1,34 @@
+use std::collections::HashMap;
+
+use super::Scheme;
+use crate::types::TypeDeclaration;
+
+/// Public inferred schemes exported by a module.
+#[derive(Debug, Clone, Default, PartialEq, Eq)]
+pub struct InferenceInterface {
+    pub values: HashMap<String, Scheme>,
+    pub types: HashMap<String, TypeDeclaration>,
+    pub constructors: HashMap<String, Scheme>,
+}
+
+impl InferenceInterface {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn insert_value(&mut self, name: impl Into<String>, scheme: Scheme) {
+        self.values.insert(name.into(), scheme);
+    }
+
+    pub fn insert_constructor(&mut self, name: impl Into<String>, scheme: Scheme) {
+        self.constructors.insert(name.into(), scheme);
+    }
+
+    pub fn value(&self, name: &str) -> Option<&Scheme> {
+        self.values.get(name)
+    }
+
+    pub fn constructor(&self, name: &str) -> Option<&Scheme> {
+        self.constructors.get(name)
+    }
+}
diff --git a/crates/core/src/inference/substitutions.rs b/crates/core/src/inference/substitutions.rs
new file mode 100644
index 0000000..bcde1a2
--- /dev/null
+++ b/crates/core/src/inference/substitutions.rs
@@ -0,0 +1,207 @@
+use std::collections::{BTreeSet, HashMap};
+
+use crate::types::{FieldInfo, Type};
+
+/// A solver-created unknown type.
+#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub struct InferenceVariable(pub u64);
+
+/// A field in an inferred record shape.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub struct Field {
+    pub name: String,
+    pub type_: TypeTerm,
+}
+
+/// Type syntax used by the inference solver.
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum TypeTerm {
+    Int,
+    Float,
+    String,
+    BitArray,
+    Bool,
+    Nil,
+    Tuple(Vec<TypeTerm>),
+    List(Box<TypeTerm>),
+    Record {
+        name: String,
+        fields: Vec<Field>,
+    },
+    Custom {
+        name: String,
+        args: Vec<TypeTerm>,
+    },
+    Generic(String),
+    Opaque {
+        name: String,
+        args: Vec<TypeTerm>,
+    },
+    Function {
+        params: Vec<TypeTerm>,
+        return_type: Box<TypeTerm>,
+    },
+    Variable(InferenceVariable),
+}
+
+/// Solved inference variables.
+#[derive(Debug, Clone, Default, PartialEq, Eq)]
+pub struct Substitutions {
+    variables: HashMap<InferenceVariable, TypeTerm>,
+}
+
+impl Substitutions {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn insert(&mut self, variable: InferenceVariable, type_: TypeTerm) {
+        self.variables.insert(variable, type_);
+    }
+
+    pub fn get(&self, variable: InferenceVariable) -> Option<&TypeTerm> {
+        self.variables.get(&variable)
+    }
+
+    pub fn is_empty(&self) -> bool {
+        self.variables.is_empty()
+    }
+
+    pub fn walk(&self, type_: &TypeTerm) -> TypeTerm {
+        match type_ {
+            TypeTerm::Variable(variable) => self
+                .variables
+                .get(variable)
+                .map(|type_| self.walk(type_))
+                .unwrap_or_else(|| type_.clone()),
+            TypeTerm::Tuple(items) => TypeTerm::Tuple(items.iter().map(|item| self.walk(item)).collect()),
+            TypeTerm::List(item) => TypeTerm::List(Box::new(self.walk(item))),
+            TypeTerm::Record { name, fields } => TypeTerm::Record {
+                name: name.clone(),
+                fields: fields
+                    .iter()
+                    .map(|field| Field { name: field.name.clone(), type_: self.walk(&field.type_) })
+                    .collect(),
+            },
+            TypeTerm::Custom { name, args } => {
+                TypeTerm::Custom { name: name.clone(), args: args.iter().map(|arg| self.walk(arg)).collect() }
+            }
+            TypeTerm::Opaque { name, args } => {
+                TypeTerm::Opaque { name: name.clone(), args: args.iter().map(|arg| self.walk(arg)).collect() }
+            }
+            TypeTerm::Function { params, return_type } => TypeTerm::Function {
+                params: params.iter().map(|param| self.walk(param)).collect(),
+                return_type: Box::new(self.walk(return_type)),
+            },
+            _ => type_.clone(),
+        }
+    }
+
+    pub fn apply(&self, type_: &mut TypeTerm) {
+        *type_ = self.walk(type_);
+    }
+}
+
+impl TypeTerm {
+    pub fn free_variables(&self) -> BTreeSet<InferenceVariable> {
+        let mut variables = BTreeSet::new();
+        self.collect_free_variables(&mut variables);
+        variables
+    }
+
+    pub fn contains_variable(&self, variable: InferenceVariable) -> bool {
+        self.free_variables().contains(&variable)
+    }
+
+    pub fn from_type(type_: &Type) -> Self {
+        match type_ {
+            Type::Int => Self::Int,
+            Type::Float => Self::Float,
+            Type::String => Self::String,
+            Type::BitArray => Self::BitArray,
+            Type::Bool => Self::Bool,
+            Type::Nil => Self::Nil,
+            Type::Tuple(items) => Self::Tuple(items.iter().map(Self::from_type).collect()),
+            Type::List(item) => Self::List(Box::new(Self::from_type(item))),
+            Type::Record { name, fields } => Self::Record {
+                name: name.clone(),
+                fields: fields
+                    .iter()
+                    .map(|field| Field { name: field.name.clone(), type_: Self::from_type(&field.type_) })
+                    .collect(),
+            },
+            Type::Custom { name, args } => {
+                Self::Custom { name: name.clone(), args: args.iter().map(Self::from_type).collect() }
+            }
+            Type::Generic(name) => Self::Generic(name.clone()),
+            Type::Opaque { name, args } => {
+                Self::Opaque { name: name.clone(), args: args.iter().map(Self::from_type).collect() }
+            }
+            Type::Function { params, return_type } => Self::Function {
+                params: params.iter().map(Self::from_type).collect(),
+                return_type: Box::new(Self::from_type(return_type)),
+            },
+        }
+    }
+
+    pub fn into_type(self) -> Option<Type> {
+        match self {
+            Self::Int => Some(Type::Int),
+            Self::Float => Some(Type::Float),
+            Self::String => Some(Type::String),
+            Self::BitArray => Some(Type::BitArray),
+            Self::Bool => Some(Type::Bool),
+            Self::Nil => Some(Type::Nil),
+            Self::Tuple(items) => Some(Type::Tuple(
+                items.into_iter().map(Self::into_type).collect::<Option<Vec<_>>>()?,
+            )),
+            Self::List(item) => Some(Type::List(Box::new(item.into_type()?))),
+            Self::Record { name, fields } => Some(Type::Record {
+                name,
+                fields: fields
+                    .into_iter()
+                    .map(|field| Some(FieldInfo { name: field.name, type_: field.type_.into_type()? }))
+                    .collect::<Option<Vec<_>>>()?,
+            }),
+            Self::Custom { name, args } => {
+                Some(Type::Custom { name, args: args.into_iter().map(Self::into_type).collect::<Option<Vec<_>>>()? })
+            }
+            Self::Generic(name) => Some(Type::Generic(name)),
+            Self::Opaque { name, args } => {
+                Some(Type::Opaque { name, args: args.into_iter().map(Self::into_type).collect::<Option<Vec<_>>>()? })
+            }
+            Self::Function { params, return_type } => Some(Type::Function {
+                params: params.into_iter().map(Self::into_type).collect::<Option<Vec<_>>>()?,
+                return_type: Box::new(return_type.into_type()?),
+            }),
+            Self::Variable(_) => None,
+        }
+    }
+
+    fn collect_free_variables(&self, variables: &mut BTreeSet<InferenceVariable>) {
+        match self {
+            Self::Variable(variable) => {
+                variables.insert(*variable);
+            }
+            Self::Tuple(items) => items.iter().for_each(|item| item.collect_free_variables(variables)),
+            Self::List(item) => item.collect_free_variables(variables),
+            Self::Record { fields, .. } => fields
+                .iter()
+                .for_each(|field| field.type_.collect_free_variables(variables)),
+            Self::Custom { args, .. } | Self::Opaque { args, .. } => {
+                args.iter().for_each(|arg| arg.collect_free_variables(variables));
+            }
+            Self::Function { params, return_type } => {
+                params.iter().for_each(|param| param.collect_free_variables(variables));
+                return_type.collect_free_variables(variables);
+            }
+            _ => {}
+        }
+    }
+}
+
+impl From<&Type> for TypeTerm {
+    fn from(type_: &Type) -> Self {
+        Self::from_type(type_)
+    }
+}
diff --git a/crates/core/src/inference/unification.rs b/crates/core/src/inference/unification.rs
new file mode 100644
index 0000000..a71d7ec
--- /dev/null
+++ b/crates/core/src/inference/unification.rs
@@ -0,0 +1,204 @@
+use crate::source::Span;
+
+use super::substitutions::{Field, InferenceVariable, Substitutions, TypeTerm};
+
+#[derive(Debug, Clone, PartialEq, Eq)]
+pub enum UnificationError {
+    Mismatch {
+        expected: Box<TypeTerm>,
+        actual: Box<TypeTerm>,
+        span: Option<Span>,
+    },
+    ArityMismatch {
+        expected: usize,
+        actual: usize,
+        span: Option<Span>,
+    },
+    FieldMismatch {
+        field: String,
+        span: Option<Span>,
+    },
+    OccursCheck {
+        variable: InferenceVariable,
+        type_: Box<TypeTerm>,
+        span: Option<Span>,
+    },
+}
+
+#[derive(Debug, Clone, Default)]
+pub struct Unifier {
+    substitutions: Substitutions,
+}
+
+impl Unifier {
+    pub fn new() -> Self {
+        Self::default()
+    }
+
+    pub fn substitutions(&self) -> &Substitutions {
+        &self.substitutions
+    }
+
+    pub fn into_substitutions(self) -> Substitutions {
+        self.substitutions
+    }
+
+    pub fn unify(
+        &mut self, expected: &TypeTerm, actual: &TypeTerm, span: Option<Span>,
+    ) -> Result<TypeTerm, UnificationError> {
+        let expected = self.substitutions.walk(expected);
+        let actual = self.substitutions.walk(actual);
+        self.unify_walked(expected, actual, span)
+    }
+
+    fn unify_walked(
+        &mut self, expected: TypeTerm, actual: TypeTerm, span: Option<Span>,
+    ) -> Result<TypeTerm, UnificationError> {
+        match (expected, actual) {
+            (TypeTerm::Variable(variable), type_) | (type_, TypeTerm::Variable(variable)) => {
+                self.bind_variable(variable, &type_, span)
+            }
+            (TypeTerm::Int, TypeTerm::Int) => Ok(TypeTerm::Int),
+            (TypeTerm::Float, TypeTerm::Float) => Ok(TypeTerm::Float),
+            (TypeTerm::String, TypeTerm::String) => Ok(TypeTerm::String),
+            (TypeTerm::BitArray, TypeTerm::BitArray) => Ok(TypeTerm::BitArray),
+            (TypeTerm::Bool, TypeTerm::Bool) => Ok(TypeTerm::Bool),
+            (TypeTerm::Nil, TypeTerm::Nil) => Ok(TypeTerm::Nil),
+            (TypeTerm::Generic(left), TypeTerm::Generic(right)) if left == right => Ok(TypeTerm::Generic(left)),
+            (TypeTerm::Tuple(expected), TypeTerm::Tuple(actual)) => {
+                Ok(TypeTerm::Tuple(self.unify_many(expected, actual, span)?))
+            }
+            (TypeTerm::List(expected), TypeTerm::List(actual)) => {
+                Ok(TypeTerm::List(Box::new(self.unify(&expected, &actual, span)?)))
+            }
+            (
+                TypeTerm::Custom { name: expected_name, args: expected_args },
+                TypeTerm::Custom { name: actual_name, args: actual_args },
+            ) if expected_name == actual_name => {
+                Ok(TypeTerm::Custom { name: expected_name, args: self.unify_many(expected_args, actual_args, span)? })
+            }
+            (
+                TypeTerm::Opaque { name: expected_name, args: expected_args },
+                TypeTerm::Opaque { name: actual_name, args: actual_args },
+            ) if expected_name == actual_name => {
+                Ok(TypeTerm::Opaque { name: expected_name, args: self.unify_many(expected_args, actual_args, span)? })
+            }
+            (
+                TypeTerm::Function { params: expected_params, return_type: expected_return },
+                TypeTerm::Function { params: actual_params, return_type: actual_return },
+            ) => Ok(TypeTerm::Function {
+                params: self.unify_many(expected_params, actual_params, span)?,
+                return_type: Box::new(self.unify(&expected_return, &actual_return, span)?),
+            }),
+            (
+                TypeTerm::Record { name: expected_name, fields: expected_fields },
+                TypeTerm::Record { name: actual_name, fields: actual_fields },
+            ) if expected_name == actual_name => Ok(TypeTerm::Record {
+                name: expected_name,
+                fields: self.unify_fields(expected_fields, &actual_fields, span)?,
+            }),
+            (expected, actual) => {
+                Err(UnificationError::Mismatch { expected: Box::new(expected), actual: Box::new(actual), span })
+            }
+        }
+    }
+
+    fn bind_variable(
+        &mut self, variable: InferenceVariable, type_: &TypeTerm, span: Option<Span>,
+    ) -> Result<TypeTerm, UnificationError> {
+        let type_ = self.substitutions.walk(type_);
+        if type_ == TypeTerm::Variable(variable) {
+            return Ok(type_);
+        }
+        if type_.contains_variable(variable) {
+            return Err(UnificationError::OccursCheck { variable, type_: Box::new(type_), span });
+        }
+        self.substitutions.insert(variable, type_.clone());
+        Ok(type_)
+    }
+
+    fn unify_many(
+        &mut self, expected: Vec<TypeTerm>, actual: Vec<TypeTerm>, span: Option<Span>,
+    ) -> Result<Vec<TypeTerm>, UnificationError> {
+        if expected.len() != actual.len() {
+            return Err(UnificationError::ArityMismatch { expected: expected.len(), actual: actual.len(), span });
+        }
+        expected
+            .into_iter()
+            .zip(actual)
+            .map(|(expected, actual)| self.unify(&expected, &actual, span))
+            .collect()
+    }
+
+    fn unify_fields(
+        &mut self, expected: Vec<Field>, actual: &[Field], span: Option<Span>,
+    ) -> Result<Vec<Field>, UnificationError> {
+        if expected.len() != actual.len() {
+            return Err(UnificationError::ArityMismatch { expected: expected.len(), actual: actual.len(), span });
+        }
+
+        let mut unified = Vec::new();
+        for expected_field in expected {
+            let Some(actual_field) = actual.iter().find(|field| field.name == expected_field.name) else {
+                return Err(UnificationError::FieldMismatch { field: expected_field.name, span });
+            };
+            unified.push(Field {
+                name: expected_field.name,
+                type_: self.unify(&expected_field.type_, &actual_field.type_, span)?,
+            });
+        }
+        Ok(unified)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn unifies_inference_variable_with_scalar() {
+        let variable = InferenceVariable(0);
+        let mut unifier = Unifier::new();
+
+        unifier
+            .unify(&TypeTerm::Variable(variable), &TypeTerm::Int, None)
+            .expect("unifies");
+
+        assert_eq!(
+            unifier.substitutions().walk(&TypeTerm::Variable(variable)),
+            TypeTerm::Int
+        );
+    }
+
+    #[test]
+    fn rejects_infinite_types() {
+        let variable = InferenceVariable(0);
+        let mut unifier = Unifier::new();
+        let recursive = TypeTerm::List(Box::new(TypeTerm::Variable(variable)));
+
+        let error = unifier
+            .unify(&TypeTerm::Variable(variable), &recursive, None)
+            .expect_err("occurs check fails");
+
+        assert!(matches!(
+            error,
+            UnificationError::OccursCheck { variable: InferenceVariable(0), .. }
+        ));
+    }
+
+    #[test]
+    fn unifies_function_types_recursively() {
+        let variable = InferenceVariable(0);
+        let mut unifier = Unifier::new();
+        let expected =
+            TypeTerm::Function { params: vec![TypeTerm::Variable(variable)], return_type: Box::new(TypeTerm::Bool) };
+        let actual = TypeTerm::Function { params: vec![TypeTerm::String], return_type: Box::new(TypeTerm::Bool) };
+
+        unifier.unify(&expected, &actual, None).expect("unifies");
+
+        assert_eq!(
+            unifier.substitutions().walk(&TypeTerm::Variable(variable)),
+            TypeTerm::String
+        );
+    }
+}
diff --git a/crates/core/src/lib.rs b/crates/core/src/lib.rs
index a23b04b..fa5e583 100644
--- a/crates/core/src/lib.rs
+++ b/crates/core/src/lib.rs
@@ -1,5 +1,6 @@
 pub mod ast;
 pub mod diagnostic;
+pub mod inference;
 pub mod ir;
 pub mod parse;
 pub mod project;
diff --git a/docs/src/internal/tasks/11_type_and_generic_inference.md b/docs/src/internal/tasks/11_type_and_generic_inference.md
index 082905c..21e27c1 100644
--- a/docs/src/internal/tasks/11_type_and_generic_inference.md
+++ b/docs/src/internal/tasks/11_type_and_generic_inference.md
@@ -8,12 +8,12 @@ Infer full Gleam expression, function, pattern, and module interface types.
 
 ### Inference core
 
-- [ ] Add inference variables distinct from named generic parameters.
-- [ ] Add type schemes for generalized values and functions.
-- [ ] Implement substitutions and type walking.
-- [ ] Implement unification for scalar, tuple, list, record, custom, opaque,
+- [x] Add inference variables distinct from named generic parameters.
+- [x] Add type schemes for generalized values and functions.
+- [x] Implement substitutions and type walking.
+- [x] Implement unification for scalar, tuple, list, record, custom, opaque,
       function, and variable types.
-- [ ] Implement occurs checks for recursive/infinite type rejection.
+- [x] Implement occurs checks for recursive/infinite type rejection.
 
 ### Constraint generation