Richard Eisenberg
I had another thought on my drive home: why do we need to sort out Constraint v Type for 8.2? I have the patch, and it's essentially all set. But it weakens equality in a way that's troublesome for D2038 and introduces heterogeneous axioms, which are strange, ill-understood beasts. And I don't think we need it.
On the other hand, D2038 is essential for the new Typeable, because it's the only way we can give (->) a proper kind.
Snipped well-considered plan for proceeding.
This route seems, to me, far preferable to monkeying around with roles and such in ways that we have no assurances are sound. (Remember, roles are there to keep the type system safe and sound. They were not added simply to annoy everyone, though they accomplish that goal quite nicely.)
:)
What do we think? It's not ideal, but I think it's the best of suboptimal alternatives. And it's no worse than 8.0 w.r.t. Constraint v Type.
This sounds quite reasonable to me. I will need to fix up the remaining issues in D2038 surrounding Constraint, but I think this shouldn't be so difficult. The only reason I haven't tried already was my belief that Constraint/Type would be resolved soon. I'll try to push another version of D2038 tonight. Cheers, - Ben