unify: a problematic implement of conversion check of sigma type

base/src/main/java/org/aya/tyck/unify/TermComparator.java

@@ -36,12 +36,19 @@ case Pair(LamTerm(var lbody), LamTerm(var rbody)) -> state().dCtx().with(pi.para
         case Pair(_, LamTerm rambda) -> compareLambda(rambda, lhs, pi);
         default -> false;
       };
-      case SigmaTerm(var components) -> {
-        components.forEachIndexed((i, iType) -> {
+      case SigmaTerm(var paramSeq) -> {
+        // We use view since we need to instantiate the remaining params after tyck some component.
+        var params = paramSeq.view();
+        var size = paramSeq.size();
+        for (var i = 0; i < size; ++ i) {
           var l = ProjTerm.make(lhs, i);
           var r = ProjTerm.make(rhs, i);
-        });
-        throw new UnsupportedOperationException("TODO: hoshino");
+          var param = params.getFirst();
+          if (! compare(l, r, param)) yield false;
+          params = params.drop(1).mapIndexed((j, term) ->
+            term.replace(j, l));
+        }
+        yield true;
       }
       default -> false;
     };

syntax/src/main/java/org/aya/syntax/ref/DeBruijnCtx.java

@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.ref;
 
+import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import org.aya.syntax.core.term.Term;
 import org.aya.util.error.InternalException;
@@ -40,4 +41,17 @@ public void push(@NotNull Term type) {
     if (ctx.isEmpty()) throw new InternalException("empty ctx");
     return ctx.removeLast();
   }
+
+  public @NotNull ImmutableSeq<Term> popMany(int how) {
+    if (how < 0) throw new InternalException(STR."Unable to pop \{how} elements without elements");
+
+    var acc = MutableList.<Term>create();
+
+    while (how > 0) {
+      -- how;
+      acc.append(pop());
+    }
+
+    return acc.toImmutableSeq();
+  }
 }