agda-unused: Check for unused code in an Agda project.

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

A tool to check for unused code in an Agda project.

[Skip to Readme]


Versions 0.1.0, 0.2.0, 0.2.0, 0.3.0
Change log
Dependencies aeson (>=1.4.7 && <1.6), Agda (>=2.6.1 && <2.6.2), agda-unused, base (>=4.13 && <4.15), containers (>=0.6.2 && <0.7), directory (>=1.3.6 && <1.4), filepath (>=1.4.2 && <1.5), mtl (>=2.2.2 && <2.3), optparse-applicative (>=0.15.1 && <0.17), text (>=1.2.4 && <1.3) [details]
License MIT
Maintainer Matt Superdock <>
Category Dependent types
Source repo head: git clone
Uploaded by msuperdock at 2021-05-05T02:29:27Z


[Index] [Quick Jump]


Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Readme for agda-unused-0.2.0

[back to package description]


agda-unused checks for unused code in an Agda project, including:

agda-unused takes a filepath representing an Agda code file and checks for unused code in that file and its dependencies. By default, agda-unused does not check public items that could be imported elsewhere. But with the --global flag, agda-unused treats the given file as a description of the public interface of the project, and additionally checks for unused files and unused public items in dependencies. (See below for more on the --global flag.)

Supported Agda versions: >= 2.6.1 && < 2.6.2


File ~/Test.agda:

module Test where

open import Agda.Builtin.Bool
  using (Bool; false; true)
open import Agda.Builtin.Unit

  : Bool
  → Bool
  → Bool
false ∧ x
  = false
_ ∧ y
  = y


$ agda-unused Test.agda


  unused imported item ‘true’
  unused import ‘Agda.Builtin.Unit’
  unused variable ‘x’


agda-unused - check for unused code in an Agda project

Usage: agda-unused FILE [-g|--global] [-j|--json]
  Check for unused code in FILE

Available options:
  -h,--help                Show this help text
  -g,--global              Check project globally
  -j,--json                Format output as JSON
  -i,--include-path DIR    Look for imports in DIR
  -l,--library LIB         Use library LIB
  --library-file FILE      Use FILE instead of the standard libraries file
  --no-libraries           Don't use any library files
  --no-default-libraries   Don't use default libraries


If the --global flag is given, all declarations in the given file must be imports. The set of imported items is treated as the public interface of the project; these items will not be marked unused. The public items in dependencies of the given module may be marked unused, unlike the default behavior. We also check for unused files.

To perform a global check on an Agda project, first create a file that imports exactly the intended public interface of your project. For example:

File All.agda:

module All where

import A
  using (f)
import B
  hiding (g)
import C


$ agda-unused All.agda --global


If the --json flag is given, the output is a JSON object with two fields:

The "none" type indicates that there is no unused code.


We make a single pass through the given Agda module and its dependencies:

This means, for example, if we have three definitions (say f, g, h), each depending on the previous one, where h is not a root, then f and g are considered used, while h is considered unused. If we remove h and run agda-unsed again, it will now report that g is unused. This behavior is different from Haskell's built-in tool, which would report that all three identifiers are unused on the first run.


We work with Agda's concrete syntax. This is a necessary choice, since Agda's abstract syntax doesn't distinguish between qualified and (opened) unqualified names, which would make it impossible to determine whether certain open statements are unused. However, using concrete syntax comes with several drawbacks:

Additionally, we currently do not support the following Agda features:

agda-unused will produce an error if your code uses these language features.