It's not that simple, right? Because the computation can actually rely on the types, so the types can't always just be erased. The complexity around knowing when the types are going to be erased or not is part of what motivated Idris 2's adoption of quantities.
https://idris2.readthedocs.io/en/latest/updates/updates.html...