error: freeze holes

aya-prover · Nov 15, 2023 · 27b8527 · 27b8527
1 parent fe6ae51
commit 27b8527
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/base/src/main/java/org/aya/tyck/error/Goal.java b/base/src/main/java/org/aya/tyck/error/Goal.java
@@ -5,6 +5,7 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.core.term.ErrorTerm;
 import org.aya.core.term.MetaTerm;
+import org.aya.core.term.Term;
 import org.aya.generic.util.NormalizeMode;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.LocalVar;
@@ -30,6 +31,7 @@ public record Goal(
       Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), result.normalize(state, NormalizeMode.NF).toDoc(options)))),
       Doc.plain("Context:"),
       Doc.vcat(meta.fullTelescope().map(param -> {
+        param = new Term.Param(param, param.type().freezeHoles(state));
         var paramDoc = param.toDoc(options);
         return Doc.par(1, scope.contains(param.ref()) ? paramDoc : Doc.sep(paramDoc, Doc.parened(Doc.english("not in scope"))));
       })),