Shipping specialization: a story of soundness

Necropost:

I recently read in a random Hacker News comment about "type roles" in Haskell:

...and it occurred to me that the problem the feature was meant to solve is pretty similar to the soundness hole here.

The compiler expects to be able to use the same trait/typeclass implementations for two types based on the assumption that they have identical representations:

  • Haskell: A newtype versus the type it wraps
  • Rust: Types that differ only in lifetime parameters

This works for normal (parametric) generic code, but is broken by the ability to create a type-to-type 'lookup table':

  • Haskell: …using type families (which are just associated types, in Rust terminology, but because Haskell's type system treats newtypes as separate types, there's nothing preventing you from impl'ing something for a newtype and its base type with different associated types)
  • Rust: …using associated types + specialization (specialization is required because the language has only a single concrete lifetime, 'static, so there's no other way to have two separate impls of the same trait for two types differing only in a lifetime parameter)

Haskell's solution is to differentiate between two 'roles' of type parameters: "representational" parameters, which allow coercions but not lookup, and "nominal" parameters, which allow lookup but not coercions. (By "coercions" I mean the features in first set of bullets, and by "lookup" I mean the second set.)

However, @glaebhoerl once wrote, about the roles feature:

The opinion of many leading members of the Haskell community is that this solution was ill-conceived and brings more complexity than it's worth.

And I'm not really sure what an equivalent feature would look like in Rust, anyway.