agda-find-reproducer

name

agda-find-reproducer

description

Reduce a large Agda file to a minimal reproducer for an Agda compiler bug (e.g. `__IMPOSSIBLE__` or any other specific internal error string). Runs an iterative edit → test → commit/revert loop, preserving the invariant that the file still emits the exact target error string at every committed step. Use when the user asks to "minimize this bug", "reduce the reproducer", "make a smaller example of this Agda crash", or mentions a specific Agda internal-error location (file:line) they want a smaller trigger for.

Agda bug reduction

Iteratively shrink an Agda source file until it's a minimal reproducer for a specific compiler bug, without ever losing the bug.

Core invariant

The file under reduction must always emit the target error string. After every edit:

1. Re-typecheck the file.
2. Grep the output for the target error string.
3. If the string is still there → the edit is kept (and usually committed).
4. If it's gone → revert the edit immediately, then try something smaller or different.

This is non-negotiable. Do NOT stack reductions on top of a file that no longer errors.

Distinguish the target trigger from benign type errors

An internal-error trigger looks like:

src/full/Agda/.../File.hs:AAA:BB: __IMPOSSIBLE__

These come from Haskell source lines inside the Agda binary — they are bugs in Agda itself.

Ordinary Agda type errors look like:

<your-file>:82.3-84.39: error: [UnequalTerms]
<your-file>:83.35-39: error: [UnsolvedInteractionMetas]
error: [UnsolvedConstraints]
error: [UnsolvedMetaVariables]

If your reduction replaces the internal-error trigger with one of these "your-file:line" errors, it killed the bug. Revert.

Always match the target by specific string, e.g.:

nix develop --command agda <file> 2>&1 | grep -E "IMPOSSIBLE" | head -5

Not just "is there an error" — that's true for any broken edit.

Workflow

1. Set up a dedicated worktree

Use a git worktree per bug so the reduction is isolated. One bug per branch:

git worktree add .claude/worktrees/<bug-name> <starting-commit>

If the user starts from a specific commit (they often will — they know where the bug first appeared), check it out on a fresh branch. Don't pollute their main branches.

2. Verify the baseline triggers

Before editing anything, confirm the starting state emits the target string:

cd <worktree>  # or wherever agda runs
nix develop --command agda <path/to/file.agda> 2>&1 | grep -E "<target-pattern>" | head -5

If it doesn't trigger, stop and ask the user — something is wrong about the starting commit or the target pattern.

3. Iterate

Loop until you can't reduce further:

1. Back the file up: cp <path/to/file>.agda <path/to/file>.agda.bak
2. Pick a candidate reduction (see strategies below).
3. Edit the file.
4. Re-run the agda grep command.
5. If the target string appears → git add -A && git commit -m "Progress: <what was removed>".
6. If it doesn't → restore the backup (cp <path/to/file>.agda.bak <path/to/file>.agda) and try a different angle.

Don't run cleans or _build/ wipes between iterations. Agda will re-typecheck the edited file; dependency interfaces stay cached and keep the loop fast.

4. When you're stuck

Ask the user. They often have domain knowledge about which fields are load-bearing or which simplifications are safe to try. Report:

• Current line count and most recent commit hash.
• What you've tried and what broke (which reductions produced which non-trigger errors).
• Current file content or relevant section.

Reduction strategies (ordered by cost-benefit)

Start cheap. Always re-test after each step. If a step kills the trigger, revert before trying the next.

Metrics

We want to find the smallest program that reproduces the issue. For the purposes of this document, 'small' does not refer to characteristics of the file, such as line or character count. Rather, it purely relates to the size of the syntax tree and context. Here are some examples:

• f is smaller than f x
• a function with less clauses or with abstractions is smaller
• a record with less fields is smaller than a record with more fields
• a data type with less constructors is smaller
• a postulated function is smaller than a defined one
• a module that defines less things is smaller than one that defines more, even if the individual definitions are larger
• a file that imports less definitions is smaller than one with more definitions

Cheap wins (try first)

• Drop unused definitions, postulates, types, arguments (functions, modules, types), imports, etc. For all imports, maintain a using directive. We consider open import X using (a) to be smaller than open import X, so adding a using directive counts as a reduction step. using is also smaller than hiding. Make sure that the using directive also includes all modules (via open import X using (module M)).
• Replace subterms with postulates or other appropriate smaller terms Always try to reduce the scope of the term. A postulate is better than a constant (e.g. 0), which is better than a variable. Also, if you have multiple different constants of the same type (e.g. ⊤ and ℕ), see if it is possible to substitute one with the other.
• Specialize types E.g. {A : Type} → List A → List A → List ℕ → List ℕ.
• Simplify function bodies with pattern-matching or with Try to simplify the right hand side so that multiple branches of a pattern-match can be defined with the same term. Then eliminate the pattern match.
• Simplify types Try to eliminate constructors from data types and fields from record types.
• Inline simple definitions or modules with a single use site Any more complicated inline may increase complexity.
• Replace named-but-unused parameters with _ module M (n : ℕ) where → module M (_ : ℕ) where if n isn't referenced inside. Same for record params: record F (A : Set) → record F (_ : Set) if A isn't used in fields. In a type signature (a : A) → B, if a does not appear in B simplify to A → B.

Medium (try only if there are no more cheap options)

• Retry cheap reductions Maintain a todo list of reductions that seem like they should work but don't. Sometimes it is possible to do those reductions at a later stage.
• Recursively replacing subterms Sometimes a reduction like f n → 0 does not work, but f n → f 0 or f n → g n (with g a postulate) do. Recursively try all options.
• Reshuffle where parameters live. A record like record R (A B : Set) : Set can sometimes be turned into module M (A : Type) where; record R (B : Type) : Set or vice versa. It is unclear which of these should be considered smaller, but such a change may unlock reductions that weren't possible before.
• Inline an import with only a single used definition If we have an import of the form open import X using (a), copy over the definition of a and all imports from X, then remove all unused imports.

Expensive (try only if the other options stopped working)

• Inline dependencies Look at the imports of the module and make a list of 'standalone imports' - modules X such that no other imports import X (transitively). Out of those, select the one with the smallest using directive. First, try to only copy the parts of the import that are actually used. If this fails, copy the whole import and simplify from there. Make sure to properly account for module parameters.

Environment gotchas

• nix develop working-directory behavior: nix develop --command agda <file> uses the current working directory to find .agda-lib. If you're not in the lib dir, pass the flake path: nix develop <flake-root> --command bash -c "cd <lib-dir>; agda <file>".
• Agda prints warnings about dirty worktrees to stderr. Filter them out with grep -E "<target-pattern>".
• Don't git checkout <commit> -- <file> in a shared branch. Create a new worktree or branch per bug; mixing reductions pollutes history.

Commit message style

Use Progress: <what was removed or simplified> — short, imperative, describes the diff.

Ask the user whether they want a commit on every reduction, before doing an expensive step or no commits. Keep in mind that there is always a backup of the most recent reproducer anyway.