Yes, current specialization is unsoundly strong, and needs to be replaced with something weaker. However, rather than the blanket impl you can always do it soundly for a long list of types instead using options like const TypeId (though that is also still unstable I think). One can, though with even more boilerplate, keep it extendable I believe, by adding additional throwaway types to each time you need to use the pattern. Or one can simply reconstruct the entire thing but only impl it for your specific types which it is sound for.
The ergonomics of doing it without specialization are even more atrocious though, and it seemed like such an ergonomics atrocity already so I left it with using specialization.
Which leaves the question: How sanctioned should this be?
Some cases seem like they should obviously work, to the point that perhaps it is a bug that they don't, like the Sized bound issue.
Stating pure mathematical laws like associativity of addition (in the correct type) is, in full generality, beyond the compiler to automate, and so can't be written off in the same way. Still, having to have (A + B) + C = X + Y and A + (B + C) = X + Y both as where clauses seems absurd.
Both of these are I think completely sound, as I believe neither Sized nor const can itself soundly rely on anything erased.
Then we get into more extreme options: specialization on this (or other things). Should code detect if a const argument is a power of two and use a better algorithm that requires such things in that case? Still sound.
Right now we always have stable access to TypeId (though last I saw that itself might have had some soundness holes as well?). This means parametricity is out the window, unless we add things like Pre-RFC: A top of the opt out hierarchy and parametricity, and even then it seems very unlikely it will be made the default.
A sound "best guess" version of try_debug_proof remains on the table, and we already have things like core::mem::needs_drop as precedent for such. But needs_drop is meant to be purely an optimization hint, and can't meaningfully return a useful value anyway since there isn't anything to reasonably do with a drop type specifically.
So how far down this slide should the language go? Which patterns 'deserve' support? TypeId seems to have been decided to be one that deserves support, and when it has a soundness bug it is tracked as a bug to be fixed. I expect plenty of uses exist for debug_with_fallback, especially if combined with a derive macro (or adding it to debug itself if it is so blessed) so that outputs like Some({NO DEBUG}) can be generated. The strict requirement of Debug on Result::expect could be changed, but should it?
I myself feel like the reverse trait implications (such as Sized, though it would also apply to things with other where clauses), the math is less clear but still overwhelmingly the right answer, and beyond that things start to get dubious.