I believe the first example in the "Going deeper" section is not a place where type check and trans actually disagree, but a place where they theoretically could disagree depending on how we decide specialization should work and how many layers of indirection are involved.
However, type check could deduce that the more specialized impl always applies when invoking special in pair, and you could imagine communicating that information down to trans.
I think the reason he was bringing this up at all was to demonstrate that the soundness issues described in the rest of the post are not necessarily unique to associated types, and that's why a truly complete solution can't focus purely on associated types but must deal with the type checker vs trans more generally.
As a naive user, I expect specialization to work as follows:
1. Find the most specific specialization without taking lifetime bounds into account.
2. Validate that the lifetime bounds are met, and give a compile error if they aren't.
I basically agree with this. I suspect there might be some legitimate exceptions like having a default impl for &str and a specialization for &'static str, or having a default impl with two unconstrained lifetimes and a specialization for when the lifetimes are the same or one is known to outlive the other. I can't come up with a concrete use case for doing either of those things myself, but I doubt it's safe to assume there aren't any.
My only concern with the proposed subset for stabilization is that the post sounds like it's proposing we stabilize at least some cases where the behavior is expected to require changing in the future, and get away with that via lints and epochs. As much as I want epochs, for a feature like this that's part of the core trait system and has massive ramifications for optimally efficient composability across the ecosystem, I don't like the idea of relying on epochs to "get away" with stabilizing unstable behavior...assuming that's a remotely accurate summary of the proposal. It also wasn't clear to me from the blog post whether there is any alternative in between "stabilize some stuff we'll have to epoch away later" and "never stabilize anything until we have a perfect solution".
Could you go into more detail on why "lifetime specialization" can't be a hard error? The post only mentions in passing that:
(This needs to be a lint, not a hard error, because the relevant impls aren’t always under your crate’s control.)
But I don't see how not owning all the impls means it can't be as hard of an error as, say, the orphan rules.