본문으로 건너뛰기
토파즈6.0 · 출시 전
다운로드 →

문서 검색

명세 6.0

방향키로 결과를 고르고 Enter를 눌러 여세요.

API 이름, 진단 번호, 규칙 또는 프로젝트 주제를 입력하세요.

    진단 TPZ5713

    A match case covered entirely by earlier unguarded cases produces TPZ5713 during checking.

    Diagnostic and cause

    링크

    Unreachable match case

    계열
    topaz
    단계
    check
    코드
    TPZ5713

    원인과 조건

    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.

    대응

    Move general unguarded cases after any specific cases they would shadow. Remove a later case if earlier unguarded patterns already cover all inputs it could match. A guard may fail and does not establish unconditional coverage.

    Topaz 6.0.0 specifies this diagnostic during checking.

    The target message is match case is unreachable because earlier unguarded cases cover its pattern.

    The pinned SELF source does not emit this diagnostic.

    Earlier unguarded cases cover every input that could match this case. The checker reports TPZ5713 at the unreachable pattern. In the example, true and false together cover every bool value before the wildcard case.

    규칙diagnostics.tpz5713.p5.rule

    Earlier cases cover this match case

    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.

    이유

    An exceptional case can intentionally precede a general case. Source order expresses that priority. Rejecting a case already covered by earlier unguarded patterns prevents that order from silently disabling a branch. A guard can fail, so it cannot establish unconditional coverage. This follows the ordered match decision.

    Response

    링크

    Remove the covered case, or place a specific case before a general case that should handle the remaining inputs. If an earlier case is conditional, express that condition with a guard. The corrected program keeps the true case before the wildcard.

    Reproduction and verification

    링크

    Rejected program

    링크
    example.tpzRejected program플레이그라운드 열기 →
    1. function classify(value: bool) -> int {
    2. match (value) {
    3. case true => 1
    4. case false => 0
    5. case _ => 2
    6. }
    7. }
    기대 출력0이 아닌 종료 코드
    표준 출력 없음.
    $ topaz check example.tpz · 대상 제품 5.21.3
    기대 결과

    기대 결과

    거절 단계 check. 종료 코드가 0이 아닙니다.

    The message pattern is the Topaz 6.0 target message. The cited SELF source checks completeness but does not emit TPZ5713. The rejected program exercises the union of two earlier unguarded cases. The corrected program keeps a reachable general case after a specific case.

    Repaired program

    링크
    example.tpzRepaired program
    1. function classify(value: bool) -> int {
    2. match (value) {
    3. case true => 1
    4. case _ => 0
    5. }
    6. }
    기대 출력종료 코드 0
    $ topaz check example.tpz · 대상 제품 5.21.3
    기대 결과

    기대 결과

    검사가 프로그램을 받아들입니다. 종료 코드 0.

    The message pattern is the Topaz 6.0 target message. The cited SELF source checks completeness but does not emit TPZ5713. The rejected program exercises the union of two earlier unguarded cases. The corrected program keeps a reachable general case after a specific case.

    메뉴

    다운로드 →