The example given in the paper is a LinArray (https://github.com/idris-lang/Idris2/blob/main/libs/contrib/...). Unfortunately, as the community discovered, a user can "leak" a non-linear binding outside of the `newArray` constructor (which is what attempts to enforce linearity for all bindings). With multiple unrestricted handles, a user can accidentally double-free for instance. (https://github.com/idris-lang/Idris2/issues/613)
The fundamental issue in this case is that linearity in QTT is a property of the parameter bindings and _not_ the type itself, meaning we can't easily express linearity as a _global_ property of the type.
On the other hand, only affecting the parameter bindings makes it really easy to use runtime-erased/comptime stuff without reimplementing a bunch of common types as runtime- and comptime-only versions.
ATS chooses the other path and makes linearity and runtime-erasure a part of the type (not without paying a hefty syntactic cost however).