Doubts on the behavior of Unit Type in a type system
The short answer is that isomorphic types are not equal, despite behaving identically, and so the type system can distinguish between them. In a nominal type system, like the one you describe, types are essentially identified by their names, even if they are structurally equivalent. This is the case for the five unit types you describe: they are structurally equivalent, but nominally unequal, and so they are treated as distinct.

Note that the pattern matching aspect is orthogonal: you can think of the five unit types as existing in isolation. In most type theories, you can take the sum of any two types, even two that are (nominally) equal, e.g. Unit + Unit. You will still be required to pattern match, and will have two cases: the left Unit and the right Unit. The nominal aspect is unimportant, although many programming languages will use the names to distinguish between the different cases like this, instead of the indices of the summands (in particular, in languages where you are only allowed to take sums of distinct nominal types, like Standard ML).