conquer: cleanup, improve unification getType

aya-prover · Jan 6, 2023 · 94b2f8b · 94b2f8b
1 parent c4e7b1d
commit 94b2f8b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 7 deletions.
diff --git a/base/src/main/java/org/aya/tyck/pat/Conquer.java b/base/src/main/java/org/aya/tyck/pat/Conquer.java
@@ -89,7 +89,7 @@ private void checkConditions(int nth, int i, Restr.Side<Term> condition, Subst m
       } else if (matchResult instanceof ErrorTerm error && error.description() instanceof MetaTerm hole) {
         hole.ref().conditions.append(Tuple.of(subst, newBody));
       }
-      var retSubst = DeltaExpander.buildSubst(def.telescope, currentClause.patterns().map(t -> t.map(Pat::toTerm)));
+      var retSubst = DeltaExpander.buildSubst(def.telescope, args);
       retSubst.add(subst);
       return tycker.unifyReported(newBody, matchResult, def.result.subst(retSubst),
         sourcePos, ctx, comparison -> new ClausesProblem.Conditions(

diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -239,7 +239,7 @@ private boolean visitLists(SeqView<Term> l, SeqView<Term> r, Sub lr, Sub rl, @No
     @NotNull Callable lhs, @NotNull Callable rhs, Sub lr, Sub rl,
     @NotNull DefVar<? extends Def, ? extends Decl.Telescopic<?>> lhsRef, int ulift
   ) {
-    var retType = getType(lhs, lhsRef);
+    var retType = synthesizer().press(lhs);
     if (synthesizer().tryPress(retType) instanceof SortTerm sort && sort.isProp()) return retType;
     // Lossy comparison
     if (visitArgs(lhs.args(), rhs.args(), lr, rl,
@@ -251,10 +251,6 @@ private boolean visitLists(SeqView<Term> l, SeqView<Term> r, Sub lr, Sub rl, @No
   /** TODO: Revise when JDK 20 is released. */
   private record Pair(Term lhs, Term rhs) {}
 
-  private @NotNull Term getType(@NotNull Callable lhs, @NotNull DefVar<? extends Def, ? extends Decl.Telescopic<?>> lhsRef) {
-    return Def.defResult(lhsRef).subst(DeltaExpander.buildSubst(Def.defTele(lhsRef), lhs.args()));
-  }
-
   private boolean doCompareTyped(@NotNull Term type, @NotNull Term lhs, @NotNull Term rhs, Sub lr, Sub rl) {
     // Skip tracing, because too easy.
     // Note that it looks tempting to apply some unification here, but it is not correct:
@@ -537,7 +533,7 @@ case OutTerm(var lPhi, var pal, var lU) -> {
    * If called from {@link #doCompareUntyped} then probably not so lossy.
    */
   private @Nullable Term lossyUnifyCon(ConCall lhs, ConCall rhs, Sub lr, Sub rl, DefVar<CtorDef, TeleDecl.DataCtor> lef) {
-    var retType = getType(lhs, lef);
+    var retType = synthesizer().press(lhs);
     var dataRef = lhs.head().dataRef();
     if (Def.defResult(dataRef).isProp()) return retType;
     var dataAlgs = lhs.head().dataArgs();