merge: Fix #1243, improve suppress (#1248)

Fix #1243

base/src/main/java/org/aya/tyck/StmtTycker.java

@@ -62,17 +62,22 @@ public void suppress(@NotNull Decl decl) {
     decl.suppresses.forEach(suppress -> {
       switch (suppress) {
         case MostGeneralSolution -> reporter.suppress(MetaVarError.DidSomethingBad.class);
+        case UnimportedCon -> reporter.suppress(PatternProblem.UnimportedConName.class);
+        case UnreachableClause -> {
+          reporter.suppress(ClausesProblem.FMDomination.class);
+          reporter.suppress(ClausesProblem.Domination.class);
+        }
       }
     });
   }
   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;
@@ -136,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) {
@@ -176,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) {

base/src/main/java/org/aya/tyck/error/PatternProblem.java

@@ -2,13 +2,15 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.error;
 
+import kala.collection.mutable.MutableList;
 import org.aya.prettier.BasePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.call.ConCall;
 import org.aya.syntax.core.term.call.DataCall;
+import org.aya.tyck.tycker.Stateful;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
 import org.aya.util.prettier.PrettierOptions;
@@ -80,15 +82,21 @@ record UnknownCon(@Override @NotNull WithPos<Pattern> pattern) implements Patter
 
   record TupleNonSig(
     @Override @NotNull WithPos<Pattern> pattern,
-    @NotNull Term type
+    @NotNull Stateful stateful, @NotNull Term type
   ) implements PatternProblem {
     @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
-      return Doc.vcat(
+      var typeDoc = type.toDoc(options);
+      var lines = MutableList.of(
         Doc.english("The tuple pattern"),
         Doc.par(1, pattern.data().toDoc(options)),
-        Doc.english("splits only on sigma types, while the actual type"),
-        Doc.par(1, type.toDoc(options)),
-        Doc.english("does not look like one"));
+        Doc.english("splits only on sigma types, while the actual type is not:"),
+        Doc.par(1, typeDoc));
+      var normalizedDoc = stateful.fullNormalize(type).toDoc(options);
+      if (!typeDoc.equals(normalizedDoc)) {
+        lines.append(Doc.english("Normalized:"));
+        lines.append(Doc.par(1, normalizedDoc));
+      }
+      return Doc.vcat(lines);
     }
   }
 
@@ -126,6 +134,21 @@ record ImplicitDisallowed(@Override @NotNull WithPos<Pattern> pattern) implement
     }
   }
 
