From e20b911c1b74d29e96410cbb49800209e18390cb Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 02:20:11 -0500
Subject: [PATCH] unify: guard error terms

---
 base/src/main/java/org/aya/tyck/unify/Unifier.java | 5 +++--
 1 file changed, 3 insertions(+), 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
index c353c86d77..1fa29c5463 100644
--- 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);