Rework match type handling of invariant types

[OlivierBlanvillain]

Currently we use !isSameType to conclude that two invariant types are disjoint, but as Guillaume pointed out that's incorrect. This should be reworked into a new def provablyNotEqual method in the same style than provablyDisjoint.