A really good question. In short, a linear List (or array, or hash map, etc) will only have two available destroyer functions:

1. drop_into(list, func): It consumes the list, calling the given `func` for each element.

2. expect_empty(list): Consumes the list, panicking if the list isn't empty.

I bet expect_empty could be defined roughly as:

  fn expect_empty(list) {
      drop_into(list, () => panic());
  }

(pardon my made up syntax)

If you want to discourage runtime checks, you could even make the programmer do the above themselves since it's a one-liner anyway.

I see, so in that second case it’s a runtime check rather that a static check. That makes sense.

Depends on the rest of your type system. If your language is capable of tracking whether a list is empty then it can allow dropping empty lists without a runtime check.