The cons example is conflating implementation details (return the value passed in to cons) with the semantics (return the left-side of this pair that was instan

The cons example is conflating implementation details (return the value passed in to cons) with the semantics (return the left-side of this pair that was instantiated by cons). In the first case it is a category error to think about mutability. In the second mutability makes perfect sense. Moreover, I suspect it is possible to construct an interface such that to prove statically that you can Liskov Substitute a type into it would be equivalent to deciding Halt: All you need are extensional semantics in your type system.