> a function with a panic that lets you write the SortedList -> SortedList

Ah, I think I see what you mean. Yes, that's also possible, but you are losing the full safety of dependent types, and are just back to contracts!