merge: #875

875: Irrelevance of `Prop` WIP r=ice1000 a=ice1000

#866 

Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>

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;
   }

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);
   }
 }

base/src/main/java/org/aya/core/pat/PatUnify.java

@@ -1,13 +1,13 @@
-// 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.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 +18,7 @@
  * The unification of patterns. This is <strong>not</strong> pattern unification.
  *
  * @author ice1000
- * @see PatUnify#unifyPat(SeqLike, SeqLike, 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) {
@@ -108,8 +108,8 @@ 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 SeqView<Pat> lpats,
+    @NotNull SeqView<Pat> rpats,
     @NotNull Subst lhsSubst,
     @NotNull Subst rhsSubst,
     @NotNull LocalCtx ctx

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,

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);

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) {

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;
@@ -41,15 +42,15 @@ public record Subst(
   }));
 
   public Subst() {
-    this(MutableMap.create());
+    this(MutableLinkedHashMap.of());
   }
 
   public Subst(@NotNull AnyVar var, @NotNull Term term) {
     this(MutableHashMap.of(var, 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) {

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(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);
               }

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;
 
@@ -11,14 +11,15 @@
 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;
 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 +34,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);
@@ -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, args);
+      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));
     });

base/src/main/java/org/aya/tyck/pat/PatClassifier.java

@@ -6,22 +6,14 @@
 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;
 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;
@@ -90,50 +82,6 @@ public static int[] firstMatchDomination(
     return numbers;
   }
 
-  public static void confluence(
-    @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(MutableMap.create());
-        var rhsSubst = new Subst(MutableMap.create());
-        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());
-        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,

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()));
     }
   }