From fef578fd519ce82a62d78028f3dae7b6f07e7b95 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Sat, 4 Jan 2025 20:04:11 +0800
Subject: [PATCH] fix: dont

---
 base/src/main/java/org/aya/tyck/pat/PatternTycker.java | 9 +++++----
 1 file changed, 5 insertions(+), 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
index 4009ebcaf..baa85323d 100644
--- 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;
     }