merge: #1014 (Freeze holes in context)

Fix #1013 Thanks @dannypsnl for reporting this 🎉
aya-prover · Nov 15, 2023 · 4a21d50 · 4a21d50
2 parents 69b0f2d + 1206ac9
commit 4a21d50
Showing 1 changed file with 11 additions and 14 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;
@@ -14,11 +15,7 @@
 import org.aya.util.reporter.Problem;
 import org.jetbrains.annotations.NotNull;
 
-public record Goal(
-  @NotNull TyckState state,
-  @NotNull MetaTerm hole,
-  @NotNull ImmutableSeq<LocalVar> scope
-) implements Problem {
+public record Goal(@NotNull TyckState state, @NotNull MetaTerm hole, @NotNull ImmutableSeq<LocalVar> scope) implements Problem {
   @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
     var meta = hole.ref();
     var nullableResult = meta.info.result();
@@ -30,18 +27,18 @@ 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"))));
       })),
-      meta.conditions.isNotEmpty() ?
-        Doc.vcat(
-          ImmutableSeq.of(Doc.plain("To ensure confluence:"))
-            .concat(meta.conditions.toImmutableSeq().map(tup -> Doc.par(1, Doc.cat(
-              Doc.plain("Given "),
-              Doc.parened(tup.component1().toDoc(options)),
-              Doc.plain(", we should have: "),
-              tup.component2().toDoc(options)
-            )))))
+      meta.conditions.isNotEmpty() ? Doc.vcat(
+        ImmutableSeq.of(Doc.plain("To ensure confluence:"))
+          .concat(meta.conditions.toImmutableSeq().map(tup -> Doc.par(1, Doc.cat(
+            Doc.plain("Given "),
+            Doc.parened(tup.component1().toDoc(options)),
+            Doc.plain(", we should have: "),
+            tup.component2().freezeHoles(state).toDoc(options)
+          )))))
         : Doc.empty()
     );
     var metas = state.metas();