From 57d4063dd1810d60b275b1c36af656c6fda21298 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 02:42:33 -0500
Subject: [PATCH 01/12] unify: irrelevance of `Prop`

---
 .../java/org/aya/tyck/tycker/StatedTycker.java  | 12 ++++++++++++
 .../java/org/aya/tyck/unify/TermComparator.java | 17 ++++++-----------
 2 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java b/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java
index 357d1629ec..2d6f1627a2 100644
--- a/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java
@@ -7,9 +7,12 @@
 import org.aya.core.UntypedParam;
 import org.aya.core.def.*;
 import org.aya.core.term.*;
+import org.aya.core.visitor.Subst;
 import org.aya.generic.Modifier;
 import org.aya.generic.util.InternalException;
 import org.aya.generic.util.NormalizeMode;
+import org.aya.guest0x0.cubical.CofThy;
+import org.aya.guest0x0.cubical.Restr;
 import org.aya.ref.DefVar;
 import org.aya.tyck.Result;
 import org.aya.tyck.env.LocalCtx;
@@ -86,4 +89,13 @@ protected StatedTycker(@NotNull Reporter reporter, @Nullable Trace.Builder trace
   public @NotNull Unifier unifier(@NotNull SourcePos pos, @NotNull Ordering ord, @NotNull LocalCtx ctx) {
     return new Unifier(ord, reporter, false, true, traceBuilder, state, pos, ctx);
   }
+
+  /**
+   * <code>Sub lr, Sub rl</code> are unused because they are solely for the purpose of unification.
+   * In this case, we don't expect unification.
+   */
+  protected final boolean compareRestr(@NotNull Restr<Term> lhs, @NotNull Restr<Term> rhs) {
+    return CofThy.conv(lhs, new Subst(), s -> CofThy.satisfied(s.restr(state, rhs)))
+      && CofThy.conv(rhs, new Subst(), s -> CofThy.satisfied(s.restr(state, lhs)));
+  }
 }
diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
index 74de53d53d..4da612a2a5 100644
--- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -20,7 +20,6 @@
 import org.aya.generic.util.InternalException;
 import org.aya.guest0x0.cubical.CofThy;
 import org.aya.guest0x0.cubical.Partial;
-import org.aya.guest0x0.cubical.Restr;
 import org.aya.prettier.AyaPrettierOptions;
 import org.aya.ref.AnyVar;
 import org.aya.ref.DefVar;
@@ -259,6 +258,11 @@ private record Pair(Term lhs, Term rhs) {}
   }
 
   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:
+    // If ?x =_A y where A : Prop, then it may not be the case that ?x is y!
+    // I think Arend has probably made such a mistake before, but they removed this feature anyway.
+    if (synthesizer().tryPress(type) instanceof SortTerm sort && sort.isProp()) return true;
     traceEntrance(new Trace.UnifyT(lhs.freezeHoles(state), rhs.freezeHoles(state),
       pos, type.freezeHoles(state)));
     var ret = switch (type) {
@@ -391,15 +395,6 @@ private boolean compareCube(@NotNull PathTerm lhs, @NotNull PathTerm rhs, Sub lr
     }));
   }
 
