synth: whnf more

aya-prover · Jan 6, 2023 · 0a999f8 · 0a999f8
1 parent b0ae994
commit 0a999f8
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/base/src/main/java/org/aya/tyck/error/HoleProblem.java b/base/src/main/java/org/aya/tyck/error/HoleProblem.java
@@ -49,9 +49,9 @@ record IllTypedError(
   ) implements HoleProblem {
     @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
       return Doc.vcat(
-        Doc.english("The meta (denoted ?) is supposed to satisfy"),
+        Doc.english("The meta (denoted ? below) is supposed to satisfy:"),
         Doc.par(1, result.toDoc(options)),
-        Doc.english("However, the solution below does not have the same type:"),
+        Doc.english("However, the solution below does not seem so:"),
         Doc.par(1, solution.toDoc(options))
       );
     }

diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java
@@ -106,7 +106,7 @@ public Unifier(
         needUnify = false;
       }
       case MetaInfo.AnyType() -> {
-        var synthesize = checker.synthesizer().synthesize(preRhs);
+        var synthesize = checker.synthesizer().tryPress(preRhs);
         if (!(synthesize instanceof SortTerm)) {
           reporter.report(new HoleProblem.IllTypedError(lhs, meta.info, preRhs));
           return null;