error: write a longer error message

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);
     }
   }
 
@@ -129,18 +137,14 @@ 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 Severity level() { return Severity.WARN; }
 
-    @Override
-    public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.vcat(
-        Doc.english("The binding name:"),
+        Doc.english("You wrote the following pattern:"),
         Doc.par(1, Doc.plain(pattern.data().bind().name())),
-        Doc.english("is equal to an un-imported constructor of:"),
-        Doc.par(1, pattern.data().type().get().toDoc(options))
+        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.")
       );
     }
   }

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

@@ -128,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))));
@@ -158,8 +158,7 @@ public record TyckResult(
         // report after tyRef.set, the error message requires it
         if (whnf(type) instanceof DataCall call) {
           var unimportedCon = collectConNames(call.ref())
-            .anyMatch(it -> it.equals(bind.name()));
-
+            .anyMatch(it -> it.equalsIgnoreCase(bind.name()));
           if (unimportedCon) {
             fail(new PatternProblem.UnimportedConName(pattern.replace(bindPat)));
           }

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

@@ -278,10 +278,10 @@ In file $FILE:4:2 ->
   4 │   | true => Bool::false
     │     ╰──╯
 
-Warning: The binding name:
+Warning: You wrote the following pattern:
            true
-         is equal to an un-imported constructor of:
-           Bool
+         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 ->
 
@@ -290,10 +290,10 @@ In file $FILE:5:2 ->
   5 │   | false => Bool::true
     │     ╰───╯
 
-Warning: The binding name:
+Warning: You wrote the following pattern:
            false
-         is equal to an un-imported constructor of:
-           Bool
+         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 ->
 
@@ -311,10 +311,10 @@ In file $FILE:8:2 ->
   8 │   | true => real_true
     │     ╰──╯
 
-Warning: The binding name:
+Warning: You wrote the following pattern:
            true
-         is equal to an un-imported constructor of:
-           Bool
+         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!