If I do convince the community at large that it’s feasible, will it have a chance of getting into Scala? I need to know before potentially spending a few days on this.
I’m worried that even if I do convince the community, it will not be picked up, and my efforts will have been in vain.
There’s a SIP process for this. For a fundamental/risky thing like this, I believe the only way to make progress is by intellectual curiosity. Can you come up with a formalization and a soundness proof of what you have in mind? If yes, the best next step would be to write a paper and have it peer reviewed. The original matchtype paper does that (to some degree) so you need to achieve at least parity with that. Once you have something that is sound and has good use cases of expressiveness the next step would be to draft a SIP. It would be a lot of work, so you should feel it’s rewarding even if it would not get in in the end. Be it because it’s actually not sound - but you have learned something interesting, or that it is sound and you have at least advanced the state of the art of what we know about match types.
So I had a look at the paper (Type-Level Programming with Match Types), and came up with an additional subtyping rule for System FM. Here is a draft presenting it.
Is anyone interested in discussing it at this early stage?
P.S.: If this discussion would be better continued in a different format, please let me know.