> abstract types can break merely by having a stronger type system which is able to prove strictly more things (such as whether two types are equal) Indeed, wh

> abstract types can break merely by having a stronger type system which is able to prove strictly more things (such as whether two types are equal) Indeed, which is why I'm not such a huge fan of overly powerful type systems. > That makes implementing completely leak-free abstractions quite difficult. It means the type system has to have the right amount of expressive power. Too little, and separation of concerns becomes difficult. Too much, and separation of concerns becomes difficult too! It also means that we can't rely on types to prove everything we would like to prove about programs. This seems intuitively right, because type systems are first and foremost meant to be mechanically checkable, not to be flexible enough to express every possible software requirement. > In your example, it is not just the existence of the union type that causes the problem, but the operation "is T", which you probably assume to be of type "forall a. (a | T) -> Bool" or something. This is correct. But removing this `is T` operation would greatly reduce the appeal of union types in practice. > you could trivially implement abstract types similar to Haskell's newtype wrapper as { [some private symbol]: implementation-type }. Both Haskell's `newtype` and your proposal are poor replacements for actual abstract types.