The backends support subtyping for @0 (mainly?) by not removing erased function arguments, and supplying dummy arguments when a function is applied to something erased, right? Is there a reason for not removing the arguments entirely, and supporting subtyping using coercions instead?

I've seen that at least the GHC backend generates wrappers for functions with erased arguments. Is the idea that GHC will optimise away the wrappers whenever possible?