TPZ5713 Unreachable match case

Cases are tried in source order. A case may overlap an earlier case if it can match an input that reaches it. A specific case can therefore precede a general case. An unguarded wildcard or total binding is an ordinary case and acts as a fallback at its written position. There is no separate residual fallback selection.

A later case is unreachable when the union of preceding unguarded patterns covers every value its pattern could match. This includes a case shadowed by a single catch-all or by several earlier cases. Pattern typing runs before this comparison. A guard cannot establish unconditional coverage because it may fail. Overlapping cases with reachable inputs remain valid even when their intersection is unknown.

Alternatives of one or-pattern describe one case domain. Their overlap does not make a later case unreachable. Binding consistency is checked by its separate rule. All case bodies are checked even when their patterns are unreachable.

An unreachable case is rejected during checking with TPZ5713. A typed pattern incompatible with the known scrutinee type still uses TPZ5001. Match completeness follows the exhaustiveness rule.

During checking, TPZ5713 rejects a match case when the union of earlier unguarded patterns covers every value that its pattern can match. The primary location is the start of the unreachable pattern. Pattern typing runs before coverage comparison. A guard on an earlier case never establishes unconditional coverage, even when the guard is constant. A later guarded case is still unreachable when earlier unguarded patterns cover its entire pattern domain. Reachable overlap and a general case after a specific case remain valid. If coverage cannot be proved, the case remains valid under this rule. Alternatives of one or-pattern form one case domain. Their mutual overlap does not trigger this diagnostic. Every case body is type checked. Existing completeness checks remain unchanged. The pattern matching rule defines ordered selection and reachability.