+  record UnimportedConName(
+    @Override @NotNull WithPos<Pattern.Bind> pattern
+  ) implements PatternProblem {
+    @Override public @NotNull Severity level() { return Severity.WARN; }
+
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.vcat(
+        Doc.english("You wrote the following pattern:"),
+        Doc.par(1, Doc.plain(pattern.data().bind().name())),
+        Doc.english("It sounds like you are trying to match with a constructor that is not in scope, " +
+          "so it will be treated as a variable pattern.")
+      );
+    }
+  }
+
   record TooManyImplicitPattern(
     @Override @NotNull WithPos<Pattern> pattern,
     @NotNull Param param

base/src/main/java/org/aya/tyck/pat/PatternTycker.java

@@ -13,11 +13,12 @@
 import org.aya.generic.term.DTKind;
 import org.aya.normalize.Normalizer;
 import org.aya.syntax.compile.JitCon;
+import org.aya.syntax.compile.JitData;
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
+import org.aya.syntax.concrete.stmt.decl.DataDecl;
 import org.aya.syntax.core.Jdg;
-import org.aya.syntax.core.def.ConDef;
-import org.aya.syntax.core.def.ConDefLike;
+import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.pat.Pat;
 import org.aya.syntax.core.pat.PatMatcher;
 import org.aya.syntax.core.pat.PatToTerm;
@@ -127,7 +128,7 @@ public record TyckResult(
       case Pattern.Tuple(var l, var r) -> {
         if (!(exprTycker.whnf(type) instanceof DepTypeTerm(var kind, var lT, var rT) && kind == DTKind.Sigma)) {
           var frozen = freezeHoles(type);
-          yield withError(new PatternProblem.TupleNonSig(pattern, frozen), frozen);
+          yield withError(new PatternProblem.TupleNonSig(pattern, this, frozen), frozen);
         }
         var lhs = doTyck(l, lT);
         yield new Pat.Tuple(lhs, doTyck(r, rT.apply(PatToTerm.visit(lhs))));
@@ -147,9 +148,22 @@ public record TyckResult(
         var typeRecog = state().shapeFactory.find(conCore.dataRef()).getOrNull();
         yield new Pat.Con(conCore, patterns, realCon.conHead);
       }
-      case Pattern.Bind(var bind, var tyRef) -> {
+      case Pattern.Bind bindPat -> {
+        var bind = bindPat.bind();
+        var tyRef = bindPat.type();
+
         exprTycker.localCtx().put(bind, type);
         tyRef.set(type);
+
+        // report after tyRef.set, the error message requires it
+        if (whnf(type) instanceof DataCall call) {
+          var unimportedCon = collectConNames(call.ref())
+            .anyMatch(it -> it.equalsIgnoreCase(bind.name()));
+          if (unimportedCon) {
+            fail(new PatternProblem.UnimportedConName(pattern.replace(bindPat)));
+          }
+        }
+
         yield new Pat.Bind(bind, type);
       }
       case Pattern.CalmFace.INSTANCE ->
@@ -465,6 +479,17 @@ private record Selection(
     };
   }
 
+  private static @NotNull SeqView<String> collectConNames(@NotNull DataDefLike call) {
+    return switch (call) {
+      case JitData jitData -> jitData.body().view().map(AnyDef::name);
+      case DataDef.Delegate delegate -> {
+        // the core may be unchecked!
+        var concrete = (DataDecl) delegate.ref.concrete;
+        yield concrete.body.view().map(it -> it.ref.name());
+      }
+    };
+  }
+
   /**
    * Check whether {@param con} is available under {@param type}
    */

cli-impl/src/test/java/org/aya/test/fixtures/PatTyckError.java

@@ -36,6 +36,15 @@ def test (a : Type) : Type
      | unit y => a
     """;
 
+  @Language("Aya") String testTupleOnNonSigma = """
+    def test (a' : Type) : Type
+     | (a, b) => a
+
+    def Alias => Type
+    def test2 (a' : Alias) : Type
+     | (a, b) => a
+    """;
+
   @Language("Aya") String testBadLiteral = """
     open inductive Test | t
     def not-conf Test : Test
@@ -106,4 +115,20 @@ open inductive Wrap (A B : Type)
     def foo (A : Type) A : A elim A
     | _, {a} => a
     """;
+
+  @Language("Aya") String testUnimportedCon = """
+    open import arith::bool using (Bool)
+    
+    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
+    """;
 }

cli-impl/src/test/resources/negative/PatTyckError.txt

@@ -71,6 +71,36 @@ Error: Cannot split on a non-inductive type
 1 error(s), 0 warning(s).
 Let's learn from that.
 
+TupleOnNonSigma:
+In file $FILE:2:3 ->
+
+  1 │   def test (a' : Type) : Type
+  2 │    | (a, b) => a
+    │      ╰────╯
+  3 │   
+
+Error: The tuple pattern
+         (a, b)
+       splits only on sigma types, while the actual type is not:
+         Type 0
+
+In file $FILE:6:3 ->
+
+  4 │   def Alias => Type
+  5 │   def test2 (a' : Alias) : Type
+  6 │    | (a, b) => a
+    │      ╰────╯
+
+Error: The tuple pattern
+         (a, b)
+       splits only on sigma types, while the actual type is not:
+         Alias
+       Normalized:
+         Type 0
+
+2 error(s), 0 warning(s).
+Let's learn from that.
+
 BadLiteral:
 In file $FILE:3:2 ->
 
@@ -270,3 +300,51 @@ Error: Pattern matching with elim is not compatible with implicit patterns.
 1 error(s), 0 warning(s).
 Let's learn from that.
 
+UnimportedCon:
+In file $FILE:4:2 ->
+
+  2 │   
+  3 │   def not (b : Bool) : Bool
+  4 │   | true => Bool::false
+    │     ╰──╯
+
+Warning: You wrote the following pattern:
+           true
+         It sounds like you are trying to match with a constructor that is not 
+         in scope, so it will be treated as a variable pattern.
+
+In file $FILE:5:2 ->
+
+  3 │   def not (b : Bool) : Bool
+  4 │   | true => Bool::false
+  5 │   | false => Bool::true
+    │     ╰───╯
+
+Warning: You wrote the following pattern:
+           false
+         It sounds like you are trying to match with a constructor that is not 
+         in scope, so it will be treated as a variable pattern.
+
+In file $FILE:5:2 ->
+
+  3 │   def not (b : Bool) : Bool
+  4 │   | true => Bool::false
+  5 │   | false => Bool::true
+    │     ╰─────────────────╯
+
+Warning: The 2nd clause is dominated by the other clauses, hence unreachable
+
+In file $FILE:13:2 ->
+
+  11 │   
+  12 │   inductive RealCase (b : Bool)
+  13 │   | true => real_true
+     │     ╰──╯
+
+Warning: You wrote the following pattern:
+           true
+         It sounds like you are trying to match with a constructor that is not 
+         in scope, so it will be treated as a variable pattern.
+
+That looks right!
+

syntax/src/main/java/org/aya/generic/Suppress.java

@@ -4,5 +4,7 @@
 
 public enum Suppress {
   Shadowing,
+  UnimportedCon,
+  UnreachableClause,
   MostGeneralSolution;
 }

tools/src/main/java/org/aya/util/reporter/SuppressingReporter.java

@@ -2,15 +2,15 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.util.reporter;
 
-import kala.collection.mutable.MutableList;
+import kala.collection.mutable.MutableSet;
 import org.jetbrains.annotations.NotNull;
 
 public record SuppressingReporter(
   @NotNull Reporter reporter,
-  @NotNull MutableList<Class<? extends Problem>> suppressed
+  @NotNull MutableSet<Class<? extends Problem>> suppressed
 ) implements Reporter {
   public SuppressingReporter(@NotNull Reporter reporter) {
-    this(reporter, MutableList.create());
+    this(reporter, MutableSet.create());
   }
 
   @Override public void report(@NotNull Problem problem) {
@@ -19,6 +19,8 @@ public SuppressingReporter(@NotNull Reporter reporter) {
   }
 
   public void suppress(@NotNull Class<? extends Problem> problem) {
-    suppressed.append(problem);
+    suppressed.add(problem);
   }
+
+  public void clearSuppress() { suppressed.clear(); }
 }