If it’s been considered already, then I guess there’s no need to pursue it…
But FWIW, I wouldn’t have thought that the performance issue would be significant: Literals are not that common in code; the intersections are not that large (there’s a limit of six types). I would have thought a single implicit search would be orders of magnitude more work. On the other hand, it’s not clear to me yet how widely these intersection types would typically be perpetuated.
The incompleteness of unification sounds like more of a problem, but I’m not sure I’m understanding correctly when it would come into play: these are general problems with unification, but the intersections of AnyVal subtypes arising from literals would be non-overlapping and not parameterized. I suspect I’ve missed the point, somewhere! For the type system to provide useful results, we would probably want to introduce a new arbitrary rule to select certain priorities (as I suggested for overload resolution).
Anyway, given @Jasper-M’s example (which surprised me, actually… I’m not convinced weak-conformance isn’t being applied here, and I actually expected the intersection to collapse under application of an overloaded +), it might be a fun exercise for someone with more time than me to attempt to implement and run some tests against, on the basis that it probably won’t be merged, but could provide interesting evidence about whether it’s a better or worse situation than the status quo. If I had a couple of days free, I’d love to try it myself…