Matthew Pickering, Rodrigo Mesquita and Adam Gundry
Cross-stage persistence rules are commonly admitted in multi- stage programming languages. These rules codify the assumption that all module and package dependencies are available at all stages. However, in practice, only a small number of dependencies may be needed at each particular stage.
This paper introduces Explicit Level Imports, a mechanism which gives programmers precise control about which dependencies are required at each stage. Imports are annotated with a modifier which brings identifiers into scope at a specific level. This precision means it is straightforward for the compiler to work out what is exactly needed at each stage, and only provide that. The result is faster compilation times and the potential for improved cross-compilation support.
We have implemented these ideas in GHC Haskell, consider a wide variety of practical considerations in the design, and finally demonstrate that the feature solves a real-world issue in a pragmatic way.
Latest version: Explicit Level Imports (PDF) in TFP 2025 post-proceedings (winner of the John McCarthy prize for best paper)