I agree that this would be an amazing thing to have, but I've never seen those anywhere in practice (not even in Idris). My gut-feeling tells me that it might not work in combination with composability in the sense that there might never be a proper global "equal" that everyone can agree one.

I'm curious - besides the ones mentioned, are there any other fundamental type concepts that you would build into your own programming language? :)