for when one expects a list to be non-empty, i think there’s strong argument in favor of an enforcement from the type checker, given that the prove will very likely be necessary. if not in the application code then in the tests.