fix: dont

aya-prover · Jan 4, 2025 · fef578f · fef578f
1 parent 06ce1a9
commit fef578f
Showing 1 changed file with 5 additions and 4 deletions.
diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
@@ -7,6 +7,7 @@
 import kala.collection.mutable.MutableList;
 import kala.control.Result;
 import kala.value.MutableValue;
+import org.aya.generic.Constants;
 import org.aya.generic.Renamer;
 import org.aya.generic.State;
 import org.aya.generic.term.DTKind;
@@ -163,7 +164,7 @@ public record TyckResult(
 
         yield new Pat.Bind(bind, type);
       }
-      case Pattern.CalmFace.INSTANCE -> doGeneratePattern(type);
+      case Pattern.CalmFace.INSTANCE -> doGeneratePattern(type, Constants.ANONYMOUS_PREFIX);
       case Pattern.Number(var number) -> {
         var ty = whnf(type);
         if (ty instanceof DataCall dataCall) {
@@ -372,8 +373,8 @@ private class Closer implements AutoCloseable {
     }
   }
 
-  private @NotNull Pat doGeneratePattern(@NotNull Term type) {
-    var freshVar = nameGen.bindName(currentParam.name());
+  private @NotNull Pat doGeneratePattern(@NotNull Term type, @NotNull String name) {
+    var freshVar = nameGen.bindName(name);
     if (exprTycker.whnf(type) instanceof DataCall dataCall) {
       // this pattern would be a Con, it can be inferred
       // TODO: I NEED A SOURCE POS!!
@@ -392,7 +393,7 @@ private class Closer implements AutoCloseable {
    */
   private @NotNull Pat generatePattern() {
     try (var _ = instCurrentParam()) {
-      var pat = doGeneratePattern(currentParam.type());
+      var pat = doGeneratePattern(currentParam.type(), currentParam.name());
       addArgSubst(pat, currentParam.type());
       return pat;
     }