unify: guard error terms

aya-prover · Jan 6, 2023 · e20b911 · e20b911
1 parent 0a999f8
commit e20b911
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/base/src/main/java/org/aya/tyck/unify/Unifier.java b/base/src/main/java/org/aya/tyck/unify/Unifier.java
@@ -96,7 +96,8 @@ public Unifier(
       reporter, false, false, traceBuilder, state, pos, ctx.deriveMap()), lr, rl);
     // Check the expected type.
     var needUnify = true;
-    switch (meta.info) {
+    if (preRhs instanceof ErrorTerm) needUnify = false;
+    else switch (meta.info) {
       case MetaInfo.AnyType()when preRhs instanceof Formation -> needUnify = false;
       case MetaInfo.AnyType()when preRhs instanceof MetaTerm rhsMeta -> {
         if (!rhsMeta.ref().info.isType(checker.synthesizer())) {
@@ -141,7 +142,7 @@ public Unifier(
         }
       }
     }
-    if (!needUnify) providedType = SortTerm.Type0;
+    if (!needUnify && providedType == null) providedType = SortTerm.Type0;
     // Pattern unification: buildSubst(lhs.args.invert(), meta.telescope)
     var subst = DeltaExpander.buildSubst(meta.contextTele, lhs.contextArgs());
     var overlap = invertSpine(subst, lhs, meta);