-  /**
-   * Sub lr, Sub rl are unused because they are solely for the purpose of unification.
-   * In this case, we don't expect unification.
-   */
-  private boolean compareRestr(@NotNull Restr<Term> lhs, @NotNull Restr<Term> rhs) {
-    return CofThy.conv(lhs, new Subst(), s -> CofThy.satisfied(s.restr(state, rhs)))
-      && CofThy.conv(rhs, new Subst(), s -> CofThy.satisfied(s.restr(state, lhs)));
-  }
-
   /**
    * @implNote Do not need to compute result type precisely because unification won't need this info
    * (written by re-xyr)
@@ -535,7 +530,7 @@ case OutTerm(var lPhi, var pal, var lU) -> {
     };
   }
 
-  @NotNull private static InternalException noRules(@NotNull Term preLhs) {
+  private static @NotNull InternalException noRules(@NotNull Term preLhs) {
     return new InternalException(preLhs.getClass() + ": " + preLhs.toDoc(AyaPrettierOptions.debug()).debugRender());
   }
 

From 38d437753c2f60db630e54f312f1a197afe87811 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 02:52:30 -0500
Subject: [PATCH 02/12] unify: improve irrelevance of `Prop`

---
 base/src/main/java/org/aya/core/def/Def.java              | 7 +++++--
 base/src/main/java/org/aya/tyck/tycker/StatedTycker.java  | 3 ++-
 base/src/main/java/org/aya/tyck/unify/TermComparator.java | 4 +++-
 3 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/base/src/main/java/org/aya/core/def/Def.java b/base/src/main/java/org/aya/core/def/Def.java
index dd91c35edb..a7dd32a4e5 100644
--- a/base/src/main/java/org/aya/core/def/Def.java
+++ b/base/src/main/java/org/aya/core/def/Def.java
@@ -13,6 +13,7 @@
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.DefVar;
 import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 
 import java.util.Objects;
@@ -35,8 +36,10 @@ public sealed interface Def extends AyaDocile, GenericDef permits SubLevelDef, T
       // guaranteed as this is already a core term
     else return defVar.concrete.checkedBody;
   }
-  static @NotNull Term defResult(@NotNull DefVar<? extends Def, ? extends Decl.Telescopic<?>> defVar) {
-    if (defVar.core != null) return defVar.core.result();
+  @SuppressWarnings("unchecked") @Contract(pure = true)
+  static <T extends Term> @NotNull T
+  defResult(@NotNull DefVar<? extends Def, ? extends Decl.Telescopic<? extends T>> defVar) {
+    if (defVar.core != null) return (T) defVar.core.result();
       // guaranteed as this is already a core term
     else return Objects.requireNonNull(defVar.concrete.signature()).result;
   }
diff --git a/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java b/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java
index 2d6f1627a2..9a519e0442 100644
--- a/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java
+++ b/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java
@@ -46,7 +46,8 @@ protected StatedTycker(@NotNull Reporter reporter, @Nullable Trace.Builder trace
     return term.normalize(state, NormalizeMode.WHNF);
   }
 
-  protected final @NotNull <D extends Def, S extends Decl & Decl.Telescopic<?>> Result defCall(DefVar<D, S> defVar, Callable.Factory<D, S> function) {
+  protected final <D extends Def, S extends Decl & Decl.Telescopic<? extends Term>> @NotNull Result
+  defCall(DefVar<D, S> defVar, Callable.Factory<D, S> function) {
     var tele = Def.defTele(defVar);
     var teleRenamed = tele.map(LamTerm::paramRenamed);
     // unbound these abstracted variables
diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
index 4da612a2a5..6f793adc47 100644
--- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -239,6 +239,7 @@ private boolean visitLists(SeqView<Term> l, SeqView<Term> r, Sub lr, Sub rl, @No
     @NotNull DefVar<? extends Def, ? extends Decl.Telescopic<?>> lhsRef, int ulift
   ) {
     var retType = getType(lhs, lhsRef);
+    if (synthesizer().tryPress(retType) instanceof SortTerm sort && sort.isProp()) return retType;
     // Lossy comparison
     if (visitArgs(lhs.args(), rhs.args(), lr, rl,
       Term.Param.subst(Def.defTele(lhsRef), ulift))) return retType;
@@ -539,9 +540,10 @@ 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);
+    if (Def.defResult(lhs.head().dataRef()).isProp()) return retType;
     if (!visitArgs(lhs.head().dataArgs(), rhs.head().dataArgs(), lr, rl,
       Term.Param.subst(Def.defTele(lef.core.dataRef), lhs.ulift()))) return null;
-    var retType = getType(lhs, lef);
     if (visitArgs(lhs.conArgs(), rhs.conArgs(), lr, rl,
       Term.Param.subst(lef.core.selfTele, lhs.ulift())))
       return retType;

From a91bd13c39cbbcd911caa3582706c3261a2bb232 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 03:06:04 -0500
Subject: [PATCH 03/12] unify: substitute data type properly

---
 .../main/java/org/aya/core/term/SigmaTerm.java   |  5 ++---
 .../main/java/org/aya/core/visitor/EndoTerm.java |  5 ++---
 .../java/org/aya/tyck/pat/PatClassifier.java     |  5 ++---
 .../java/org/aya/tyck/unify/TermComparator.java  | 16 ++++++++--------
 4 files changed, 14 insertions(+), 17 deletions(-)

diff --git a/base/src/main/java/org/aya/core/term/SigmaTerm.java b/base/src/main/java/org/aya/core/term/SigmaTerm.java
index baf09410a0..573169d28d 100644
--- a/base/src/main/java/org/aya/core/term/SigmaTerm.java
+++ b/base/src/main/java/org/aya/core/term/SigmaTerm.java
@@ -1,11 +1,10 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.core.term;
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableArrayList;
 import kala.collection.mutable.MutableList;
-import kala.collection.mutable.MutableMap;
 import org.aya.core.visitor.BetaExpander;
 import org.aya.core.visitor.Subst;
 import org.aya.generic.SortKind;
@@ -84,7 +83,7 @@ record Item(@NotNull CoeTerm coe, @NotNull Arg<Term> arg) {
   public <T> @Nullable TupTerm check(@NotNull ImmutableSeq<? extends T> it, @NotNull BiFunction<T, Term, Term> inherit) {
     var items = MutableList.<Arg<Term>>create();
     var againstTele = params.view();
-    var subst = new Subst(MutableMap.create());
+    var subst = new Subst();
     for (var iter = it.iterator(); iter.hasNext(); ) {
       var item = iter.next();
       var first = againstTele.first().subst(subst);
diff --git a/base/src/main/java/org/aya/core/visitor/EndoTerm.java b/base/src/main/java/org/aya/core/visitor/EndoTerm.java
index dcc5585635..873706492d 100644
--- a/base/src/main/java/org/aya/core/visitor/EndoTerm.java
+++ b/base/src/main/java/org/aya/core/visitor/EndoTerm.java
@@ -1,8 +1,7 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.core.visitor;
 
-import kala.collection.mutable.MutableMap;
 import org.aya.core.term.*;
 import org.aya.generic.util.InternalException;
 import org.aya.ref.AnyVar;
@@ -37,7 +36,7 @@ public interface EndoTerm extends UnaryOperator<Term> {
   /** Not an IntelliJ Renamer. */
   record Renamer(@NotNull Subst subst) implements EndoTerm {
     public Renamer() {
-      this(new Subst(MutableMap.create()));
+      this(new Subst());
     }
 
     private @NotNull Term.Param handleBinder(@NotNull Term.Param param) {
diff --git a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
index 6c0af32ff9..7ccb95f01f 100644
--- a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
+++ b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
@@ -6,7 +6,6 @@
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
-import kala.collection.mutable.MutableMap;
 import kala.tuple.Tuple;
 import kala.tuple.primitive.IntObjTuple2;
 import kala.value.MutableValue;
@@ -103,8 +102,8 @@ public static void confluence(
       for (int i = 1, size = contents.size(); i < size; i++) {
         var lhsInfo = contents.get(i - 1);
         var rhsInfo = contents.get(i);
-        var lhsSubst = new Subst(MutableMap.create());
-        var rhsSubst = new Subst(MutableMap.create());
+        var lhsSubst = new Subst();
+        var rhsSubst = new Subst();
         var ctx = PatUnify.unifyPat(lhsInfo.component2().patterns().map(Arg::term), rhsInfo.component2().patterns().map(Arg::term),
           lhsSubst, rhsSubst, tycker.ctx.deriveMap());
         domination(ctx, rhsSubst, tycker.reporter, lhsInfo.component1(), rhsInfo.component1(), rhsInfo.component2());
diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
index 6f793adc47..40fb49323e 100644
--- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -15,6 +15,7 @@
 import org.aya.core.def.PrimDef;
 import org.aya.core.term.*;
 import org.aya.core.visitor.AyaRestrSimplifier;
+import org.aya.core.visitor.DeltaExpander;
 import org.aya.core.visitor.Subst;
 import org.aya.generic.SortKind;
 import org.aya.generic.util.InternalException;
@@ -251,11 +252,7 @@ private boolean visitLists(SeqView<Term> l, SeqView<Term> r, Sub lr, Sub rl, @No
   private record Pair(Term lhs, Term rhs) {}
 
   private @NotNull Term getType(@NotNull Callable lhs, @NotNull DefVar<? extends Def, ? extends Decl.Telescopic<?>> lhsRef) {
-    var substMap = MutableMap.<AnyVar, Term>create();
-    for (var pa : lhs.args().view().zip(Def.defTele(lhsRef))) {
-      substMap.set(pa.component2().ref(), pa.component1().term());
-    }
-    return Def.defResult(lhsRef).subst(substMap);
+    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) {
@@ -541,11 +538,14 @@ case OutTerm(var lPhi, var pal, var lU) -> {
    */
   private @Nullable Term lossyUnifyCon(ConCall lhs, ConCall rhs, Sub lr, Sub rl, DefVar<CtorDef, TeleDecl.DataCtor> lef) {
     var retType = getType(lhs, lef);
-    if (Def.defResult(lhs.head().dataRef()).isProp()) return retType;
-    if (!visitArgs(lhs.head().dataArgs(), rhs.head().dataArgs(), lr, rl,
+    var dataRef = lhs.head().dataRef();
+    if (Def.defResult(dataRef).isProp()) return retType;
+    var dataAlgs = lhs.head().dataArgs();
+    if (!visitArgs(dataAlgs, rhs.head().dataArgs(), lr, rl,
       Term.Param.subst(Def.defTele(lef.core.dataRef), lhs.ulift()))) return null;
+    var ownerSubst = DeltaExpander.buildSubst(Def.defTele(dataRef), dataAlgs);
     if (visitArgs(lhs.conArgs(), rhs.conArgs(), lr, rl,
-      Term.Param.subst(lef.core.selfTele, lhs.ulift())))
+      Term.Param.subst(lef.core.selfTele, ownerSubst, lhs.ulift())))
       return retType;
     return null;
   }

From 3f89c8f6877f0c30dfc1c71a94b6507422ce3cb1 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 03:12:51 -0500
Subject: [PATCH 04/12] conquer: use simpler interface

---
 base/src/main/java/org/aya/tyck/pat/Conquer.java | 8 ++++----
 1 file changed, 4 insertions(+), 4 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
index 705f234f5d..2a786fbb85 100644
--- a/base/src/main/java/org/aya/tyck/pat/Conquer.java
+++ b/base/src/main/java/org/aya/tyck/pat/Conquer.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck.pat;
 
@@ -16,9 +16,9 @@
 import org.aya.guest0x0.cubical.CofThy;
 import org.aya.guest0x0.cubical.Partial;
 import org.aya.guest0x0.cubical.Restr;
-import org.aya.tyck.ExprTycker;
 import org.aya.tyck.env.MapLocalCtx;
 import org.aya.tyck.error.UnifyInfo;
+import org.aya.tyck.tycker.UnifiedTycker;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
@@ -33,11 +33,11 @@ public record Conquer(
   @NotNull ImmutableSeq<Term.Matching> matchings,
   @NotNull SourcePos sourcePos,
   boolean orderIndependent,
-  @NotNull ExprTycker tycker
+  @NotNull UnifiedTycker tycker
 ) {
   public static void against(
     @NotNull FnDef def, boolean orderIndependent,
-    @NotNull ExprTycker tycker, @NotNull SourcePos pos
+    @NotNull UnifiedTycker tycker, @NotNull SourcePos pos
   ) {
     var matchings = def.body.getRightValue();
     var conquer = new Conquer(def, matchings, pos, orderIndependent, tycker);

From c4e7b1d5183ba584ac7f443aa5f56a6bb1d21405 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 03:20:12 -0500
Subject: [PATCH 05/12] conquer: subst return type

---
 base/src/main/java/org/aya/tyck/pat/Conquer.java | 9 ++++++---
 1 file changed, 6 insertions(+), 3 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
index 2a786fbb85..157418e672 100644
--- a/base/src/main/java/org/aya/tyck/pat/Conquer.java
+++ b/base/src/main/java/org/aya/tyck/pat/Conquer.java
@@ -11,6 +11,7 @@
 import org.aya.core.term.MetaTerm;
 import org.aya.core.term.Term;
 import org.aya.core.visitor.AyaRestrSimplifier;
+import org.aya.core.visitor.DeltaExpander;
 import org.aya.core.visitor.Subst;
 import org.aya.generic.util.NormalizeMode;
 import org.aya.guest0x0.cubical.CofThy;
@@ -84,11 +85,13 @@ private void checkConditions(int nth, int i, Restr.Side<Term> condition, Subst m
       var matchResult = new FnCall(def.ref, 0, args).normalize(tycker.state, NormalizeMode.WHNF).subst(subst);
       currentClause.patterns().forEach(p -> p.term().storeBindings(ctx, subst));
       if (newBody instanceof ErrorTerm error && error.description() instanceof MetaTerm hole) {
-        hole.ref().conditions.append(Tuple.of(matchy, matchResult));
+        hole.ref().conditions.append(Tuple.of(subst, matchResult));
       } else if (matchResult instanceof ErrorTerm error && error.description() instanceof MetaTerm hole) {
-        hole.ref().conditions.append(Tuple.of(matchy, newBody));
+        hole.ref().conditions.append(Tuple.of(subst, newBody));
       }
-      return tycker.unifyReported(newBody, matchResult, def.result.subst(matchy),
+      var retSubst = DeltaExpander.buildSubst(def.telescope, currentClause.patterns().map(t -> t.map(Pat::toTerm)));
+      retSubst.add(subst);
+      return tycker.unifyReported(newBody, matchResult, def.result.subst(retSubst),
         sourcePos, ctx, comparison -> new ClausesProblem.Conditions(
           sourcePos, currentClause.sourcePos(), nth + 1, i, args, new UnifyInfo(tycker.state), comparison));
     });

From 94b2f8b546025a7d5128d297c4c749f85422a0d8 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 03:25:47 -0500
Subject: [PATCH 06/12] conquer: cleanup, improve unification `getType`

---
 base/src/main/java/org/aya/tyck/pat/Conquer.java          | 2 +-
 base/src/main/java/org/aya/tyck/unify/TermComparator.java | 8 ++------
 2 files changed, 3 insertions(+), 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
index 157418e672..0e8d6a0e5b 100644
--- 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
index 40fb49323e..c1b248683a 100644
--- 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();

From 5dfa3a0f426c31bcd5ff17a6326ddc4db51e233b Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 03:30:26 -0500
Subject: [PATCH 07/12] confluence: prepare for unify pat to produce a subst

---
 base/src/main/java/org/aya/core/pat/PatUnify.java  | 14 ++++++++------
 base/src/main/java/org/aya/tyck/StmtTycker.java    |  2 +-
 .../main/java/org/aya/tyck/pat/PatClassifier.java  |  5 ++++-
 3 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/base/src/main/java/org/aya/core/pat/PatUnify.java b/base/src/main/java/org/aya/core/pat/PatUnify.java
index 5db07b832c..5d178dd322 100644
--- a/base/src/main/java/org/aya/core/pat/PatUnify.java
+++ b/base/src/main/java/org/aya/core/pat/PatUnify.java
@@ -1,13 +1,14 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.core.pat;
 
-import kala.collection.SeqLike;
+import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.core.term.RefTerm;
+import org.aya.core.term.Term;
 import org.aya.core.visitor.Subst;
-import org.aya.prettier.AyaPrettierOptions;
 import org.aya.generic.util.InternalException;
+import org.aya.prettier.AyaPrettierOptions;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.LocalVar;
 import org.aya.tyck.env.LocalCtx;
@@ -18,7 +19,7 @@
  * The unification of patterns. This is <strong>not</strong> pattern unification.
  *
  * @author ice1000
- * @see PatUnify#unifyPat(SeqLike, SeqLike, Subst, Subst, LocalCtx)
+ * @see PatUnify#unifyPat(ImmutableSeq, SeqView, SeqView, Subst, Subst, LocalCtx)
  */
 public record PatUnify(@NotNull Subst lhsSubst, @NotNull Subst rhsSubst, @NotNull LocalCtx ctx) {
   private void unify(@NotNull Pat lhs, @NotNull Pat rhs) {
@@ -108,8 +109,9 @@ private static void unifyPat(Pat lhs, Pat rhs, Subst lhsSubst, Subst rhsSubst, L
    * @see PatUnify#visitAs(LocalVar, org.aya.core.pat.Pat)
    */
   public static @NotNull LocalCtx unifyPat(
-    @NotNull SeqLike<Pat> lpats,
-    @NotNull SeqLike<Pat> rpats,
+    @NotNull ImmutableSeq<Term.Param> telescope,
+    @NotNull SeqView<Pat> lpats,
+    @NotNull SeqView<Pat> rpats,
     @NotNull Subst lhsSubst,
     @NotNull Subst rhsSubst,
     @NotNull LocalCtx ctx
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index 97e091bd5a..64a4f23485 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -89,7 +89,7 @@ public StmtTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuild
               def = factory.apply(result.result(), Either.right(result.matchings()));
               if (!result.hasLhsError()) {
                 tracing(builder -> builder.shift(new Trace.LabelT(pos, "confluence check")));
-                PatClassifier.confluence(result, tycker, pos,
+                PatClassifier.confluence(signature.param(), result, tycker, pos,
                   PatClassifier.classify(result.clauses(), signature.param(), tycker, pos));
                 tracing(TreeBuilder::reduce);
               }
diff --git a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
index 7ccb95f01f..91ab6c79f3 100644
--- a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
+++ b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
@@ -90,6 +90,7 @@ public static int[] firstMatchDomination(
   }
 
   public static void confluence(
+    @NotNull ImmutableSeq<Term.Param> telescope,
     @NotNull ClauseTycker.PatResult clauses,
     @NotNull ExprTycker tycker, @NotNull SourcePos pos,
     @NotNull MCT<Term, PatErr> mct
@@ -104,7 +105,9 @@ public static void confluence(
         var rhsInfo = contents.get(i);
         var lhsSubst = new Subst();
         var rhsSubst = new Subst();
-        var ctx = PatUnify.unifyPat(lhsInfo.component2().patterns().map(Arg::term), rhsInfo.component2().patterns().map(Arg::term),
+        var ctx = PatUnify.unifyPat(telescope,
+          lhsInfo.component2().patterns().view().map(Arg::term),
+          rhsInfo.component2().patterns().view().map(Arg::term),
           lhsSubst, rhsSubst, tycker.ctx.deriveMap());
         domination(ctx, rhsSubst, tycker.reporter, lhsInfo.component1(), rhsInfo.component1(), rhsInfo.component2());
         domination(ctx, lhsSubst, tycker.reporter, rhsInfo.component1(), lhsInfo.component1(), lhsInfo.component2());

From 60474a6a9176bc237c49ecc3f222d095d8e93509 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 16:58:35 -0500
Subject: [PATCH 08/12] refactor: introduce a standalone class for confluence
 check

---
 .../main/java/org/aya/core/pat/PatUnify.java  |  4 +-
 .../main/java/org/aya/tyck/StmtTycker.java    |  4 +-
 .../java/org/aya/tyck/pat/PatClassifier.java  | 54 --------------
 .../main/java/org/aya/tyck/pat/YouTrack.java  | 74 +++++++++++++++++++
 4 files changed, 78 insertions(+), 58 deletions(-)
 create mode 100644 base/src/main/java/org/aya/tyck/pat/YouTrack.java

diff --git a/base/src/main/java/org/aya/core/pat/PatUnify.java b/base/src/main/java/org/aya/core/pat/PatUnify.java
index 5d178dd322..878203b24e 100644
--- a/base/src/main/java/org/aya/core/pat/PatUnify.java
+++ b/base/src/main/java/org/aya/core/pat/PatUnify.java
@@ -5,7 +5,6 @@
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.core.term.RefTerm;
-import org.aya.core.term.Term;
 import org.aya.core.visitor.Subst;
 import org.aya.generic.util.InternalException;
 import org.aya.prettier.AyaPrettierOptions;
@@ -19,7 +18,7 @@
  * The unification of patterns. This is <strong>not</strong> pattern unification.
  *
  * @author ice1000
- * @see PatUnify#unifyPat(ImmutableSeq, SeqView, SeqView, Subst, Subst, LocalCtx)
+ * @see #unifyPat(SeqView, SeqView, Subst, Subst, LocalCtx)
  */
 public record PatUnify(@NotNull Subst lhsSubst, @NotNull Subst rhsSubst, @NotNull LocalCtx ctx) {
   private void unify(@NotNull Pat lhs, @NotNull Pat rhs) {
@@ -109,7 +108,6 @@ private static void unifyPat(Pat lhs, Pat rhs, Subst lhsSubst, Subst rhsSubst, L
    * @see PatUnify#visitAs(LocalVar, org.aya.core.pat.Pat)
    */
   public static @NotNull LocalCtx unifyPat(
-    @NotNull ImmutableSeq<Term.Param> telescope,
     @NotNull SeqView<Pat> lpats,
     @NotNull SeqView<Pat> rpats,
     @NotNull Subst lhsSubst,
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index 64a4f23485..4010646a49 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -25,6 +25,7 @@
 import org.aya.tyck.pat.ClauseTycker;
 import org.aya.tyck.pat.Conquer;
 import org.aya.tyck.pat.PatClassifier;
+import org.aya.tyck.pat.YouTrack;
 import org.aya.tyck.trace.Trace;
 import org.aya.tyck.tycker.TracedTycker;
 import org.aya.util.Arg;
@@ -89,7 +90,8 @@ public StmtTycker(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuild
               def = factory.apply(result.result(), Either.right(result.matchings()));
               if (!result.hasLhsError()) {
                 tracing(builder -> builder.shift(new Trace.LabelT(pos, "confluence check")));
-                PatClassifier.confluence(signature.param(), result, tycker, pos,
+                var confluence = new YouTrack(signature.param(), tycker, pos);
+                confluence.check(result,
                   PatClassifier.classify(result.clauses(), signature.param(), tycker, pos));
                 tracing(TreeBuilder::reduce);
               }
diff --git a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
index 91ab6c79f3..f33c76e8c6 100644
--- a/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
+++ b/base/src/main/java/org/aya/tyck/pat/PatClassifier.java
@@ -6,21 +6,14 @@
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
-import kala.tuple.Tuple;
-import kala.tuple.primitive.IntObjTuple2;
 import kala.value.MutableValue;
 import org.aya.concrete.Pattern;
 import org.aya.core.def.Def;
 import org.aya.core.pat.Pat;
-import org.aya.core.pat.PatUnify;
 import org.aya.core.term.*;
-import org.aya.core.visitor.Subst;
 import org.aya.generic.util.NormalizeMode;
 import org.aya.ref.AnyVar;
-import org.aya.tyck.ExprTycker;
-import org.aya.tyck.env.LocalCtx;
 import org.aya.tyck.error.TyckOrderError;
-import org.aya.tyck.error.UnifyInfo;
 import org.aya.tyck.tycker.StatedTycker;
 import org.aya.tyck.tycker.TyckState;
 import org.aya.util.Arg;
@@ -89,53 +82,6 @@ public static int[] firstMatchDomination(
     return numbers;
   }
 
-  public static void confluence(
-    @NotNull ImmutableSeq<Term.Param> telescope,
-    @NotNull ClauseTycker.PatResult clauses,
-    @NotNull ExprTycker tycker, @NotNull SourcePos pos,
-    @NotNull MCT<Term, PatErr> mct
-  ) {
-    var result = clauses.result();
-    mct.forEach(results -> {
-      var contents = results.contents()
-        .flatMap(i -> Pat.Preclause.lift(clauses.clauses().get(i))
-          .map(matching -> IntObjTuple2.of(i, matching)));
-      for (int i = 1, size = contents.size(); i < size; i++) {
-        var lhsInfo = contents.get(i - 1);
-        var rhsInfo = contents.get(i);
-        var lhsSubst = new Subst();
-        var rhsSubst = new Subst();
-        var ctx = PatUnify.unifyPat(telescope,
-          lhsInfo.component2().patterns().view().map(Arg::term),
-          rhsInfo.component2().patterns().view().map(Arg::term),
-          lhsSubst, rhsSubst, tycker.ctx.deriveMap());
-        domination(ctx, rhsSubst, tycker.reporter, lhsInfo.component1(), rhsInfo.component1(), rhsInfo.component2());
-        domination(ctx, lhsSubst, tycker.reporter, rhsInfo.component1(), lhsInfo.component1(), lhsInfo.component2());
-        var lhsTerm = lhsInfo.component2().body().subst(lhsSubst);
-        var rhsTerm = rhsInfo.component2().body().subst(rhsSubst);
-        // TODO: Currently all holes at this point are in an ErrorTerm
-        if (lhsTerm instanceof ErrorTerm error && error.description() instanceof MetaTerm hole) {
-          hole.ref().conditions.append(Tuple.of(lhsSubst, rhsTerm));
-        } else if (rhsTerm instanceof ErrorTerm error && error.description() instanceof MetaTerm hole) {
-          hole.ref().conditions.append(Tuple.of(rhsSubst, lhsTerm));
-        }
-        tycker.unifyReported(lhsTerm, rhsTerm, result, pos, ctx, comparison ->
-          new ClausesProblem.Confluence(pos, rhsInfo.component1() + 1, lhsInfo.component1() + 1,
-            comparison, new UnifyInfo(tycker.state), rhsInfo.component2().sourcePos(), lhsInfo.component2().sourcePos()));
-      }
-    });
-  }
-
-  private static void domination(
-    LocalCtx ctx, Subst rhsSubst, Reporter reporter,
-    int lhsIx, int rhsIx, Term.Matching matching
-  ) {
-    if (rhsSubst.map().valuesView().allMatch(dom ->
-      dom instanceof RefTerm(var ref) && ctx.contains(ref))
-    ) reporter.report(new ClausesProblem.Domination(
-      lhsIx + 1, rhsIx + 1, matching.sourcePos()));
-  }
-
   private @NotNull MCT<Term, PatErr> classifySub(
     @NotNull SeqView<Term.Param> telescope,
     @NotNull ImmutableSeq<MCT.SubPats<Pat>> clauses,
diff --git a/base/src/main/java/org/aya/tyck/pat/YouTrack.java b/base/src/main/java/org/aya/tyck/pat/YouTrack.java
new file mode 100644
index 0000000000..c790470cb0
--- /dev/null
+++ b/base/src/main/java/org/aya/tyck/pat/YouTrack.java
@@ -0,0 +1,74 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.tyck.pat;
+
+import kala.collection.immutable.ImmutableSeq;
+import kala.tuple.Tuple;
+import kala.tuple.primitive.IntObjTuple2;
+import org.aya.core.pat.Pat;
+import org.aya.core.pat.PatUnify;
+import org.aya.core.term.ErrorTerm;
+import org.aya.core.term.MetaTerm;
+import org.aya.core.term.RefTerm;
+import org.aya.core.term.Term;
+import org.aya.core.visitor.DeltaExpander;
+import org.aya.core.visitor.Subst;
+import org.aya.tyck.ExprTycker;
+import org.aya.tyck.env.LocalCtx;
+import org.aya.tyck.error.UnifyInfo;
+import org.aya.util.Arg;
+import org.aya.util.error.SourcePos;
+import org.aya.util.tyck.MCT;
+import org.jetbrains.annotations.NotNull;
+
+/**
+ * YouTrack checks confluence.
+ *
+ * @author ice1000
+ * @see PatClassifier#classify
+ */
+public record YouTrack(
+  @NotNull ImmutableSeq<Term.Param> telescope,
+  @NotNull ExprTycker tycker, @NotNull SourcePos pos
+) {
+  private void unifyClauses(Term result, IntObjTuple2<Term.Matching> lhsInfo, IntObjTuple2<Term.Matching> rhsInfo) {
+    var lhsSubst = new Subst();
+    var rhsSubst = new Subst();
+    var ctx = PatUnify.unifyPat(
+      lhsInfo.component2().patterns().view().map(Arg::term),
+      rhsInfo.component2().patterns().view().map(Arg::term),
+      lhsSubst, rhsSubst, tycker.ctx.deriveMap());
+    domination(ctx, rhsSubst, lhsInfo.component1(), rhsInfo.component1(), rhsInfo.component2());
+    domination(ctx, lhsSubst, rhsInfo.component1(), lhsInfo.component1(), lhsInfo.component2());
+    var lhsTerm = lhsInfo.component2().body().subst(lhsSubst);
+    var rhsTerm = rhsInfo.component2().body().subst(rhsSubst);
+    // TODO: Currently all holes at this point are in an ErrorTerm
+    if (lhsTerm instanceof ErrorTerm error && error.description() instanceof MetaTerm hole) {
+      hole.ref().conditions.append(Tuple.of(lhsSubst, rhsTerm));
+    } else if (rhsTerm instanceof ErrorTerm error && error.description() instanceof MetaTerm hole) {
+      hole.ref().conditions.append(Tuple.of(rhsSubst, lhsTerm));
+    }
+    var resultSubst = DeltaExpander.buildSubst(telescope, Arg.mapSeq(lhsInfo.component2().patterns(), Pat::toTerm));
+    resultSubst.add(lhsSubst);
+    tycker.unifyReported(lhsTerm, rhsTerm, result.subst(resultSubst), pos, ctx, comparison ->
+      new ClausesProblem.Confluence(pos, rhsInfo.component1() + 1, lhsInfo.component1() + 1,
+        comparison, new UnifyInfo(tycker.state), rhsInfo.component2().sourcePos(), lhsInfo.component2().sourcePos()));
+  }
+
+  private void domination(LocalCtx ctx, Subst rhsSubst, int lhsIx, int rhsIx, Term.Matching matching) {
+    if (rhsSubst.map().valuesView().allMatch(dom ->
+      dom instanceof RefTerm(var ref) && ctx.contains(ref))
+    ) tycker.reporter.report(new ClausesProblem.Domination(
+      lhsIx + 1, rhsIx + 1, matching.sourcePos()));
+  }
+
+  public void check(@NotNull ClauseTycker.PatResult clauses, @NotNull MCT<Term, PatClassifier.PatErr> mct) {
+    mct.forEach(results -> {
+      var contents = results.contents()
+        .flatMap(i -> Pat.Preclause.lift(clauses.clauses().get(i))
+          .map(matching -> IntObjTuple2.of(i, matching)));
+      for (int i = 1, size = contents.size(); i < size; i++)
+        unifyClauses(clauses.result(), contents.get(i - 1), contents.get(i));
+    });
+  }
+}

From 6fa8442802d8b5a1e55809e1fc4df82fa673deb8 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 17:41:34 -0500
Subject: [PATCH 09/12] con: use correct `selfTele`, which is substituted by
 `mischa`

---
 base/src/main/java/org/aya/core/pat/PatToTerm.java        | 4 +---
 base/src/main/java/org/aya/core/term/ConCall.java         | 6 ++++--
 base/src/main/java/org/aya/tyck/pat/PatternTycker.java    | 2 +-
 base/src/main/java/org/aya/tyck/unify/TermComparator.java | 8 ++++----
 note/glossary.md                                          | 5 ++++-
 5 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/base/src/main/java/org/aya/core/pat/PatToTerm.java b/base/src/main/java/org/aya/core/pat/PatToTerm.java
index 9115e8a14b..cd9acdaf9c 100644
--- a/base/src/main/java/org/aya/core/pat/PatToTerm.java
+++ b/base/src/main/java/org/aya/core/pat/PatToTerm.java
@@ -32,8 +32,6 @@ public Term visit(@NotNull Pat pat) {
   protected @NotNull Term visitCtor(Pat.@NotNull Ctor ctor) {
     var data = (DataCall) ctor.type();
     var args = Arg.mapSeq(ctor.params(), this::visit);
-    return new ConCall(data.ref(), ctor.ref(),
-      data.args().map(Arg::implicitify),
-      data.ulift(), args);
+    return new ConCall(data.ref(), ctor.ref(), data.args(), data.ulift(), args);
   }
 }
diff --git a/base/src/main/java/org/aya/core/term/ConCall.java b/base/src/main/java/org/aya/core/term/ConCall.java
index 85b047b6e4..96e9ff85eb 100644
--- a/base/src/main/java/org/aya/core/term/ConCall.java
+++ b/base/src/main/java/org/aya/core/term/ConCall.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.core.term;
 
@@ -43,11 +43,13 @@ public ConCall(
   }
 
   @Override public @NotNull ImmutableSeq<Arg<@NotNull Term>> args() {
-    return head.dataArgs.view().concat(conArgs).toImmutableSeq();
+    return head.dataArgs.view().map(Arg::implicitify).concat(conArgs).toImmutableSeq();
   }
 
   /**
    * @param dataArgs the arguments to the data type, NOT the constructor patterns!!
+   *                 They need to be turned implicit when used as arguments.
+   * @see org.aya.tyck.pat.PatternTycker#mischa
    */
   public record Head(
     @NotNull DefVar<DataDef, TeleDecl.DataDecl> dataRef,
diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
index 453e322aa3..0fd779a00a 100644
--- a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
+++ b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
@@ -388,7 +388,7 @@ public static Result<Subst, Boolean> mischa(DataCall dataCall, CtorDef ctor, @No
     if (ctor.pats.isNotEmpty()) {
       return PatMatcher.tryBuildSubst(true, ctor.pats, dataCall.args(), new Expander.WHNFer(state));
     } else {
-      return kala.control.Result.ok(DeltaExpander.buildSubst(Def.defTele(dataCall.ref()), dataCall.args()));
+      return Result.ok(DeltaExpander.buildSubst(Def.defTele(dataCall.ref()), dataCall.args()));
     }
   }
 
diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
index c1b248683a..0a19ef23ab 100644
--- a/base/src/main/java/org/aya/tyck/unify/TermComparator.java
+++ b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -15,7 +15,6 @@
 import org.aya.core.def.PrimDef;
 import org.aya.core.term.*;
 import org.aya.core.visitor.AyaRestrSimplifier;
-import org.aya.core.visitor.DeltaExpander;
 import org.aya.core.visitor.Subst;
 import org.aya.generic.SortKind;
 import org.aya.generic.util.InternalException;
@@ -27,6 +26,7 @@
 import org.aya.ref.LocalVar;
 import org.aya.tyck.env.LocalCtx;
 import org.aya.tyck.error.LevelError;
+import org.aya.tyck.pat.PatternTycker;
 import org.aya.tyck.trace.Trace;
 import org.aya.tyck.tycker.MockTycker;
 import org.aya.tyck.tycker.TyckState;
@@ -534,12 +534,12 @@ case OutTerm(var lPhi, var pal, var lU) -> {
    */
   private @Nullable Term lossyUnifyCon(ConCall lhs, ConCall rhs, Sub lr, Sub rl, DefVar<CtorDef, TeleDecl.DataCtor> lef) {
     var retType = synthesizer().press(lhs);
-    var dataRef = lhs.head().dataRef();
+    var dataRef = lef.core.dataRef;
     if (Def.defResult(dataRef).isProp()) return retType;
     var dataAlgs = lhs.head().dataArgs();
     if (!visitArgs(dataAlgs, rhs.head().dataArgs(), lr, rl,
-      Term.Param.subst(Def.defTele(lef.core.dataRef), lhs.ulift()))) return null;
-    var ownerSubst = DeltaExpander.buildSubst(Def.defTele(dataRef), dataAlgs);
+      Term.Param.subst(Def.defTele(dataRef), lhs.ulift()))) return null;
+    var ownerSubst = PatternTycker.mischa(lhs.head().underlyingDataCall(), lef.core, state).get();
     if (visitArgs(lhs.conArgs(), rhs.conArgs(), lr, rl,
       Term.Param.subst(lef.core.selfTele, ownerSubst, lhs.ulift())))
       return retType;
diff --git a/note/glossary.md b/note/glossary.md
index e8219ee5cd..648b3cacf1 100644
--- a/note/glossary.md
+++ b/note/glossary.md
@@ -57,7 +57,10 @@ data Vec (n : Nat) (A : Type)
   对于非 simple indexed data types，它是 `dataTele`
 + `dataTele` -- 一个 data 的 telescope，对于 `Vec`，它是 `(n : Nat) (A : Type)`
 
-> 关于类似的 xxxArgs，也使用这种解释方式。
+> 关于类似的 `xxxArgs`，也使用这种解释方式。
+
++ `ConCall::dataArgs` 完全对应 `dataTele`，因此和 `ownerTele` 是不配对的（在非 indexed constructor 下是配对的，但是 indexed 的情况下，`ownerTele` 对应的是 pattern 而不是 `dataTele`）。在获取对应的 subst 的时候应该使用 `PatternTycker::mischa`。
++ `ConCall::conArgs` 完全对应 `selfTele`。
 
 ## 类型检查时用到的状态
 

From 92be27830fa7598a3a29582efee38b4c37a31a9c Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 17:53:37 -0500
Subject: [PATCH 10/12] subst: linked

---
 base/src/main/java/org/aya/core/visitor/Subst.java | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/base/src/main/java/org/aya/core/visitor/Subst.java b/base/src/main/java/org/aya/core/visitor/Subst.java
index 1f1ce7a1c8..49fd5c6604 100644
--- a/base/src/main/java/org/aya/core/visitor/Subst.java
+++ b/base/src/main/java/org/aya/core/visitor/Subst.java
@@ -1,21 +1,22 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.core.visitor;
 
 import kala.collection.SeqLike;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableHashMap;
+import kala.collection.mutable.MutableLinkedHashMap;
 import kala.collection.mutable.MutableMap;
 import kala.collection.mutable.MutableTreeMap;
 import org.aya.core.term.FormulaTerm;
 import org.aya.core.term.RefTerm;
 import org.aya.core.term.Term;
-import org.aya.prettier.BasePrettier;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.util.NormalizeMode;
 import org.aya.guest0x0.cubical.CofThy;
 import org.aya.guest0x0.cubical.Formula;
 import org.aya.guest0x0.cubical.Restr;
+import org.aya.prettier.BasePrettier;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.AnyVar;
 import org.aya.ref.LocalVar;
@@ -49,7 +50,7 @@ public Subst(@NotNull AnyVar var, @NotNull Term term) {
   }
 
   public Subst(@NotNull SeqLike<LocalVar> from, @NotNull SeqLike<? extends Term> to) {
-    this(MutableMap.from(from.zipView(to)));
+    this(MutableLinkedHashMap.from(from.zipView(to)));
   }
 
   public void subst(@NotNull Subst subst) {

From ef947332234082fdfae82c769eab91b17fd57b08 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 22:54:19 +0000
Subject: [PATCH 11/12] tests: add fixtures

---
 base/src/test/resources/failure/holes/issue747.aya.txt | 2 +-
 base/src/test/resources/success/src/Prop.aya           | 8 ++++++++
 2 files changed, 9 insertions(+), 1 deletion(-)

diff --git a/base/src/test/resources/failure/holes/issue747.aya.txt b/base/src/test/resources/failure/holes/issue747.aya.txt
index 1c62c2cba9..c6518135ef 100644
--- a/base/src/test/resources/failure/holes/issue747.aya.txt
+++ b/base/src/test/resources/failure/holes/issue747.aya.txt
@@ -11,7 +11,7 @@ Goal: Goal of type
       Context:
         {a : Nat}
       To ensure confluence:
-        Given (i ⇒ _), we should have: 0
+        Given (_ ⇒ 0, i ⇒ _), we should have: 0
 
 In file $FILE:11:13 ->
 
diff --git a/base/src/test/resources/success/src/Prop.aya b/base/src/test/resources/success/src/Prop.aya
index 3e9b66037e..380478f99e 100644
--- a/base/src/test/resources/success/src/Prop.aya
+++ b/base/src/test/resources/success/src/Prop.aya
@@ -1,3 +1,5 @@
+open import Paths
+
 open struct Squash (A: Type): Prop
   | value: A
 
@@ -9,3 +11,9 @@ def squashElim {A: Type} {P: Prop} (f: A -> P) (squash: Squash A): P => f squash
 def squash2Elim {A: Type} {P: Prop} (f: A -> P) (squash: Squash2 A): P
   | f, (squash a) => f a
 
+open data Carry (A : Prop) : Type
+| carry A
+
+open data Bool : Prop | true | false
+
+def check : carry true = carry false => idp

From 7c01dacfd2e06be70b94035b16480517e1a7acab Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Fri, 6 Jan 2023 19:32:41 -0500
Subject: [PATCH 12/12] subst: always use a linked map

---
 base/src/main/java/org/aya/core/visitor/Subst.java     | 2 +-
 base/src/test/resources/failure/holes/issue747.aya.txt | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/base/src/main/java/org/aya/core/visitor/Subst.java b/base/src/main/java/org/aya/core/visitor/Subst.java
index 49fd5c6604..9cedb76b47 100644
--- a/base/src/main/java/org/aya/core/visitor/Subst.java
+++ b/base/src/main/java/org/aya/core/visitor/Subst.java
@@ -42,7 +42,7 @@ public record Subst(
   }));
 
   public Subst() {
-    this(MutableMap.create());
+    this(MutableLinkedHashMap.of());
   }
 
   public Subst(@NotNull AnyVar var, @NotNull Term term) {
diff --git a/base/src/test/resources/failure/holes/issue747.aya.txt b/base/src/test/resources/failure/holes/issue747.aya.txt
index c6518135ef..c189d603ab 100644
--- a/base/src/test/resources/failure/holes/issue747.aya.txt
+++ b/base/src/test/resources/failure/holes/issue747.aya.txt
@@ -11,7 +11,7 @@ Goal: Goal of type
       Context:
         {a : Nat}
       To ensure confluence:
-        Given (_ ⇒ 0, i ⇒ _), we should have: 0
+        Given (i ⇒ _, _ ⇒ 0), we should have: 0
 
 In file $FILE:11:13 ->