Dependently typed programs often contain a lot of information that is useful only for type checking but useless for execution. Sometimes the amount of such information not only makes the program slower but it also worsens the time/space complexity of the program. However, we should not have to make a program asymptotically slower just by describing it more precisely.

In this talk, I will illustrate how this happens and where traditional approaches to (proof) erasure, such as proof universes or compile-time irrelevance fall short. I will show that by addressing erasure directly, we can remove (much of) this overhead, and I will describe an automatic way of discovering and removing it, while retaining the convenience of fully dependent pattern matching. Finally, I’ll sketch possible ways forward, such as integration with additional modalities/quantities or erasure polymorphism.