diff --git a/.claude/skills/type-checker-tests/SKILL.md b/.claude/skills/type-checker-tests/SKILL.md
index 7cf38576..cacaeb82 100644
--- a/.claude/skills/type-checker-tests/SKILL.md
+++ b/.claude/skills/type-checker-tests/SKILL.md
@@ -16,6 +16,7 @@ Use this skill when adding new type checker functions or expanding behavior.
 |--------|---------|
 | Find next test number | `ls tests-integration/fixtures/checking/ \| tail -5` |
 | Run a test or multiple tests | `just tc NNN` or `just tc 101 102` |
+| Run with tracing enabled | `just tc --debug NNN` |
 | Run all checking tests | `just tc` |
 | Accept all pending snapshots | `cargo insta accept` |
 
@@ -162,6 +163,55 @@ When investigating a potential compiler bug:
 ```bash
 # Focus on single test to reduce noise
 just tc NNN
+
+# Enable tracing to see type checker behaviour
+just tc --debug NNN
+```
+
+### Trace Files
+
+The `--debug` flag emits detailed type checker traces to `target/compiler-tracing/`.
+
+**Trace file naming:** `{test_id}_{module_name}.jsonl`
+- Example: `200_int_compare_transitive_Main.jsonl`
+
+**Output format:** JSON Lines (one JSON object per line), containing:
+- `timestamp` - when the event occurred
+- `level` - DEBUG, INFO, or TRACE
+- `fields` - trace data (e.g., types being unified)
+- `target` - the module emitting the trace (e.g., `checking::algorithm::unification`)
+- `span`/`spans` - current span and span stack
+
+**Example trace line:**
+```json
+{"timestamp":"...","level":"DEBUG","fields":{"t1":"?0","t2":"Int"},"target":"checking::algorithm::unification","span":{"name":"unify"}}
+```
+
+When `--debug` is used, the trace file path is shown alongside pending snapshots:
+```
+UPDATED tests-integration/fixtures/checking/200_int_compare_transitive/Main.snap
+  TRACE target/compiler-tracing/200_int_compare_transitive_Main.jsonl
+```
+
+### Analysing Traces
+
+Trace files can be large for complex tests. Use sampling and filtering:
+
+```bash
+# Check file size and line count
+wc -l target/compiler-tracing/NNN_*.jsonl
+
+# Sample random lines to get an overview
+shuf -n 20 target/compiler-tracing/NNN_*.jsonl | jq .
+
+# Filter by level
+jq 'select(.level == "DEBUG")' target/compiler-tracing/NNN_*.jsonl
+
+# Filter by target module
+jq 'select(.target | contains("unification"))' target/compiler-tracing/NNN_*.jsonl
+
+# Extract specific fields
+jq '{level, target, fields}' target/compiler-tracing/NNN_*.jsonl
 ```
 
 You should run `just tc` to check for regressions.
diff --git a/Cargo.lock b/Cargo.lock
index 606acdd2..d3543b09 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -278,12 +278,15 @@ dependencies = [
  "interner",
  "itertools 0.14.0",
  "lowering",
+ "parsing",
  "petgraph",
  "pretty",
  "resolving",
  "rustc-hash 2.1.1",
  "smol_str",
+ "stabilizing",
  "sugar",
+ "tracing",
 ]
 
 [[package]]
@@ -1094,6 +1097,15 @@ dependencies = [
  "url",
 ]
 
+[[package]]
+name = "matchers"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d1525a2a28c7f4fa0fc98bb91ae755d1e2d1505079e05539e35bc876b5d65ae9"
+dependencies = [
+ "regex-automata",
+]
+
 [[package]]
 name = "md-5"
 version = "0.10.6"
@@ -1373,6 +1385,7 @@ version = "0.0.9"
 dependencies = [
  "analyzer",
  "async-lsp",
+ "checking",
  "clap",
  "files",
  "globset",
@@ -1853,10 +1866,13 @@ dependencies = [
  "line-index",
  "lowering",
  "rowan",
+ "serde_json",
  "stabilizing",
  "sugar",
  "syntax",
  "tabled",
+ "tracing",
+ "tracing-subscriber",
  "url",
 ]
 
@@ -2038,18 +2054,35 @@ dependencies = [
  "tracing-core",
 ]
 
+[[package]]
+name = "tracing-serde"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "704b1aeb7be0d0a84fc9828cae51dab5970fee5088f83d1dd7ee6f6246fc6ff1"
+dependencies = [
+ "serde",
+ "tracing-core",
+]
+
 [[package]]
 name = "tracing-subscriber"
 version = "0.3.22"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "2f30143827ddab0d256fd843b7a66d164e9f271cfa0dde49142c5ca0ca291f1e"
 dependencies = [
+ "matchers",
  "nu-ansi-term",
+ "once_cell",
+ "regex-automata",
+ "serde",
+ "serde_json",
  "sharded-slab",
  "smallvec",
  "thread_local",
+ "tracing",
  "tracing-core",
  "tracing-log",
+ "tracing-serde",
 ]
 
 [[package]]
diff --git a/compiler-bin/Cargo.toml b/compiler-bin/Cargo.toml
index 0cc95a58..9e32f00a 100644
--- a/compiler-bin/Cargo.toml
+++ b/compiler-bin/Cargo.toml
@@ -11,7 +11,12 @@ repository = "https://github.com/purefunctor/purescript-analyzer"
 keywords = ["purescript", "language server"]
 categories = ["compilers"]
 
+[features]
+default = []
+no-tracing = ["checking/no-tracing"]
+
 [dependencies]
+checking = { version = "0.1.0", path = "../compiler-core/checking" }
 analyzer = { version = "0.1.0", path = "../compiler-lsp/analyzer" }
 async-lsp = "0.2.2"
 clap = { version = "4.5.53", features = ["derive"] }
diff --git a/compiler-bin/src/cli.rs b/compiler-bin/src/cli.rs
index 98bd37a0..bc7859ad 100644
--- a/compiler-bin/src/cli.rs
+++ b/compiler-bin/src/cli.rs
@@ -24,6 +24,13 @@ pub struct Config {
         default_value("info")
     )]
     pub lsp_log: LevelFilter,
+    #[arg(
+        long,
+        value_name("LevelFilter"),
+        help("Log level for the type checker"),
+        default_value("off")
+    )]
+    pub checking_log: LevelFilter,
     #[arg(
         long,
         help("Command to use to get source files"),
