"But if the compiler can verify that a value is used exactly once, then why can't it verify that a value is destructed? We mark a function as a destructor and the compiler verifies that the value is passed to a destructor exactly once."
Even when you could verify this, it wouldn't prevent use after free bugs.
Agreed. To be clear, I'm not explaining why the OP chose linear types over affine types (I have mixed feelings on choosing one or the other) but rather why one needs either affine or linear types rather than "disposed exactly once" types.
Even when you could verify this, it wouldn't prevent use after free bugs.