[ryangs]

But the nonempty list never has an element, so we don't need to worry about the type mutation of removing an element from it. Filter just returns a nonempty list.

[jerf]

"But the nonempty list never has an element, so we don't need to worry about the type mutation of removing an element from it."

NonEmpty always has an element.