diff --git a/compiler-bin/src/logging.rs b/compiler-bin/src/logging.rs
index 19aeb00d..9cae72c3 100644
--- a/compiler-bin/src/logging.rs
+++ b/compiler-bin/src/logging.rs
@@ -51,6 +51,7 @@ pub fn start(config: Arc<cli::Config>) {
     let fmt_filter = filter::Targets::new()
         .with_target("building::engine", config.query_log)
         .with_target("purescript_analyzer::lsp", config.lsp_log)
+        .with_target("checking", config.checking_log)
         .with_default(LevelFilter::INFO);
     let fmt = fmt::layer().with_writer(file).with_filter(fmt_filter);
 
diff --git a/compiler-core/checking/Cargo.toml b/compiler-core/checking/Cargo.toml
index 1f6303bc..e38cfe9e 100644
--- a/compiler-core/checking/Cargo.toml
+++ b/compiler-core/checking/Cargo.toml
@@ -3,7 +3,12 @@ name = "checking"
 version = "0.1.0"
 edition = "2024"
 
+[features]
+default = []
+no-tracing = ["tracing/max_level_off"]
+
 [dependencies]
+tracing = "0.1.44"
 building-types = { version = "0.1.0", path = "../building-types" }
 files = { version = "0.1.0", path = "../files" }
 indexing = { version = "0.1.0", path = "../indexing" }
@@ -11,9 +16,11 @@ indexmap = "2.12.1"
 interner = { version = "0.1.0", path = "../interner" }
 itertools = "0.14.0"
 lowering = { version = "0.1.0", path = "../lowering" }
+parsing = { version = "0.1.0", path = "../parsing" }
 petgraph = "0.8.3"
 pretty = "0.12"
 resolving = { version = "0.1.0", path = "../resolving" }
 rustc-hash = "2.1.1"
 smol_str = "0.3.4"
+stabilizing = { version = "0.1.0", path = "../stabilizing" }
 sugar = { version = "0.1.0", path = "../sugar" }
diff --git a/compiler-core/checking/src/algorithm/constraint.rs b/compiler-core/checking/src/algorithm/constraint.rs
index d76d7d4e..671fb025 100644
--- a/compiler-core/checking/src/algorithm/constraint.rs
+++ b/compiler-core/checking/src/algorithm/constraint.rs
@@ -19,11 +19,12 @@ use rustc_hash::{FxHashMap, FxHashSet};
 
 use crate::algorithm::fold::{FoldAction, TypeFold, fold_type};
 use crate::algorithm::state::{CheckContext, CheckState};
-use crate::algorithm::visit::CollectFileReferences;
+use crate::algorithm::visit::{CollectFileReferences, TypeVisitor, VisitAction, visit_type};
 use crate::algorithm::{toolkit, transfer, unification};
 use crate::core::{Class, Instance, InstanceKind, Variable, debruijn};
 use crate::{CheckedModule, ExternalQueries, Type, TypeId};
 
+#[tracing::instrument(skip_all, name = "solve_constraints")]
 pub fn solve_constraints<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -33,6 +34,11 @@ pub fn solve_constraints<Q>(
 where
     Q: ExternalQueries,
 {
+    crate::debug_fields!(state, context, {
+        ?wanted = wanted.len(),
+        ?given = given.len(),
+    });
+
     let given = elaborate_given(state, context, given)?;
 
     let mut work_queue = wanted;
@@ -42,6 +48,8 @@ where
         let mut made_progress = false;
 
         'work: while let Some(wanted) = work_queue.pop_front() {
+            crate::trace_fields!(state, context, { wanted = wanted }, "work");
+
             let Some(application) = constraint_application(state, wanted) else {
                 residual.push(wanted);
                 continue;
@@ -106,6 +114,8 @@ where
         }
     }
 
+    crate::debug_fields!(state, context, { ?residual = residual.len() });
+
     Ok(residual)
 }
 
@@ -646,61 +656,84 @@ fn can_unify(state: &mut CheckState, t1: TypeId, t2: TypeId) -> CanUnify {
 
         (Type::Row(_), Type::Row(_)) => Unify,
 
-        (&Type::Application(f1, a1), &Type::Application(f2, a2)) => {
-            can_unify(state, f1, f2).and_also(|| can_unify(state, a1, a2))
+        (
+            &Type::Application(t1_function, t1_argument),
+            &Type::Application(t2_function, t2_argument),
+        ) => can_unify(state, t1_function, t2_function)
+            .and_also(|| can_unify(state, t1_argument, t2_argument)),
+
+        (&Type::Function(t1_argument, t1_result), &Type::Function(t2_argument, t2_result)) => {
+            can_unify(state, t1_argument, t2_argument)
+                .and_also(|| can_unify(state, t1_result, t2_result))
         }
 
-        (&Type::Function(a1, r1), &Type::Function(a2, r2)) => {
-            can_unify(state, a1, a2).and_also(|| can_unify(state, r1, r2))
-        }
+        (
+            &Type::KindApplication(t1_function, t1_argument),
+            &Type::KindApplication(t2_function, t2_argument),
+        ) => can_unify(state, t1_function, t2_function)
+            .and_also(|| can_unify(state, t1_argument, t2_argument)),
 
-        (&Type::KindApplication(f1, a1), &Type::KindApplication(f2, a2)) => {
-            can_unify(state, f1, f2).and_also(|| can_unify(state, a1, a2))
+        (&Type::Kinded(t1_type, t1_kind), &Type::Kinded(t2_type, t2_kind)) => {
+            can_unify(state, t1_type, t2_type).and_also(|| can_unify(state, t1_kind, t2_kind))
         }
 
-        (&Type::Kinded(t1, k1), &Type::Kinded(t2, k2)) => {
-            can_unify(state, t1, t2).and_also(|| can_unify(state, k1, k2))
-        }
+        (
+            &Type::Constrained(t1_constraint, t1_body),
+            &Type::Constrained(t2_constraint, t2_body),
+        ) => can_unify(state, t1_constraint, t2_constraint)
+            .and_also(|| can_unify(state, t1_body, t2_body)),
 
-        (&Type::Constrained(c1, b1), &Type::Constrained(c2, b2)) => {
-            can_unify(state, c1, c2).and_also(|| can_unify(state, b1, b2))
+        (&Type::Forall(_, t1_body), &Type::Forall(_, t2_body)) => {
+            can_unify(state, t1_body, t2_body)
         }
 
-        (&Type::Forall(_, b1), &Type::Forall(_, b2)) => can_unify(state, b1, b2),
-
         (
-            &Type::OperatorApplication(f1, t1, l1, r1),
-            &Type::OperatorApplication(f2, t2, l2, r2),
+            &Type::OperatorApplication(t1_file, t1_item, t1_left, t1_right),
+            &Type::OperatorApplication(t2_file, t2_item, t2_left, t2_right),
         ) => {
-            if f1 == f2 && t1 == t2 {
-                can_unify(state, l1, l2).and_also(|| can_unify(state, r1, r2))
+            if t1_file == t2_file && t1_item == t2_item {
+                can_unify(state, t1_left, t2_left).and_also(|| can_unify(state, t1_right, t2_right))
             } else {
                 Apart
             }
         }
 
-        (Type::SynonymApplication(_, f1, t1, a1), Type::SynonymApplication(_, f2, t2, a2)) => {
-            if f1 == f2 && t1 == t2 && a1.len() == a2.len() {
-                let a1 = Arc::clone(a1);
-                let a2 = Arc::clone(a2);
-                iter::zip(a1.iter(), a2.iter())
-                    .fold(Equal, |result, (&a1, &a2)| result.and_also(|| can_unify(state, a1, a2)))
+        (
+            Type::SynonymApplication(_, t1_file, t1_item, t1_arguments),
+            Type::SynonymApplication(_, t2_file, t2_item, t2_arguments),
+        ) => {
+            if t1_file == t2_file && t1_item == t2_item && t1_arguments.len() == t2_arguments.len()
+            {
+                let t1_arguments = Arc::clone(t1_arguments);
+                let t2_arguments = Arc::clone(t2_arguments);
+                iter::zip(t1_arguments.iter(), t2_arguments.iter()).fold(
+                    Equal,
+                    |result, (&t1_argument, &t2_argument)| {
+                        result.and_also(|| can_unify(state, t1_argument, t2_argument))
+                    },
+                )
             } else {
                 Apart
             }
         }
 
-        (&Type::Variable(Variable::Bound(l1, k1)), &Type::Variable(Variable::Bound(l2, k2))) => {
-            if l1 == l2 {
-                can_unify(state, k1, k2)
+        (
+            &Type::Variable(Variable::Bound(t1_level, t1_kind)),
+            &Type::Variable(Variable::Bound(t2_level, t2_kind)),
+        ) => {
+            if t1_level == t2_level {
+                can_unify(state, t1_kind, t2_kind)
             } else {
                 Apart
             }
         }
 
-        (&Type::Variable(Variable::Skolem(l1, k1)), &Type::Variable(Variable::Skolem(l2, k2))) => {
-            if l1 == l2 {
-                can_unify(state, k1, k2)
+        (
+            &Type::Variable(Variable::Skolem(t1_level, t1_kind)),
+            &Type::Variable(Variable::Skolem(t2_level, t2_kind)),
+        ) => {
+            if t1_level == t2_level {
+                can_unify(state, t1_kind, t2_kind)
             } else {
                 Apart
             }
@@ -711,6 +744,7 @@ fn can_unify(state: &mut CheckState, t1: TypeId, t2: TypeId) -> CanUnify {
 }
 
 /// Matches a wanted constraint to an instance.
+#[tracing::instrument(skip_all, name = "match_instance")]
 fn match_instance<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -733,6 +767,7 @@ where
         let match_result = match_type(state, &mut bindings, &mut equalities, *wanted, given);
 
         if matches!(match_result, MatchType::Apart) {
+            crate::trace_fields!(state, context, { ?wanted = wanted, ?given = given }, "apart");
             return Ok(MatchInstance::Apart);
         }
 
@@ -745,6 +780,7 @@ where
 
     if !stuck_positions.is_empty() {
         if !can_determine_stuck(context, file_id, item_id, &match_results, &stuck_positions)? {
+            crate::trace_fields!(state, context, { ?wanted = wanted }, "stuck");
             return Ok(MatchInstance::Stuck);
         }
 
@@ -775,7 +811,7 @@ where
         }
     }
 
-    let constraints = instance
+    let constraints: Vec<_> = instance
         .constraints
         .iter()
         .map(|(constraint, _)| {
@@ -784,6 +820,11 @@ where
         })
         .collect();
 
+    crate::trace_fields!(state, context, {
+        ?constraints = constraints.len(),
+        ?equalities = equalities.len()
+    }, "match");
+
     Ok(MatchInstance::Match { constraints, equalities })
 }
 
@@ -953,19 +994,16 @@ struct CollectBoundLevels<'a> {
 
 impl<'a> CollectBoundLevels<'a> {
     fn on(state: &mut CheckState, type_id: TypeId, levels: &'a mut FxHashSet<debruijn::Level>) {
-        fold_type(state, type_id, &mut CollectBoundLevels { levels });
+        visit_type(state, type_id, &mut CollectBoundLevels { levels });
     }
 }
 
-impl TypeFold for CollectBoundLevels<'_> {
-    fn transform(&mut self, _state: &mut CheckState, id: TypeId, t: &Type) -> FoldAction {
-        match t {
-            Type::Variable(Variable::Bound(level, _)) => {
-                self.levels.insert(*level);
-                FoldAction::Replace(id)
-            }
-            _ => FoldAction::Continue,
+impl TypeVisitor for CollectBoundLevels<'_> {
+    fn visit(&mut self, _state: &mut CheckState, _id: TypeId, t: &Type) -> VisitAction {
+        if let Type::Variable(Variable::Bound(level, _)) = t {
+            self.levels.insert(*level);
         }
+        VisitAction::Continue
     }
 }
 
@@ -980,18 +1018,15 @@ impl<'a> CollectBoundVariables<'a> {
         type_id: TypeId,
         variables: &'a mut FxHashMap<debruijn::Level, TypeId>,
     ) {
-        fold_type(state, type_id, &mut CollectBoundVariables { variables });
+        visit_type(state, type_id, &mut CollectBoundVariables { variables });
     }
 }
 
-impl TypeFold for CollectBoundVariables<'_> {
-    fn transform(&mut self, _state: &mut CheckState, id: TypeId, t: &Type) -> FoldAction {
-        match t {
-            Type::Variable(Variable::Bound(level, kind)) => {
-                self.variables.insert(*level, *kind);
-                FoldAction::Replace(id)
-            }
-            _ => FoldAction::Continue,
+impl TypeVisitor for CollectBoundVariables<'_> {
+    fn visit(&mut self, _state: &mut CheckState, _id: TypeId, t: &Type) -> VisitAction {
+        if let Type::Variable(Variable::Bound(level, kind)) = t {
+            self.variables.insert(*level, *kind);
         }
+        VisitAction::Continue
     }
 }
diff --git a/compiler-core/checking/src/algorithm/kind.rs b/compiler-core/checking/src/algorithm/kind.rs
index 751f9ae4..044f81b2 100644
--- a/compiler-core/checking/src/algorithm/kind.rs
+++ b/compiler-core/checking/src/algorithm/kind.rs
@@ -17,6 +17,7 @@ use crate::error::ErrorStep;
 
 const MISSING_NAME: SmolStr = SmolStr::new_static("<MissingName>");
 
+#[tracing::instrument(skip_all, name = "infer_surface_kind")]
 pub fn infer_surface_kind<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -26,7 +27,9 @@ where
     Q: ExternalQueries,
 {
     state.with_error_step(ErrorStep::InferringKind(id), |state| {
-        infer_surface_kind_core(state, context, id)
+        let (t, k) = infer_surface_kind_core(state, context, id)?;
+        crate::trace_fields!(state, context, { inferred_type = t, inferred_kind = k });
+        Ok((t, k))
     })
 }
 
@@ -403,6 +406,7 @@ where
     }
 }
 
+#[tracing::instrument(skip_all, name = "elaborate_kind")]
 pub fn elaborate_kind<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -411,6 +415,8 @@ pub fn elaborate_kind<Q>(
 where
     Q: ExternalQueries,
 {
+    crate::trace_fields!(state, context, { type_ = id });
+
     let unknown = context.prim.unknown;
     let id = state.normalize_type(id);
 
@@ -519,6 +525,7 @@ where
     Ok(type_id)
 }
 
+#[tracing::instrument(skip_all, name = "check_surface_kind")]
 pub fn check_surface_kind<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -528,9 +535,16 @@ pub fn check_surface_kind<Q>(
 where
     Q: ExternalQueries,
 {
+    crate::trace_fields!(state, context, { expected_kind = kind });
+
     state.with_error_step(ErrorStep::CheckingKind(id), |state| {
         let (inferred_type, inferred_kind) = infer_surface_kind_core(state, context, id)?;
         let _ = unification::subtype(state, context, inferred_kind, kind)?;
+        crate::trace_fields!(state, context, {
+            inferred_type = inferred_type,
+            inferred_kind = inferred_kind,
+            expected_kind = kind
+        });
         Ok((inferred_type, inferred_kind))
     })
 }
diff --git a/compiler-core/checking/src/algorithm/state.rs b/compiler-core/checking/src/algorithm/state.rs
index 618f9874..4009aff6 100644
--- a/compiler-core/checking/src/algorithm/state.rs
+++ b/compiler-core/checking/src/algorithm/state.rs
@@ -15,6 +15,7 @@ use lowering::{
 };
 use resolving::ResolvedModule;
 use rustc_hash::FxHashMap;
+use stabilizing::StabilizedModule;
 use sugar::{Bracketed, Sectioned};
 
 use crate::algorithm::{constraint, transfer};
@@ -343,6 +344,7 @@ where
     pub known_generic: Option<KnownGeneric>,
 
     pub id: FileId,
+    pub stabilized: Arc<StabilizedModule>,
     pub indexed: Arc<IndexedModule>,
     pub lowered: Arc<LoweredModule>,
     pub grouped: Arc<GroupedModule>,
@@ -363,6 +365,7 @@ where
         state: &mut CheckState,
         id: FileId,
     ) -> QueryResult<CheckContext<'a, Q>> {
+        let stabilized = queries.stabilized(id)?;
         let indexed = queries.indexed(id)?;
         let lowered = queries.lowered(id)?;
         let grouped = queries.grouped(id)?;
@@ -399,6 +402,7 @@ where
             known_reflectable,
             known_generic,
             id,
+            stabilized,
             indexed,
             lowered,
             grouped,
diff --git a/compiler-core/checking/src/algorithm/substitute.rs b/compiler-core/checking/src/algorithm/substitute.rs
index 51954ca3..d64c9323 100644
--- a/compiler-core/checking/src/algorithm/substitute.rs
+++ b/compiler-core/checking/src/algorithm/substitute.rs
@@ -57,7 +57,8 @@ impl TypeFold for ShiftBound {
     fn transform(&mut self, state: &mut CheckState, _id: TypeId, t: &Type) -> FoldAction {
         if let Type::Variable(Variable::Bound(level, kind)) = t {
             let level = debruijn::Level(level.0 + self.offset);
-            FoldAction::Replace(state.storage.intern(Type::Variable(Variable::Bound(level, *kind))))
+            let kind = ShiftBound::on(state, *kind, self.offset);
+            FoldAction::Replace(state.storage.intern(Type::Variable(Variable::Bound(level, kind))))
         } else {
             FoldAction::Continue
         }
@@ -88,6 +89,7 @@ impl TypeFold for SubstituteUnification<'_> {
     fn transform(&mut self, state: &mut CheckState, id: TypeId, t: &Type) -> FoldAction {
         if let Type::Unification(unification_id) = t {
             if let Some(&(level, kind)) = self.substitutions.get(unification_id) {
+                let kind = SubstituteUnification::on(self.substitutions, state, kind);
                 return FoldAction::Replace(
                     state.storage.intern(Type::Variable(Variable::Bound(level, kind))),
                 );
diff --git a/compiler-core/checking/src/algorithm/term.rs b/compiler-core/checking/src/algorithm/term.rs
index bee5fe78..4a102c42 100644
--- a/compiler-core/checking/src/algorithm/term.rs
+++ b/compiler-core/checking/src/algorithm/term.rs
@@ -272,6 +272,7 @@ where
 }
 
 /// Checks the type of an expression.
+#[tracing::instrument(skip_all, name = "check_expression")]
 pub fn check_expression<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -281,14 +282,17 @@ pub fn check_expression<Q>(
 where
     Q: ExternalQueries,
 {
+    crate::trace_fields!(state, context, { expected = expected });
     state.with_error_step(ErrorStep::CheckingExpression(expr_id), |state| {
         let inferred = infer_expression_quiet(state, context, expr_id)?;
         let _ = unification::subtype(state, context, inferred, expected)?;
+        crate::trace_fields!(state, context, { inferred = inferred, expected = expected });
         Ok(inferred)
     })
 }
 
 /// Infers the type of an expression.
+#[tracing::instrument(skip_all, name = "infer_expression")]
 pub fn infer_expression<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -298,7 +302,9 @@ where
     Q: ExternalQueries,
 {
     state.with_error_step(ErrorStep::InferringExpression(expr_id), |state| {
-        infer_expression_quiet(state, context, expr_id)
+        let inferred = infer_expression_quiet(state, context, expr_id)?;
+        crate::trace_fields!(state, context, { inferred = inferred });
+        Ok(inferred)
     })
 }
 
@@ -1277,6 +1283,7 @@ where
 /// [`lowering::ExpressionKind::Do`] and [`lowering::ExpressionKind::Ado`].
 ///
 /// [`check_constructor_binder_application`]: binder::check_constructor_binder_application
+#[tracing::instrument(skip_all, name = "check_function_application")]
 pub fn check_function_application_core<Q, A, F>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -1288,6 +1295,7 @@ where
     Q: ExternalQueries,
     F: FnOnce(&mut CheckState, &CheckContext<Q>, A, TypeId) -> QueryResult<TypeId>,
 {
+    crate::trace_fields!(state, context, { function = function_t });
     let function_t = state.normalize_type(function_t);
     match state.storage[function_t] {
         // Check that `argument_id :: argument_type`
diff --git a/compiler-core/checking/src/algorithm/term_item.rs b/compiler-core/checking/src/algorithm/term_item.rs
index a7fdb104..007db08e 100644
--- a/compiler-core/checking/src/algorithm/term_item.rs
+++ b/compiler-core/checking/src/algorithm/term_item.rs
@@ -39,6 +39,8 @@ where
     Q: ExternalQueries,
 {
     state.with_error_step(ErrorStep::TermDeclaration(item_id), |state| {
+        let _span = tracing::debug_span!("check_term_signature").entered();
+
         let Some(item) = context.lowered.info.get_term_item(item_id) else {
             return Ok(());
         };
@@ -57,6 +59,8 @@ where
                     .map(|(quantified_type, _)| quantified_type)
                     .unwrap_or(inferred_type);
 
+                crate::debug_fields!(state, context, { quantified_type = quantified_type });
+
                 let global_type = transfer::globalize(state, context, quantified_type);
                 state.checked.terms.insert(item_id, global_type);
             }
@@ -106,10 +110,14 @@ where
 {
     let CheckInstance { item_id, constraints, arguments, resolution } = input;
     state.with_error_step(ErrorStep::TermDeclaration(item_id), |state| {
+        let _span = tracing::debug_span!("check_instance").entered();
+
         let Some((class_file, class_item)) = *resolution else {
             return Ok(());
         };
 
+        crate::debug_fields!(state, context, { ?class_file = class_file, ?class_item = class_item });
+
         let TermItemKind::Instance { id: instance_id } = context.indexed.items[item_id].kind else {
             return Ok(());
         };
@@ -252,6 +260,7 @@ where
 {
     let CheckValueGroup { item_id, signature, equations } = input;
     state.with_error_step(ErrorStep::TermDeclaration(item_id), |state| {
+        let _span = tracing::debug_span!("check_value_group").entered();
         if let Some(signature_id) = signature {
             let group_type = term::lookup_file_term(state, context, context.id, item_id)?;
 
@@ -262,10 +271,12 @@ where
                 inspect::inspect_signature_core(state, context, group_type, surface_bindings)?;
 
             term::check_equations(state, context, *signature_id, signature, equations)?;
+            crate::debug_fields!(state, context, { group_type = group_type }, "checking");
             Ok(None)
         } else {
             let (inferred_type, residual_constraints) =
                 term::infer_equations(state, context, item_id, equations)?;
+            crate::debug_fields!(state, context, { inferred_type = inferred_type }, "inferring");
             Ok(Some(InferredValueGroup { inferred_type, residual_constraints }))
         }
     })
@@ -290,6 +301,7 @@ where
     };
 
     state.with_error_step(ErrorStep::TermDeclaration(item_id), |state| {
+        let _span = tracing::debug_span!("commit_value_group").entered();
         for constraint in result.ambiguous {
             let constraint = transfer::globalize(state, context, constraint);
             state.insert_error(ErrorKind::AmbiguousConstraint { constraint });
@@ -298,6 +310,7 @@ where
             let constraint = transfer::globalize(state, context, constraint);
             state.insert_error(ErrorKind::NoInstanceFound { constraint });
         }
+        crate::debug_fields!(state, context, { quantified = result.quantified });
     });
 
     let type_id = transfer::globalize(state, context, result.quantified);
@@ -435,6 +448,8 @@ where
     } = input;
 
     state.with_error_step(ErrorStep::TermDeclaration(instance_id), |state| {
+        let _span = tracing::debug_span!("check_instance_member_group").entered();
+
         // Save the current size of the environment for unbinding.
         let size = state.type_scope.size();
 
diff --git a/compiler-core/checking/src/algorithm/transfer.rs b/compiler-core/checking/src/algorithm/transfer.rs
index 7be62ec8..69894497 100644
--- a/compiler-core/checking/src/algorithm/transfer.rs
+++ b/compiler-core/checking/src/algorithm/transfer.rs
@@ -30,6 +30,7 @@ use crate::core::{RowType, Variable};
 use crate::{ExternalQueries, Type, TypeId};
 
 /// Moves a type from local memory to global memory.
+#[tracing::instrument(skip_all, name = "localise")]
 pub fn localize<Q>(state: &mut CheckState, context: &CheckContext<Q>, id: TypeId) -> TypeId
 where
     Q: ExternalQueries,
@@ -40,6 +41,7 @@ where
 }
 
 /// Moves a type from global memory to local memory.
+#[tracing::instrument(skip_all, name = "globalise")]
 pub fn globalize<Q>(state: &mut CheckState, context: &CheckContext<Q>, id: TypeId) -> TypeId
 where
     Q: ExternalQueries,
@@ -146,13 +148,13 @@ fn traverse<'a, Q: ExternalQueries>(source: &mut TraversalSource<'a, Q>, id: Typ
             Type::SynonymApplication(saturation, file_id, type_id, arguments)
         }
 
-        Type::Unification(_) => match source.mode {
+        Type::Unification(unification_id) => match source.mode {
             TraversalMode::FromGlobal => {
-                // eprintln!("localize: unification variable ?{unification_id} escaped");
+                tracing::trace!(unification_id = ?unification_id, "escaped unification variable");
                 Type::Unknown
             }
             TraversalMode::FromLocal => {
-                // eprintln!("globalize: unification variable ?{unification_id} escaped");
+                tracing::trace!(unification_id = ?unification_id, "escaped unification variable");
                 Type::Unknown
             }
         },
diff --git a/compiler-core/checking/src/algorithm/type_item.rs b/compiler-core/checking/src/algorithm/type_item.rs
index 202bd8fa..cdcfab9e 100644
--- a/compiler-core/checking/src/algorithm/type_item.rs
+++ b/compiler-core/checking/src/algorithm/type_item.rs
@@ -73,6 +73,8 @@ where
     Q: ExternalQueries,
 {
     state.with_error_step(ErrorStep::TypeDeclaration(item_id), |state| {
+        let _span = tracing::debug_span!("check_type_item").entered();
+
         let Some(item) = context.lowered.info.get_type_item(item_id) else {
             return Ok(None);
         };
@@ -168,6 +170,8 @@ where
         state.type_scope.unbind(level);
     }
 
+    crate::debug_fields!(state, context, { inferred_kind = inferred_kind });
+
     Ok(Some(CheckedTypeItem::Data(CheckedData {
         inferred_kind,
         kind_variables,
@@ -216,6 +220,8 @@ where
         state.type_scope.unbind(variable.level);
     }
 
+    crate::debug_fields!(state, context, { synonym_type = synonym_type });
+
     Ok(Some(CheckedTypeItem::Synonym(CheckedSynonym {
         inferred_kind,
         kind_variables,
@@ -287,6 +293,8 @@ where
         state.type_scope.unbind(variable.level);
     }
 
+    crate::debug_fields!(state, context, { ?superclass_count = superclasses.len(), ?member_count = members.len() });
+
     Ok(Some(CheckedTypeItem::Class(CheckedClass {
         inferred_kind,
         kind_variables,
@@ -630,6 +638,8 @@ where
     Q: ExternalQueries,
 {
     state.with_error_step(ErrorStep::TypeDeclaration(item_id), |state| {
+        let _span = tracing::debug_span!("check_type_signature").entered();
+
         let Some(item) = context.lowered.info.get_type_item(item_id) else {
             return Ok(());
         };
@@ -831,6 +841,7 @@ fn check_constructor_arguments<Q>(
 where
     Q: ExternalQueries,
 {
+    let _span = tracing::debug_span!("check_constructor_arguments").entered();
     let mut constructors = vec![];
 
     for item_id in context.indexed.pairs.data_constructors(item_id) {
@@ -840,24 +851,33 @@ where
             continue;
         };
 
-        let mut inferred_arguments = vec![];
-
-        for &argument in arguments.iter() {
-            let inferred_type =
-                state.with_error_step(ErrorStep::ConstructorArgument(argument), |state| {
-                    let (inferred_type, _) =
-                        kind::check_surface_kind(state, context, argument, context.prim.t)?;
-                    Ok(inferred_type)
-                })?;
-            inferred_arguments.push(inferred_type);
-        }
+        let arguments = arguments
+            .iter()
+            .map(|argument| infer_constructor_argument(state, context, *argument))
+            .try_collect()?;
 
-        constructors.push(CheckedConstructor { item_id, arguments: inferred_arguments });
+        constructors.push(CheckedConstructor { item_id, arguments });
     }
 
     Ok(constructors)
 }
 
+fn infer_constructor_argument<Q>(
+    state: &mut CheckState,
+    context: &CheckContext<Q>,
+    argument: lowering::TypeId,
+) -> Result<interner::Id<Type>, building_types::QueryError>
+where
+    Q: ExternalQueries,
+{
+    state.with_error_step(ErrorStep::ConstructorArgument(argument), |state| {
+        let _span = tracing::debug_span!("infer_constructor_argument").entered();
+        let (inferred_type, _) =
+            kind::check_surface_kind(state, context, argument, context.prim.t)?;
+        Ok(inferred_type)
+    })
+}
+
 /// Infers roles for type parameters based on their usage in constructors.
 fn infer_roles(
     state: &mut CheckState,
diff --git a/compiler-core/checking/src/algorithm/unification.rs b/compiler-core/checking/src/algorithm/unification.rs
index ff5c1cd4..8a94f56c 100644
--- a/compiler-core/checking/src/algorithm/unification.rs
+++ b/compiler-core/checking/src/algorithm/unification.rs
@@ -42,6 +42,7 @@ use crate::error::ErrorKind;
 ///   subtype (?a -> ?a) (~a -> ~a)
 ///     subtype ?a ~a
 /// ```
+#[tracing::instrument(skip_all, name = "subtype")]
 pub fn subtype<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -54,7 +55,10 @@ where
     let t1 = synonym::normalize_expand_type(state, context, t1)?;
     let t2 = synonym::normalize_expand_type(state, context, t2)?;
 
+    crate::debug_fields!(state, context, { t1 = t1, t2 = t2 });
+
     if t1 == t2 {
+        crate::trace_fields!(state, context, { t1 = t1, t2 = t2 }, "identical");
         return Ok(true);
     }
 
@@ -92,6 +96,7 @@ where
     }
 }
 
+#[tracing::instrument(skip_all, name = "unify")]
 pub fn unify<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -104,7 +109,10 @@ where
     let t1 = synonym::normalize_expand_type(state, context, t1)?;
     let t2 = synonym::normalize_expand_type(state, context, t2)?;
 
+    crate::debug_fields!(state, context, { t1 = t1, t2 = t2 });
+
     if t1 == t2 {
+        crate::trace_fields!(state, context, { t1 = t1, t2 = t2 }, "identical");
         return Ok(true);
     }
 
@@ -172,6 +180,7 @@ where
     Ok(unifies)
 }
 
+#[tracing::instrument(skip_all, name = "solve")]
 pub fn solve<Q>(
     state: &mut CheckState,
     context: &CheckContext<Q>,
@@ -181,10 +190,18 @@ pub fn solve<Q>(
 where
     Q: ExternalQueries,
 {
+    crate::trace_fields!(state, context, {
+        ?unification_id = unification_id,
+        solution = solution,
+    });
+
     let codomain = state.type_scope.size();
-    let occurs = unification_id;
 
-    if !promote_type(state, occurs, codomain, unification_id, solution) {
+    if !promote_type(state, codomain, unification_id, solution) {
+        crate::trace_fields!(state, context, {
+            ?unification_id = unification_id,
+            solution = solution,
+        }, "occurs check failed");
         return Ok(None);
     }
 
@@ -199,7 +216,6 @@ where
 
 pub fn promote_type(
     state: &mut CheckState,
-    occurs: u32,
     codomain: debruijn::Size,
     unification_id: u32,
     solution: TypeId,
@@ -207,58 +223,58 @@ pub fn promote_type(
     let solution = state.normalize_type(solution);
     match state.storage[solution] {
         Type::Application(function, argument) => {
-            promote_type(state, occurs, codomain, unification_id, function)
-                && promote_type(state, occurs, codomain, unification_id, argument)
+            promote_type(state, codomain, unification_id, function)
+                && promote_type(state, codomain, unification_id, argument)
         }
 
         Type::Constrained(constraint, inner) => {
-            promote_type(state, occurs, codomain, unification_id, constraint)
-                && promote_type(state, occurs, codomain, unification_id, inner)
+            promote_type(state, codomain, unification_id, constraint)
+                && promote_type(state, codomain, unification_id, inner)
         }
 
         Type::Constructor(_, _) => true,
 
         Type::Forall(ref binder, inner) => {
             let inner_codomain = codomain.increment();
-            promote_type(state, occurs, codomain, unification_id, binder.kind)
-                && promote_type(state, occurs, inner_codomain, unification_id, inner)
+            promote_type(state, codomain, unification_id, binder.kind)
+                && promote_type(state, inner_codomain, unification_id, inner)
         }
 
         Type::Function(argument, result) => {
-            promote_type(state, occurs, codomain, unification_id, argument)
-                && promote_type(state, occurs, codomain, unification_id, result)
+            promote_type(state, codomain, unification_id, argument)
+                && promote_type(state, codomain, unification_id, result)
         }
 
         Type::Integer(_) => true,
 
         Type::KindApplication(function, argument) => {
-            promote_type(state, occurs, codomain, unification_id, function)
-                && promote_type(state, occurs, codomain, unification_id, argument)
+            promote_type(state, codomain, unification_id, function)
+                && promote_type(state, codomain, unification_id, argument)
         }
 
         Type::Kinded(inner, kind) => {
-            promote_type(state, occurs, codomain, unification_id, inner)
-                && promote_type(state, occurs, codomain, unification_id, kind)
+            promote_type(state, codomain, unification_id, inner)
+                && promote_type(state, codomain, unification_id, kind)
         }
 
         Type::Operator(_, _) => true,
 
         Type::OperatorApplication(_, _, left, right) => {
-            promote_type(state, occurs, codomain, unification_id, left)
-                && promote_type(state, occurs, codomain, unification_id, right)
+            promote_type(state, codomain, unification_id, left)
+                && promote_type(state, codomain, unification_id, right)
         }
 
         Type::Row(RowType { ref fields, tail }) => {
             let fields = Arc::clone(fields);
 
             for field in fields.iter() {
-                if !promote_type(state, occurs, codomain, unification_id, field.id) {
+                if !promote_type(state, codomain, unification_id, field.id) {
                     return false;
                 }
             }
 
             if let Some(tail) = tail
-                && !promote_type(state, occurs, codomain, unification_id, tail)
+                && !promote_type(state, codomain, unification_id, tail)
             {
                 return false;
             }
@@ -271,7 +287,7 @@ pub fn promote_type(
         Type::SynonymApplication(_, _, _, ref arguments) => {
             let arguments = Arc::clone(arguments);
             for argument in arguments.iter() {
-                if !promote_type(state, occurs, codomain, unification_id, *argument) {
+                if !promote_type(state, codomain, unification_id, *argument) {
                     return false;
                 }
             }
@@ -282,7 +298,7 @@ pub fn promote_type(
             let unification = state.unification.get(unification_id);
             let solution = state.unification.get(solution_id);
 
-            if occurs == solution_id {
+            if unification_id == solution_id {
                 return false;
             }
 
@@ -306,11 +322,9 @@ pub fn promote_type(
                     if level.0 >= unification.domain.0 {
                         return false;
                     }
-                    promote_type(state, occurs, codomain, unification_id, *kind)
-                }
-                Variable::Skolem(_, kind) => {
-                    promote_type(state, occurs, codomain, unification_id, *kind)
+                    promote_type(state, codomain, unification_id, *kind)
                 }
+                Variable::Skolem(_, kind) => promote_type(state, codomain, unification_id, *kind),
                 Variable::Free(_) => true,
             }
         }
diff --git a/compiler-core/checking/src/lib.rs b/compiler-core/checking/src/lib.rs
index 91731e7e..06ec0273 100644
--- a/compiler-core/checking/src/lib.rs
+++ b/compiler-core/checking/src/lib.rs
@@ -1,5 +1,6 @@
 pub mod algorithm;
 pub mod error;
+pub mod trace;
 
 pub mod core;
 pub use core::{Type, TypeId, TypeInterner};
@@ -12,11 +13,14 @@ use indexing::{DeriveId, IndexedModule, InstanceId, TermItemId, TypeItemId};
 use lowering::{GroupedModule, LoweredModule};
 use resolving::ResolvedModule;
 use rustc_hash::FxHashMap;
+use stabilizing::StabilizedModule;
 
 use crate::error::CheckError;
 
 pub trait ExternalQueries:
     QueryProxy<
+        Parsed = parsing::FullParsedModule,
+        Stabilized = Arc<StabilizedModule>,
         Indexed = Arc<IndexedModule>,
         Lowered = Arc<LoweredModule>,
         Grouped = Arc<GroupedModule>,
@@ -75,6 +79,7 @@ impl CheckedModule {
 }
 
 pub fn check_module(queries: &impl ExternalQueries, file_id: FileId) -> QueryResult<CheckedModule> {
+    let _span = trace::check_module(queries, file_id)?;
     let prim_id = queries.prim_id();
     if file_id == prim_id {
         algorithm::check_prim(queries, prim_id)
diff --git a/compiler-core/checking/src/trace.rs b/compiler-core/checking/src/trace.rs
new file mode 100644
index 00000000..a452e84f
--- /dev/null
+++ b/compiler-core/checking/src/trace.rs
@@ -0,0 +1,315 @@
+//! Tracing infrastructure for type checker debugging.
+//!
+//! This module provides macros and helpers for emitting structured trace events
+//! with pretty-printed type information. All tracing is compiled out when the
+//! `no-tracing` feature is enabled.
+
+use building_types::QueryResult;
+
+use crate::ExternalQueries;
+use crate::algorithm::state::CheckContext;
+use crate::error::ErrorStep;
+
+/// Extracts the byte offset range from an error step.
+pub fn step_byte_range<Q>(step: &ErrorStep, context: &CheckContext<Q>) -> Option<(u32, u32)>
+where
+    Q: ExternalQueries,
+{
+    let pointer = match step {
+        ErrorStep::ConstructorArgument(id) => context.stabilized.syntax_ptr(*id)?,
+        ErrorStep::InferringKind(id) | ErrorStep::CheckingKind(id) => {
+            context.stabilized.syntax_ptr(*id)?
+        }
+        ErrorStep::InferringBinder(id) | ErrorStep::CheckingBinder(id) => {
+            context.stabilized.syntax_ptr(*id)?
+        }
+        ErrorStep::InferringExpression(id) | ErrorStep::CheckingExpression(id) => {
+            context.stabilized.syntax_ptr(*id)?
+        }
+        ErrorStep::TermDeclaration(id) => {
+            context.indexed.term_item_ptr(&context.stabilized, *id).next()?
+        }
+        ErrorStep::TypeDeclaration(id) => {
+            context.indexed.type_item_ptr(&context.stabilized, *id).next()?
+        }
+    };
+
+    let range = pointer.text_range();
+
+    let start = range.start().into();
+    let end = range.end().into();
+
+    Some((start, end))
+}
+
+/// Returns the byte offset range for the most specific (innermost) error step.
+pub fn current_offset<Q>(check_steps: &[ErrorStep], context: &CheckContext<Q>) -> Option<(u32, u32)>
+where
+    Q: ExternalQueries,
+{
+    check_steps.last().and_then(|step| step_byte_range(step, context))
+}
+
+#[cfg(not(feature = "no-tracing"))]
+mod enabled {
+    use std::fmt;
+
+    use crate::ExternalQueries;
+    use crate::algorithm::state::{CheckContext, CheckState};
+    use crate::core::TypeId;
+    use crate::core::pretty::print_local;
+
+    /// A rendered type for tracing output.
+    ///
+    /// Implements both [`fmt::Display`] for human-readable output and
+    /// [`fmt::Debug`] for JSON serialisation via tracing subscribers.
+    #[derive(Clone)]
+    pub struct TypeTrace(String);
+
+    impl fmt::Display for TypeTrace {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            f.write_str(&self.0)
+        }
+    }
+
+    impl fmt::Debug for TypeTrace {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            write!(f, "{:?}", self.0)
+        }
+    }
+
+    /// A trace value that can be either pretty-printed or debug-formatted.
+    pub enum TraceValue {
+        Pretty(TypeTrace),
+        Debug(String),
+    }
+
+    impl fmt::Display for TraceValue {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            match self {
+                TraceValue::Pretty(trace) => fmt::Display::fmt(trace, f),
+                TraceValue::Debug(s) => f.write_str(s),
+            }
+        }
+    }
+
+    impl fmt::Debug for TraceValue {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            match self {
+                TraceValue::Pretty(trace) => fmt::Debug::fmt(trace, f),
+                TraceValue::Debug(s) => write!(f, "{:?}", s),
+            }
+        }
+    }
+
+    /// Trait for types that can be traced with type context.
+    pub trait Traceable<Q>
+    where
+        Q: ExternalQueries,
+    {
+        fn trace(self, state: &mut CheckState, context: &CheckContext<Q>) -> TraceValue;
+    }
+
+    impl<Q> Traceable<Q> for TypeId
+    where
+        Q: ExternalQueries,
+    {
+        fn trace(self, state: &mut CheckState, context: &CheckContext<Q>) -> TraceValue {
+            TraceValue::Pretty(render(state, context, self))
+        }
+    }
+
+    impl<Q> Traceable<Q> for Option<TypeId>
+    where
+        Q: ExternalQueries,
+    {
+        fn trace(self, state: &mut CheckState, context: &CheckContext<Q>) -> TraceValue {
+            if let Some(value) = self {
+                value.trace(state, context)
+            } else {
+                TraceValue::Debug("None".to_string())
+            }
+        }
+    }
+
+    /// Wrapper for tracing arbitrary `Debug` types.
+    pub struct TraceDebug<T>(pub T);
+
+    impl<T, Q> Traceable<Q> for TraceDebug<T>
+    where
+        T: fmt::Debug,
+        Q: ExternalQueries,
+    {
+        fn trace(self, _state: &mut CheckState, _context: &CheckContext<Q>) -> TraceValue {
+            TraceValue::Debug(format!("{:?}", self.0))
+        }
+    }
+
+    /// Renders a type for tracing, normalising through unification chains.
+    #[inline]
+    pub fn render<Q>(
+        state: &mut CheckState,
+        context: &CheckContext<Q>,
+        type_id: TypeId,
+    ) -> TypeTrace
+    where
+        Q: ExternalQueries,
+    {
+        let normalised = state.normalize_type(type_id);
+        TypeTrace(print_local(state, context, normalised))
+    }
+}
+
+#[cfg(not(feature = "no-tracing"))]
+pub use enabled::*;
+
+/// Core macro for emitting type fields at a configurable tracing level.
+///
+/// Supports both pretty-printed types and debug-formatted values:
+/// - `name = expr` - pretty-prints TypeId values via Traceable
+/// - `?name = expr` - debug-formats arbitrary values via Dbg wrapper
+///
+/// # Examples
+///
+/// ```ignore
+/// // Pretty-print TypeIds
+/// trace_fields!(state, context, { t1 = t1, t2 = t2 });
+///
+/// // Debug-format primitives with ? prefix
+/// trace_fields!(state, context, { ?count = count });
+///
+/// // Mix both with a message
+/// trace_fields!(state, context, { t1 = t1, ?level = level }, "solving");
+/// ```
+#[cfg(not(feature = "no-tracing"))]
+#[macro_export]
+macro_rules! type_fields {
+    // Entry point: fields only
+    ($level:expr, $state:expr, $context:expr, { $($fields:tt)* }) => {
+        $crate::type_fields!(@impl $level, $state, $context, [] { $($fields)* })
+    };
+    // Entry point: fields + message
+    ($level:expr, $state:expr, $context:expr, { $($fields:tt)* }, $($msg:tt)+) => {
+        $crate::type_fields!(@impl_msg $level, $state, $context, [] { $($fields)* }, $($msg)+)
+    };
+
+    // === No-message variant ===
+
+    // Done processing fields
+    (@impl $level:expr, $state:expr, $context:expr, [$(($name:ident, $bind:expr))*] { $(,)? }) => {
+        if ::tracing::enabled!($level) {
+            $(let $name = $bind;)*
+            if let Some((offset_start, offset_end)) = $crate::trace::current_offset(&$state.check_steps, $context) {
+                ::tracing::event!($level, offset_start, offset_end, $($name = %$name),*);
+            } else {
+                ::tracing::event!($level, $($name = %$name),*);
+            }
+        }
+    };
+
+    // Match ?name = expr,
+    (@impl $level:expr, $state:expr, $context:expr, [$($acc:tt)*] { ? $name:ident = $value:expr, $($rest:tt)* }) => {
+        $crate::type_fields!(@impl $level, $state, $context, [$($acc)* ($name, $crate::trace::Traceable::trace($crate::trace::TraceDebug($value), $state, $context))] { $($rest)* })
+    };
+
+    // Match ?name = expr (last, no comma)
+    (@impl $level:expr, $state:expr, $context:expr, [$($acc:tt)*] { ? $name:ident = $value:expr }) => {
+        $crate::type_fields!(@impl $level, $state, $context, [$($acc)* ($name, $crate::trace::Traceable::trace($crate::trace::TraceDebug($value), $state, $context))] { })
+    };
+
+    // Match name = expr,
+    (@impl $level:expr, $state:expr, $context:expr, [$($acc:tt)*] { $name:ident = $value:expr, $($rest:tt)* }) => {
+        $crate::type_fields!(@impl $level, $state, $context, [$($acc)* ($name, $crate::trace::Traceable::trace($value, $state, $context))] { $($rest)* })
+    };
+
+    // Match name = expr (last, no comma)
+    (@impl $level:expr, $state:expr, $context:expr, [$($acc:tt)*] { $name:ident = $value:expr }) => {
+        $crate::type_fields!(@impl $level, $state, $context, [$($acc)* ($name, $crate::trace::Traceable::trace($value, $state, $context))] { })
+    };
+
+    // === Message variant ===
+
+    // Done processing fields
+    (@impl_msg $level:expr, $state:expr, $context:expr, [$(($name:ident, $bind:expr))*] { $(,)? }, $($msg:tt)+) => {
+        if ::tracing::enabled!($level) {
+            $(let $name = $bind;)*
+            if let Some((offset_start, offset_end)) = $crate::trace::current_offset(&$state.check_steps, $context) {
+                ::tracing::event!($level, offset_start, offset_end, $($name = %$name,)* $($msg)+);
+            } else {
+                ::tracing::event!($level, $($name = %$name,)* $($msg)+);
+            }
+        }
+    };
+
+    // Match ?name = expr,
+    (@impl_msg $level:expr, $state:expr, $context:expr, [$($acc:tt)*] { ? $name:ident = $value:expr, $($rest:tt)* }, $($msg:tt)+) => {
+        $crate::type_fields!(@impl_msg $level, $state, $context, [$($acc)* ($name, $crate::trace::Traceable::trace($crate::trace::TraceDebug($value), $state, $context))] { $($rest)* }, $($msg)+)
+    };
+
+    // Match ?name = expr (last, no comma)
+    (@impl_msg $level:expr, $state:expr, $context:expr, [$($acc:tt)*] { ? $name:ident = $value:expr }, $($msg:tt)+) => {
+        $crate::type_fields!(@impl_msg $level, $state, $context, [$($acc)* ($name, $crate::trace::Traceable::trace($crate::trace::TraceDebug($value), $state, $context))] { }, $($msg)+)
+    };
+
+    // Match name = expr,
+    (@impl_msg $level:expr, $state:expr, $context:expr, [$($acc:tt)*] { $name:ident = $value:expr, $($rest:tt)* }, $($msg:tt)+) => {
+        $crate::type_fields!(@impl_msg $level, $state, $context, [$($acc)* ($name, $crate::trace::Traceable::trace($value, $state, $context))] { $($rest)* }, $($msg)+)
+    };
+
+    // Match name = expr (last, no comma)
+    (@impl_msg $level:expr, $state:expr, $context:expr, [$($acc:tt)*] { $name:ident = $value:expr }, $($msg:tt)+) => {
+        $crate::type_fields!(@impl_msg $level, $state, $context, [$($acc)* ($name, $crate::trace::Traceable::trace($value, $state, $context))] { }, $($msg)+)
+    };
+}
+
+#[cfg(feature = "no-tracing")]
+#[macro_export]
+macro_rules! type_fields {
+    ($($tt:tt)*) => {};
+}
+
+/// Emits an INFO-level event with type fields.
+#[macro_export]
+macro_rules! info_fields {
+    ($($args:tt)*) => {
+        $crate::type_fields!(::tracing::Level::INFO, $($args)*)
+    };
+}
+
+/// Emits a DEBUG-level event with type fields.
+#[macro_export]
+macro_rules! debug_fields {
+    ($($args:tt)*) => {
+        $crate::type_fields!(::tracing::Level::DEBUG, $($args)*)
+    };
+}
+
+/// Emits a TRACE-level event with type fields.
+#[macro_export]
+macro_rules! trace_fields {
+    ($($args:tt)*) => {
+        $crate::type_fields!(::tracing::Level::TRACE, $($args)*)
+    };
+}
+
+/// Creates an info-level span for module checking.
+#[cfg(not(feature = "no-tracing"))]
+#[inline]
+pub fn check_module(
+    queries: &impl ExternalQueries,
+    file_id: files::FileId,
+) -> QueryResult<tracing::span::EnteredSpan> {
+    const UNKNOWN: smol_str::SmolStr = smol_str::SmolStr::new_static("<Unknown>");
+
+    let (parsed, _) = queries.parsed(file_id)?;
+    let module_name = parsed.module_name();
+    let module_name = module_name.unwrap_or(UNKNOWN);
+
+    Ok(tracing::info_span!("check_module", ?file_id, %module_name).entered())
+}
+
+#[cfg(feature = "no-tracing")]
+#[inline]
+pub fn module_span(_queries: &impl ExternalQueries, _file_id: files::FileId) -> QueryResult<()> {
+    Ok(())
+}
diff --git a/compiler-scripts/src/bin/test-checking.rs b/compiler-scripts/src/bin/test-checking.rs
index 818b8c8e..ab4ec034 100644
--- a/compiler-scripts/src/bin/test-checking.rs
+++ b/compiler-scripts/src/bin/test-checking.rs
@@ -1,6 +1,7 @@
-use std::path::Path;
+use std::collections::HashMap;
+use std::path::{Path, PathBuf};
 use std::process::{Command, Stdio};
-use std::time::Instant;
+use std::time::{Duration, Instant};
 use std::{env, fs};
 
 use clap::Parser;
@@ -9,6 +10,8 @@ use compiler_scripts::fixtures::fixture_env;
 use compiler_scripts::snapshots::{print_diff, strip_frontmatter};
 use serde::Deserialize;
 
+const TRACE_DIR: &str = "target/compiler-tracing";
+
 #[derive(Deserialize)]
 struct PendingSnapshot {
     path: String,
@@ -16,7 +19,7 @@ struct PendingSnapshot {
 
 #[derive(Parser)]
 #[command(about = "Run type checker integration tests with snapshot diffing")]
-struct Args {
+struct Config {
     /// Test name or number filters
     #[arg(num_args = 0..)]
     filters: Vec<String>,
@@ -24,73 +27,144 @@ struct Args {
     /// Verbose output (show test progress)
     #[arg(short, long)]
     verbose: bool,
+
+    /// Enable tracing output for debugging
+    #[arg(long)]
+    debug: bool,
 }
 
 fn main() {
-    let args = Args::parse();
-    let verbose = args.verbose;
-    let filters = args.filters;
+    let config = Config::parse();
+
+    let (fixture_hashes, hash_duration) = hash_fixtures();
+    println!("{}", style(format!("Hashed fixtures in {}ms", hash_duration.as_millis())).dim());
+
+    run_tests(&config, &fixture_hashes);
 
-    // Hash fixtures and print timing
+    let trace_paths = collect_trace_paths(&config);
+    process_pending_snapshots(&config, &trace_paths);
+}
+
+fn hash_fixtures() -> (HashMap<String, String>, Duration) {
     let start = Instant::now();
-    let fixture_hashes = fixture_env();
-    println!("{}", style(format!("Hashed fixtures in {}ms", start.elapsed().as_millis())).dim());
+    let hashes = fixture_env();
+    (hashes, start.elapsed())
+}
 
-    // Build cargo nextest command
+fn build_nextest_command(config: &Config, fixture_hashes: &HashMap<String, String>) -> Command {
     let mut cmd = Command::new("cargo");
     cmd.arg("nextest").arg("run").arg("-p").arg("tests-integration").arg("--test").arg("checking");
 
-    for filter in &filters {
+    if config.debug {
+        cmd.env("TRACE_LEVEL", "debug");
+    }
+
+    for filter in &config.filters {
         cmd.arg(filter);
     }
 
-    if verbose {
+    if config.verbose {
         cmd.arg("--status-level=fail");
         cmd.arg("--color=always");
     } else {
         cmd.arg("--status-level=none");
     }
 
-    // Set environment variables
     cmd.env("INSTA_FORCE_PASS", "1");
-    for (key, value) in &fixture_hashes {
+    for (key, value) in fixture_hashes {
         cmd.env(key, value);
     }
 
-    // Run tests
-    let _status = if verbose {
-        cmd.status().expect("Failed to run cargo nextest")
+    cmd
+}
+
+fn run_tests(config: &Config, fixture_hashes: &HashMap<String, String>) {
+    let mut cmd = build_nextest_command(config, fixture_hashes);
+
+    if config.verbose {
+        cmd.status().expect("Failed to run cargo nextest");
     } else {
-        // Capture output in quiet mode
         cmd.stdout(Stdio::null()).stderr(Stdio::null());
         let status = cmd.status().expect("Failed to run cargo nextest");
 
         if !status.success() {
-            // Re-run verbose to show errors
             eprintln!("{}", style("Tests failed, re-running verbose...").yellow());
-            let mut retry = Command::new("cargo");
-            retry
-                .arg("nextest")
-                .arg("run")
-                .arg("-p")
-                .arg("tests-integration")
-                .arg("--test")
-                .arg("checking");
-            for filter in &filters {
-                retry.arg(filter);
-            }
-            retry.arg("--status-level=fail");
-            retry.arg("--color=always");
-            retry.env("INSTA_FORCE_PASS", "1");
-            for (key, value) in &fixture_hashes {
-                retry.env(key, value);
-            }
+
+            let verbose_config =
+                Config { filters: config.filters.clone(), verbose: true, debug: config.debug };
+            let mut retry = build_nextest_command(&verbose_config, fixture_hashes);
             let _ = retry.status();
         }
-        status
+    }
+}
+
+fn collect_trace_paths(config: &Config) -> Vec<PathBuf> {
+    if !config.debug {
+        return Vec::new();
+    }
+
+    let trace_dir = PathBuf::from(TRACE_DIR);
+    if !trace_dir.exists() {
+        return Vec::new();
+    }
+
+    let Ok(entries) = fs::read_dir(&trace_dir) else {
+        return Vec::new();
     };
 
-    // Get pending snapshots (suppress stderr)
+    let mut entries: Vec<_> = entries.filter_map(|e| e.ok()).collect();
+    entries.sort_by_key(|e| e.path());
+
+    let mut trace_paths = Vec::new();
+    for entry in entries {
+        let path = entry.path();
+        if path.extension().is_some_and(|ext| ext == "jsonl") {
+            let file_name = path.file_name().unwrap_or_default().to_string_lossy();
+
+            // Skip traces that don't match any filter
+            if !config.filters.is_empty() && !config.filters.iter().any(|f| file_name.contains(f)) {
+                continue;
+            }
+
+            trace_paths.push(path);
+        }
+    }
+
+    trace_paths
+}
+
+/// Finds a trace file that matches the given snapshot path.
+///
+/// Snapshot paths look like: `.../fixtures/checking/200_int_compare_transitive/Main.snap`
+/// Trace files look like: `200_int_compare_transitive_Main.jsonl`
+///
+/// We extract the test identifier (e.g., `200_int_compare_transitive`) from the snapshot's
+/// parent directory and the module name from the file, then find a matching trace file.
+fn find_trace_for_snapshot(snap_path: &str, trace_paths: &[PathBuf]) -> Option<PathBuf> {
+    let path = Path::new(snap_path);
+
+    // Get module name from file (e.g., "Main" from "Main.snap")
+    let module_name = path.file_stem()?.to_str()?;
+
+    // Get test identifier from parent directory (e.g., "200_int_compare_transitive")
+    let test_id = path.parent()?.file_name()?.to_str()?;
+
+    // Trace files are named: {test_id}_{module_name}.jsonl
+    let expected_trace_name = format!("{}_{}.jsonl", test_id, module_name);
+
+    // Find matching trace file
+    trace_paths
+        .iter()
+        .find(|trace_path| {
+            trace_path
+                .file_name()
+                .and_then(|name| name.to_str())
+                .is_some_and(|name| name == expected_trace_name)
+        })
+        .cloned()
+}
+
+fn process_pending_snapshots(config: &Config, trace_paths: &[PathBuf]) {
     let pending_output = Command::new("cargo")
         .arg("insta")
         .arg("pending-snapshots")
@@ -117,45 +191,70 @@ fn main() {
             continue;
         }
 
-        let snap_path = match serde_json::from_str::<PendingSnapshot>(line) {
-            Ok(snapshot) => snapshot.path,
-            Err(_) => continue,
+        let snapshot_path = if let Ok(snapshot) = serde_json::from_str::<PendingSnapshot>(line) {
+            snapshot.path
+        } else {
+            continue;
         };
 
         // Skip snapshots that don't match any filter
-        if !filters.is_empty() && !filters.iter().any(|f| snap_path.contains(f)) {
+        if !config.filters.is_empty() && !config.filters.iter().any(|f| snapshot_path.contains(f)) {
             continue;
         }
 
-        let short_path = snap_path
+        let short_path = snapshot_path
             .strip_prefix(cwd.to_str().unwrap_or(""))
-            .unwrap_or(&snap_path)
+            .unwrap_or(&snapshot_path)
             .trim_start_matches('/');
 
-        let snap = Path::new(&snap_path);
-        let snap_new = format!("{}.new", snap_path);
+        let snap = Path::new(&snapshot_path);
+        let snap_new = PathBuf::from(format!("{}.new", snapshot_path));
+        let trace_path = find_trace_for_snapshot(&snapshot_path, trace_paths);
 
         if snap.exists() {
-            // Updated snapshot
-            println!("{} {}\n", style("UPDATED").yellow().bold(), style(short_path).cyan());
+            display_snapshot_diff(snap, &snap_new, short_path, trace_path.as_deref());
+        } else {
+            display_new_snapshot(&snap_new, short_path, trace_path.as_deref());
+        }
 
-            let old_content = fs::read_to_string(snap).unwrap_or_default();
-            let new_content = fs::read_to_string(&snap_new).unwrap_or_default();
+        println!();
+    }
+}
 
-            let old_stripped = strip_frontmatter(&old_content);
-            let new_stripped = strip_frontmatter(&new_content);
+fn display_snapshot_diff(
+    snap: &Path,
+    snap_new: &Path,
+    short_path: &str,
+    trace_path: Option<&Path>,
+) {
+    println!("{} {}", style("UPDATED").yellow().bold(), style(short_path).cyan());
 
-            print_diff(old_stripped, new_stripped);
-        } else {
-            // New snapshot
-            println!("{} {}\n", style("CREATED").green().bold(), style(short_path).cyan());
+    if let Some(trace) = trace_path {
+        println!("  {} {}", style("TRACE").magenta().bold(), style(trace.display()).cyan());
+    }
 
-            let new_content = fs::read_to_string(&snap_new).unwrap_or_default();
-            for (i, line) in strip_frontmatter(&new_content).lines().enumerate() {
-                println!("{}  {}", style(format!("{:3}", i + 1)).dim(), line);
-            }
-        }
+    println!();
 
-        println!();
+    let old_content = fs::read_to_string(snap).unwrap_or_default();
+    let new_content = fs::read_to_string(snap_new).unwrap_or_default();
+
+    let old_stripped = strip_frontmatter(&old_content);
+    let new_stripped = strip_frontmatter(&new_content);
+
+    print_diff(old_stripped, new_stripped);
+}
+
+fn display_new_snapshot(snap_new: &Path, short_path: &str, trace_path: Option<&Path>) {
+    println!("{} {}", style("CREATED").green().bold(), style(short_path).cyan());
+
+    if let Some(trace) = trace_path {
+        println!("  {} {}", style("TRACE").magenta().bold(), style(trace.display()).cyan());
+    }
+
+    println!();
+
+    let new_content = fs::read_to_string(snap_new).unwrap_or_default();
+    for (i, line) in strip_frontmatter(&new_content).lines().enumerate() {
+        println!("{}  {}", style(format!("{:3}", i + 1)).dim(), line);
     }
 }
diff --git a/tests-integration/Cargo.toml b/tests-integration/Cargo.toml
index b6ba4b3b..d1fe8d5c 100644
--- a/tests-integration/Cargo.toml
+++ b/tests-integration/Cargo.toml
@@ -8,6 +8,8 @@ build = "build.rs"
 analyzer = { version = "0.1.0", path = "../compiler-lsp/analyzer" }
 async-lsp = "0.2.2"
 checking = { version = "0.1.0", path = "../compiler-core/checking" }
+tracing = "0.1.44"
+tracing-subscriber = { version = "0.3.22", features = ["env-filter", "json"] }
 files = { version = "0.1.0", path = "../compiler-core/files" }
 glob = "0.3.3"
 indexing = { version = "0.1.0", path = "../compiler-core/indexing" }
@@ -28,3 +30,4 @@ itertools = "0.14.0"
 
 [dev-dependencies]
 insta = "1.45.1"
+serde_json = "1.0"
diff --git a/tests-integration/build.rs b/tests-integration/build.rs
index bae8f5ce..036d6871 100644
--- a/tests-integration/build.rs
+++ b/tests-integration/build.rs
@@ -134,7 +134,23 @@ fn run_test(folder: &str, file: &str) {{
     let path = std::path::Path::new("fixtures/checking").join(folder);
     let (engine, _) = tests_integration::load_compiler(&path);
     let Some(id) = engine.module_file(file) else {{ return }};
-    let report = tests_integration::generated::basic::report_checked(&engine, id);
+
+    let level = match std::env::var("TRACE_LEVEL").as_deref() {{
+        Ok("debug") => tracing::Level::DEBUG,
+        _ => tracing::Level::WARN,
+    }};
+
+    let target_dir = env!("CARGO_TARGET_TMPDIR");
+    let test_name = format!("{{}}_{{}}",  folder, file);
+    let (report, trace_path) = tests_integration::trace::with_file_trace(
+        level,
+        target_dir,
+        &test_name,
+        || tests_integration::generated::basic::report_checked(&engine, id)
+    );
+
+    println!("trace: {{}}", trace_path.display());
+
     let mut settings = insta::Settings::clone_current();
     settings.set_snapshot_path(std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("fixtures/checking").join(folder));
     settings.set_prepend_module_to_snapshot(false);
diff --git a/tests-integration/fixtures/checking/102_builtin_row/Main.snap b/tests-integration/fixtures/checking/102_builtin_row/Main.snap
index 196bd1b9..6ba87762 100644
--- a/tests-integration/fixtures/checking/102_builtin_row/Main.snap
+++ b/tests-integration/fixtures/checking/102_builtin_row/Main.snap
@@ -91,8 +91,8 @@ solveCons ::
   }
 solveLacks ::
   forall (t160 :: Type) (t161 :: (t160 :: Type)) (t164 :: Type) (t166 :: (t164 :: Type)).
-    { lacksEmpty :: Proxy @(t164 :: Type) (t166 :: ???)
-    , lacksSimple :: Proxy @(t160 :: Type) (t161 :: ???)
+    { lacksEmpty :: Proxy @(t164 :: Type) (t166 :: (t164 :: Type))
+    , lacksSimple :: Proxy @(t160 :: Type) (t161 :: (t160 :: Type))
     }
 solveNub ::
   forall (t175 :: Type).
diff --git a/tests-integration/fixtures/checking/126_instance_phantom/Main.snap b/tests-integration/fixtures/checking/126_instance_phantom/Main.snap
index 671b5468..99151044 100644
--- a/tests-integration/fixtures/checking/126_instance_phantom/Main.snap
+++ b/tests-integration/fixtures/checking/126_instance_phantom/Main.snap
@@ -6,7 +6,7 @@ Terms
 identity :: forall (a :: Type). Phantom (a :: Type) => (a :: Type) -> (a :: Type)
 Proxy :: forall (t1 :: Type) (a :: (t1 :: Type)). Proxy @(t1 :: Type) (a :: (t1 :: Type))
 forceSolve ::
-  forall (t8 :: Type) (t9 :: (t8 :: Type)). { solution :: Proxy @(t8 :: Type) (t9 :: ???) }
+  forall (t8 :: Type) (t9 :: (t8 :: Type)). { solution :: Proxy @(t8 :: Type) (t9 :: (t8 :: Type)) }
 
 Types
 Phantom :: Type -> Constraint
diff --git a/tests-integration/src/lib.rs b/tests-integration/src/lib.rs
index 07a54087..0cb79b63 100644
--- a/tests-integration/src/lib.rs
+++ b/tests-integration/src/lib.rs
@@ -1,4 +1,5 @@
 pub mod generated;
+pub mod trace;
 
 use std::fs;
 use std::path::{Path, PathBuf};
diff --git a/tests-integration/src/trace.rs b/tests-integration/src/trace.rs
new file mode 100644
index 00000000..584fca37
--- /dev/null
+++ b/tests-integration/src/trace.rs
@@ -0,0 +1,62 @@
+//! Tracing capture utilities for tests.
+
+use std::fs;
+use std::io::{BufWriter, Write};
+use std::path::PathBuf;
+use std::sync::{Arc, Mutex};
+
+use tracing::Level;
+use tracing_subscriber::EnvFilter;
+use tracing_subscriber::fmt::MakeWriter;
+use tracing_subscriber::fmt::format::FmtSpan;
+use tracing_subscriber::layer::SubscriberExt;
+
+#[derive(Clone)]
+struct FileWriter(Arc<Mutex<BufWriter<fs::File>>>);
+
+impl Write for FileWriter {
+    fn write(&mut self, buf: &[u8]) -> std::io::Result<usize> {
+        self.0.lock().unwrap().write(buf)
+    }
+    fn flush(&mut self) -> std::io::Result<()> {
+        self.0.lock().unwrap().flush()
+    }
+}
+
+impl<'a> MakeWriter<'a> for FileWriter {
+    type Writer = Self;
+    fn make_writer(&'a self) -> Self::Writer {
+        self.clone()
+    }
+}
+
+/// Writes trace output to a file at the given level.
+/// Pass `env!("CARGO_TARGET_TMPDIR")` from test code as `target`.
+pub fn with_file_trace<F, T>(level: Level, target: &str, test_name: &str, f: F) -> (T, PathBuf)
+where
+    F: FnOnce() -> T,
+{
+    let directory =
+        PathBuf::from(target).parent().expect("no parent directory").join("compiler-tracing");
+
+    fs::create_dir_all(&directory).expect("failed to create trace directory");
+
+    let log_file = directory.join(format!("{}.jsonl", test_name));
+    let log_handle = fs::File::create(&log_file).expect("failed to create trace file");
+    let file_writer = FileWriter(Arc::new(Mutex::new(BufWriter::new(log_handle))));
+    let file_writer_ref = file_writer.clone();
+
+    let formatter = tracing_subscriber::fmt::layer()
+        .with_writer(file_writer_ref)
+        .with_span_events(FmtSpan::CLOSE)
+        .json();
+
+    let subscriber = tracing_subscriber::registry()
+        .with(formatter)
+        .with(EnvFilter::default().add_directive(level.into()));
+
+    let result = tracing::subscriber::with_default(subscriber, f);
+    file_writer.0.lock().unwrap().flush().expect("failed to flush trace file");
+
+    (result, log_file)
+}
diff --git a/tests-integration/tests/checking/generated.rs b/tests-integration/tests/checking/generated.rs
index 02b02886..7eb29d87 100644
--- a/tests-integration/tests/checking/generated.rs
+++ b/tests-integration/tests/checking/generated.rs
@@ -5,7 +5,23 @@ fn run_test(folder: &str, file: &str) {
     let path = std::path::Path::new("fixtures/checking").join(folder);
     let (engine, _) = tests_integration::load_compiler(&path);
     let Some(id) = engine.module_file(file) else { return };
-    let report = tests_integration::generated::basic::report_checked(&engine, id);
+
+    let level = match std::env::var("TRACE_LEVEL").as_deref() {
+        Ok("debug") => tracing::Level::DEBUG,
+        _ => tracing::Level::WARN,
+    };
+
+    let target_dir = env!("CARGO_TARGET_TMPDIR");
+    let test_name = format!("{}_{}",  folder, file);
+    let (report, trace_path) = tests_integration::trace::with_file_trace(
+        level,
+        target_dir,
+        &test_name,
+        || tests_integration::generated::basic::report_checked(&engine, id)
+    );
+
+    println!("trace: {}", trace_path.display());
+
     let mut settings = insta::Settings::clone_current();
     settings.set_snapshot_path(std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("fixtures/checking").join(folder));
     settings.set_prepend_module_to_snapshot(false);
diff --git a/tests-integration/tests/snapshots/checking__quantify_multiple_scoped.snap b/tests-integration/tests/snapshots/checking__quantify_multiple_scoped.snap
index eb7418f9..a02a268d 100644
--- a/tests-integration/tests/snapshots/checking__quantify_multiple_scoped.snap
+++ b/tests-integration/tests/snapshots/checking__quantify_multiple_scoped.snap
@@ -2,6 +2,6 @@
 source: tests-integration/tests/checking.rs
 expression: snapshot
 ---
-forall (t0 :: Type) (t1 :: (t0 :: Type)) (t2 :: (t1 :: ?0[:0])) (t3 :: Type) (t4 :: (t3 :: Type))
-  (t5 :: (t4 :: ?3[:0])).
-  (t2 :: ?1[:0]) -> (t5 :: ?4[:0])
+forall (t0 :: Type) (t1 :: (t0 :: Type)) (t2 :: (t1 :: (t0 :: Type))) (t3 :: Type)
+  (t4 :: (t3 :: Type)) (t5 :: (t4 :: (t3 :: Type))).
+  (t2 :: (t1 :: (t0 :: Type))) -> (t5 :: (t4 :: (t3 :: Type)))
diff --git a/tests-integration/tests/snapshots/checking__quantify_polykind.snap b/tests-integration/tests/snapshots/checking__quantify_polykind.snap
index 1cf0f21c..a301cdd5 100644
--- a/tests-integration/tests/snapshots/checking__quantify_polykind.snap
+++ b/tests-integration/tests/snapshots/checking__quantify_polykind.snap
@@ -2,4 +2,4 @@
 source: tests-integration/tests/checking.rs
 expression: snapshot
 ---
-forall (t0 :: Type) (t1 :: (t0 :: Type)). (t1 :: ?0[:0])
+forall (t0 :: Type) (t1 :: (t0 :: Type)). (t1 :: (t0 :: Type))
diff --git a/tests-integration/tests/snapshots/checking__quantify_scoped.snap b/tests-integration/tests/snapshots/checking__quantify_scoped.snap
index 402d795d..a57a1e40 100644
--- a/tests-integration/tests/snapshots/checking__quantify_scoped.snap
+++ b/tests-integration/tests/snapshots/checking__quantify_scoped.snap
@@ -2,4 +2,4 @@
 source: tests-integration/tests/checking.rs
 expression: snapshot
 ---
-forall (t0 :: Type) (t1 :: (t0 :: Type)) (t2 :: (t1 :: ?0[:0])). (t2 :: ?1[:0])
+forall (t0 :: Type) (t1 :: (t0 :: Type)) (t2 :: (t1 :: (t0 :: Type))). (t2 :: (t1 :: (t0 :: Type)))