What is the lead time? There are at least four backends: those targeting GHC (called MAlonzo), UHC, Epic, and JavaScript. Some source data can be found in the Agda wiki : you can read how the Epic backend erases types there or in this (chapter "3.3 Erasure"). In short, Epic and UHC backends erase all types that the fully applied function receives, but do not completely erase, as this can change the semantics of the program (cited from the UHC backend document ):
Type of translation
The remaining members Ξ , Set and Level are important for type checking. In Agda, a value of type Set or Level cannot be verified or matched against a pattern. Because Agda makes it impossible to observe any value of these types, they cannot influence execution semantics. To run a program, it is safe to replace all occurrences of such values ββwith a unit of β€ .
It may also be tempting to completely remove any meanings of these kind. This can potentially change the semantics of the translated program. Agda does not evaluate expressions under lambdas; discarding lambda abstractions that take type expressions can remove the lambda bound lock. Partial erasure of types is possible in a sound way. For example, applications with rich functions can always be optimized in this way. A more detailed description of when such types can be well erased can be found in the previous work of Letozey.