diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index ddbe09e58..6356e2eba 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -71,13 +71,13 @@ public void suppress(@NotNull Decl decl) { }); } public @Nullable TyckDef check(@NotNull Decl predecl) { - suppress(predecl); ExprTycker tycker = null; if (predecl instanceof TeleDecl decl) { if (decl.ref().signature == null) tycker = checkHeader(decl); } - return switch (predecl) { + suppress(predecl); + var core = switch (predecl) { case FnDecl fnDecl -> { var fnRef = fnDecl.ref; assert fnRef.signature != null; @@ -141,6 +141,8 @@ yield switch (fnDecl.body) { yield new DataDef(data.ref, data.body.map(kon -> kon.ref.core)); } }; + reporter.clearSuppress(); + return core; } public ExprTycker checkHeader(@NotNull TeleDecl decl) { @@ -181,6 +183,7 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(), } } } + reporter.clearSuppress(); return tycker; } private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker) { diff --git a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java index f70b650d6..0155a937f 100644 --- a/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java +++ b/cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java @@ -123,6 +123,11 @@ def not (b : Bool) : Bool | true => Bool::false | false => Bool::true + @suppress(UnimportedCon, UnreachableClause) + def don't-care (b : Bool) : Bool + | true => Bool::false + | false => Bool::true + inductive RealCase (b : Bool) | true => real_true """; diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt index b662e1d22..6ca6296e1 100644 --- a/cli-impl/src/test/resources/negative/PatTyckError.txt +++ b/cli-impl/src/test/resources/negative/PatTyckError.txt @@ -334,12 +334,12 @@ In file $FILE:5:2 -> Warning: The 2nd clause is dominated by the other clauses, hence unreachable -In file $FILE:8:2 -> +In file $FILE:13:2 -> - 6 │ - 7 │ inductive RealCase (b : Bool) - 8 │ | true => real_true - │ ╰──╯ + 11 │ + 12 │ inductive RealCase (b : Bool) + 13 │ | true => real_true + │ ╰──╯ Warning: You wrote the following pattern: true diff --git a/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java b/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java index 361bebfa5..ce2dfc65a 100644 --- a/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java +++ b/tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java @@ -21,4 +21,6 @@ public SuppressingReporter(@NotNull Reporter reporter) { public void suppress(@NotNull Class problem) { suppressed.add(problem); } + + public void clearSuppress() { suppressed.clear(); } }