Sadly ICFP didn't want this, but maybe you'll find it interesting anyway. https://www.type-driven.org.uk/edwinb/idris-2-quantitative-type-theory-in-action.html … Off I go to the LaTeX mines to make it harder to reject... but not just yet.
It is valuable to be able to say "this argument must not be used". Idris 1 does something a bit like that - erasure inference - and you can accidentally end up with big proof objects in your program.