Author of the roles system here. I’m aware of no ideas that will move us forward in this direction. The problem is that we’d need to check a delicate property in order to ensure that the coercion is safe. Specifically, we want to be able to coerce e.g. HList [Age, Int, String]
to HList [Int, Age, String]
but not to HList [String, String, Int]
(or an HList
with something other than three elements). (I’m assuming newtype Age = MkAge Int
here.) Pulling this off would require some Very Glorious role-like system — capable of describing exactly what coercions would be safe for such a GADT — and I don’t know of any work toward creating such a system.
The reason the data family approach works is that GHC can see that HList [Age, Int, String]
is really the same as (Age, (Int, (String, HList '[])))
, and then it knows tuples well enough to do the rest of the work.
Sorry to have no encouragement here, but this seems well beyond what we can do now.