db-closeness: more annotation, and find some bugs

Author: HoshinoTented

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

@@ -15,13 +15,14 @@
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.core.Jdg;
+import org.aya.syntax.core.annotation.Closed;
 import org.aya.syntax.core.def.FnClauseBody;
 import org.aya.syntax.core.pat.Pat;
 import org.aya.syntax.core.pat.PatToTerm;
 import org.aya.syntax.core.term.*;
-import org.aya.syntax.ref.GenerateKind;
 import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.syntax.telescope.AbstractTele;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.TyckState;
 import org.aya.tyck.ctx.LocalLet;
@@ -68,26 +69,27 @@ public record TyckResult(@NotNull ImmutableSeq<Pat.Preclause<Term>> clauses, boo
     }
   }
 
-  /**
-   * @param result     the result according to the pattern tycking, the
-   *                   {@link DepTypeTerm.Unpi#params} is always empty if the signature result is
-   *                   {@link org.aya.tyck.pat.iter.Pusheenable.Const}
-   * @param paramSubst substitution for parameter, in the same ordeer as parameter.
-   *                   See {@link PatternTycker#paramSubst}. Only used by ExprTycker, see {@link #dumpLocalLetTo}
-   * @param freePats   a free version of the patterns, see {@link #freePats()}
-   * @param asSubst    substitution of the {@code as} patterns
-   * @implNote If there are fewer pats than parameters, there will be some pats inserted,
-   * but this will not affect {@code paramSubst}, and the inserted pat are "ignored" in tycking
-   * of the body, because we check the body against to {@link #result}.
-   * Then we apply the inserted pats to the body to complete it.
-   */
+  /// @param result     the result according to the pattern tycking, the
+  ///                                     [#params] is always empty if the signature result is
+  ///                                     [org.aya.tyck.pat.iter.Pusheenable.Const].
+  ///                                     The result is always [Closed] under [#localCtx]
+  /// @param paramSubst substitution for parameter, in the same ordeer as parameter.
+  ///                                     [Closed] under [#localCtx]
+  ///                                     Only used by ExprTycker, see [#dumpLocalLetTo]
+  /// @param freePats   free version of the patterns, [Closed] under [#localCtx()]
+  /// @param asSubst    substitution of the `as` patterns, [Closed] under [#localCtx]
+  /// @implNote TL;DR: `freePats.dropLast(unpiParamSize)` is compatible with [#localCtx], [#paramSubst], [#result] and [#body]
+  /// If there are fewer pats than parameters, there will be some pats inserted,
+  /// but this will not affect `paramSubst`, and the inserted pat are "ignored" in tycking
+  /// of the body, because we check the body against to [#result].
+  /// Then we apply the inserted pats to the body to complete it.
   public record LhsResult(
     @NotNull LocalCtx localCtx,
-    @NotNull Term result, int unpiParamSize,
-    @NotNull ImmutableSeq<Pat> freePats,
+    @NotNull @Closed Term result, int unpiParamSize,
+    @NotNull ImmutableSeq<@Closed Pat> freePats,
     @Override @NotNull SourcePos sourcePos,
     @Nullable WithPos<Expr> body,
-    @NotNull ImmutableSeq<Jdg> paramSubst,
+    @NotNull ImmutableSeq<@Closed Jdg> paramSubst,
     @NotNull LocalLet asSubst,
     boolean hasError
   ) implements SourceNode {
@@ -248,14 +250,14 @@ public record Worker(
 
       // fill missing patterns
       // This is not a typo of "repl"
-      var instRepi = sigIter.unpiBody().makePi().instTele(patResult.paramSubst().view().map(Jdg::wellTyped));
-      var instUnpiParam = DepTypeTerm.unpiUnsafe(instRepi, UnaryOperator.identity(), userUnpiSize);
-      var missingPats = instUnpiParam.params().mapIndexed((idx, x) ->
-        // It would be nice if we have a SourcePos here
-        new Pat.Bind(new LocalVar("unpi" + idx, SourcePos.NONE, GenerateKind.Basic.Tyck),
-          x.type()));
-
-      var wellTypedPats = patResult.wellTyped().appendedAll(missingPats);
+      @Closed var instRepi = sigIter.unpiBody().makePi()
+        // safe to inst, as paramSubst is closed
+        .instTele(patResult.paramSubst().view().map(Jdg::wellTyped));
+      var instUnpiParam = DepTypeTerm.unpiUnsafe(instRepi, userUnpiSize);
+      var freeParam = AbstractTele.enrich(new AbstractTele.Locns(instUnpiParam.params(), instUnpiParam.body()));
+      var missingPats = freeParam.map((x) -> new Pat.Bind(x.ref(), x.type()));
+
+      ImmutableSeq<@Closed Pat> wellTypedPats = patResult.wellTyped().appendedAll(missingPats);
       return new LhsResult(ctx, instRepi, userUnpiSize,
         wellTypedPats, clause.sourcePos, patIter.exprBody(),
         patResult.paramSubst(), patResult.asSubst(), patResult.hasError());
@@ -292,16 +294,18 @@ else if (result.hasError) {
         exprTycker.solveMetas();
         var zonkBody = zonker.zonk(rawCheckedBody);
 
+        // eta body with inserted patterns
+        // make before [Pat.collectVariables], as we need [pats] are [Closed].
+        @Closed var insertPatternBody = AppTerm.make(zonkBody, pats.view().takeLast(result.unpiParamSize).map(PatToTerm::visit));
+        var insertLetBody = makeLet(exprTycker.localLet(), insertPatternBody);
+
         // bind all pat bindings
-        var patWithTypeBound = Pat.collectVariables(result.freePats().view());
+        var patWithTypeBound = Pat.collectVariables(pats.view());
+        // now pats is Bound
         pats = patWithTypeBound.component2();
         var patBindTele = patWithTypeBound.component1();
 
         bindCount = patBindTele.size();
-
-        // eta body with inserted patterns
-        var insertPatternBody = AppTerm.make(zonkBody, pats.view().takeLast(result.unpiParamSize).map(PatToTerm::visit));
-        var insertLetBody = makeLet(exprTycker.localLet(), insertPatternBody);
         wellBody = insertLetBody.bindTele(patBindTele.view());
       }
 
@@ -371,7 +375,7 @@ public static void apply(@NotNull Pattern pat) {
   /// contain let bindings from real let expressions,
   ///
   /// @param term a free term
-  public static @NotNull Term makeLet(@NotNull LocalLet lets, @NotNull Term term) {
+  public static @NotNull Term makeLet(@NotNull LocalLet lets, @NotNull @Closed Term term) {
     // only one level
     return lets.let()
       .toSeq()

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

@@ -17,6 +17,8 @@
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.concrete.stmt.decl.DataDecl;
 import org.aya.syntax.core.Jdg;
+import org.aya.syntax.core.annotation.Bound;
+import org.aya.syntax.core.annotation.Closed;
 import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.pat.Pat;
 import org.aya.syntax.core.pat.PatMatcher;
@@ -59,10 +61,11 @@ public class PatternTycker implements Problematic, Stateful {
   /// [org.aya.syntax.core.term.LocalTerm])
   private final @NotNull SignatureIterator telescope;
 
-  /** Substitution for parameter, in the same order as parameter */
-  private final @NotNull MutableList<Jdg> paramSubst;
+  /// Substitution for parameter, in the same order as parameter
+  private final @NotNull MutableList<@Closed Jdg> paramSubst;
 
-  /// Substitution for `as` pattern
+  /// Substitution for `as` pattern.
+  /// Assertion: `asSubst.parent == null`
   private final @NotNull LocalLet asSubst;
 
   /// Almost equivalent to {@code telescope.peek()}, but we may instantiate it.
@@ -101,8 +104,8 @@ public PatternTycker(
   }
 
   public record TyckResult(
-    @NotNull ImmutableSeq<Pat> wellTyped,
-    @NotNull ImmutableSeq<Jdg> paramSubst,
+    @NotNull ImmutableSeq<@Closed Pat> wellTyped,
+    @NotNull ImmutableSeq<@Closed Jdg> paramSubst,
     @NotNull LocalLet asSubst,
     boolean hasError
   ) { }
@@ -114,7 +117,7 @@ public record TyckResult(
    * @param type    the type of {@param pattern}, it probably contains {@link MetaPatTerm}
    * @return a well-typed {@link Pat}, but still need to be inline!
    */
-  private @NotNull Pat doTyck(@NotNull WithPos<Pattern> pattern, @NotNull Term type) {
+  private @NotNull @Closed Pat doTyck(@NotNull WithPos<Pattern> pattern, @NotNull @Closed Term type) {
     return switch (pattern.data()) {
       case Pattern.Absurd _ -> {
         var selection = makeSureEmpty(type, pattern);
@@ -215,19 +218,19 @@ private void consumeParam() {
     telescope.next();
   }
 
-  private record FindNextParam(@NotNull ImmutableSeq<Pat> generated, @NotNull Kind kind) {
+  private record FindNextParam(@NotNull ImmutableSeq<@Closed Pat> generated, @NotNull Kind kind) {
     public enum Kind {
       Success, TooManyPattern, TooManyImplicit
     }
   }
 
-  /// Find next param until the predicate success
+  /// Find next param until the predicate success.
   ///
   /// @return (generated implicit patterns, status)
   /// @apiNote before call: {@link #currentParam} is the last checked parameter
   ///          after call: {@link #currentParam} is the first unchecked parameter which {@param until} success on
   private @NotNull FindNextParam findNextParam(@Nullable WithPos<Pattern> pattern, @NotNull Predicate<Param> until) {
-    var generatedPats = MutableList.<Pat>create();
+    var generatedPats = MutableList.<@Closed Pat>create();
 
     peekNextParam();
     // loop invariant: currentParam is the first unchecked parameter if not null
@@ -263,11 +266,12 @@ public enum Kind {
     @NotNull PatternIterator patterns,
     @Nullable WithPos<Pattern> outerPattern
   ) {
-    var wellTyped = MutableList.<Pat>create();
+    var wellTyped = MutableList.<@Closed Pat>create();
     // last user given pattern, that is, not aya generated
     @Nullable Arg<WithPos<Pattern>> lastPat = null;
 
     // loop invariant: [patterns] points to the last checked pattern, same for [telescope]
+    // "points to" means the last element it consumes holds the property.
     outer:
     while (patterns.hasNext()) {
       var currentPat = patterns.peek();
@@ -283,7 +287,7 @@ public enum Kind {
       var fnp = findNextParam(currentPat.term(), p ->
         p.explicit() == currentPat.explicit());
       // || telescope.isFromPusheen() == patterns.isFromPusheen()
-      // ^this check implies the first one
+      // ^this check is implied by the first one
 
       ImmutableSeq<Pat> generated = null;
 
@@ -312,8 +316,10 @@ public enum Kind {
         break;
       }
 
-      wellTyped.append(tyckPattern(currentPat.term()));
+      wellTyped.append(tyckPattern(currentPat.term()));   // tyckPattern consumes [currentParam] by move [telescope] forward
       patterns.next();    // consume pattern
+
+      // now: [patterns] points to the last checked pattern, same for [telescope]
     }
 
     // now: ! patterns.hasNext()
@@ -323,12 +329,18 @@ public enum Kind {
     // all not pusheen patterns have their parameters
 
     // is there any explicit parameters?
+    // this process also generate pattern for tailing implicit parameters
     var generated = findNextParam(null, p ->
       p.explicit() || telescope.isFromPusheen());
     // ^this check implies the first one
 
     // what kind of parameter you found?
     if (generated.kind == FindNextParam.Kind.Success && !telescope.isFromPusheen()) {
+      // [findNextParam] success means at least one parameter is peeked,
+      // thus `telescope.hasNext()` is true before the call to `findNextParam`.
+      // Therefore, now: ! patterns.hasNext(),
+      // other two cases are ruled out by `telescope.hasNext()` and `! telescope.isFromPusheen()`
+
       // no you can't!
       WithPos<Pattern> errorPattern = lastPat == null
         ? Objects.requireNonNull(outerPattern)
@@ -348,6 +360,7 @@ public enum Kind {
     return done(wellTyped);
   }
 
+  /// Must be called before using [#currentParam]
   private @NotNull Closer instCurrentParam() {
     currentParam = currentParam.descent(t -> t.instTele(paramSubst.view().map(Jdg::wellTyped)));
     return CLOSER;
@@ -361,18 +374,19 @@ private class Closer implements AutoCloseable {
   /**
    * Checking {@param pattern} with {@link PatternTycker#currentParam}
    */
-  private @NotNull Pat tyckPattern(@NotNull WithPos<Pattern> pattern) {
+  private @NotNull @Closed Pat tyckPattern(@NotNull WithPos<Pattern> pattern) {
     try (var _ = instCurrentParam()) {
       var result = doTyck(pattern, currentParam.type());
       addArgSubst(result, currentParam.type());
       return result;
     }
   }
 
-  private @NotNull Pat doGeneratePattern(@NotNull Term type, @NotNull String name, @NotNull SourcePos pos) {
+  private @NotNull @Closed Pat doGeneratePattern(@NotNull @Closed Term type, @NotNull String name, @NotNull SourcePos pos) {
     var freshVar = nameGen.bindName(name);
     if (exprTycker.whnf(type) instanceof DataCall dataCall) {
       // this pattern would be a Con, it can be inferred
+      // the db-closeness of Pat.Meta is determined by [dataCall], not its solution.
       return new Pat.Meta(MutableValue.create(), freshVar.name(), dataCall, pos);
     } else {
       // If the type is not a DataCall, then the only available pattern is Pat.Bind
@@ -386,7 +400,7 @@ private class Closer implements AutoCloseable {
    * we generate a MetaPat for each,
    * so that they can be inferred during {@link ClauseTycker}
    */
-  private @NotNull Pat generatePattern() {
+  private @NotNull @Closed Pat generatePattern() {
     try (var _ = instCurrentParam()) {
       // TODO: I NEED A SOURCE POS!!
       var pat = doGeneratePattern(currentParam.type(), currentParam.name(), SourcePos.NONE);
@@ -396,7 +410,7 @@ private class Closer implements AutoCloseable {
   }
 
   private @NotNull ImmutableSeq<Pat> tyckInner(
-    @NotNull ImmutableSeq<Param> telescope,
+    @NotNull ImmutableSeq<@Bound Param> telescope,
     @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns,
     @NotNull WithPos<Pattern> outerPattern
   ) {
@@ -407,25 +421,25 @@ private class Closer implements AutoCloseable {
     return tyckResult.wellTyped;
   }
 
-  private void addArgSubst(@NotNull Pat pattern, @NotNull Term type) {
+  private void addArgSubst(@NotNull @Closed Pat pattern, @NotNull @Closed Term type) {
     paramSubst.append(new Jdg.Default(PatToTerm.visit(pattern), type));
   }
 
-  private void addAsSubst(@NotNull LocalVar as, @NotNull Pat pattern, @NotNull Term type) {
+  private void addAsSubst(@NotNull LocalVar as, @NotNull Pat pattern, @NotNull @Closed Term type) {
     asSubst.put(as, new Jdg.Default(PatToTerm.visit(pattern), type), false);
   }
 
-  private @NotNull TyckResult done(@NotNull MutableList<Pat> wellTyped) {
+  private @NotNull TyckResult done(@NotNull MutableList<@Closed Pat> wellTyped) {
     return new TyckResult(wellTyped.toSeq(), paramSubst.toSeq(), asSubst, hasError);
   }
 
   private record Selection(
-    @NotNull DataCall data,
-    @NotNull ImmutableSeq<Term> ownerArgs,
-    @NotNull ConCallLike.Head conHead
+    @NotNull @Closed DataCall data,
+    @NotNull ImmutableSeq<@Closed Term> ownerArgs,
+    @NotNull ConCallLike.@Closed Head conHead
   ) { }
 
-  private @Nullable ConCallLike.Head makeSureEmpty(Term type, @NotNull WithPos<Pattern> pattern) {
+  private @Nullable ConCallLike.Head makeSureEmpty(@Closed Term type, @NotNull WithPos<Pattern> pattern) {
     if (!(exprTycker.whnf(type) instanceof DataCall dataCall)) {
       foundError(new PatternProblem.SplittingOnNonData(pattern, type));
       return null;
@@ -450,7 +464,7 @@ private record Selection(
     return null;
   }
 
-  private @Nullable Selection makeSureAvail(Term type, @NotNull ConDefLike name, @NotNull WithPos<Pattern> pattern) {
+  private @Nullable Selection makeSureAvail(@Closed Term type, @NotNull ConDefLike name, @NotNull WithPos<Pattern> pattern) {
     if (!(exprTycker.whnf(type) instanceof DataCall dataCall)) {
       foundError(new PatternProblem.SplittingOnNonData(pattern, type));
       return null;
@@ -462,8 +476,8 @@ private record Selection(
 
     return switch (checkAvail(dataCall, name, exprTycker.state)) {
       case Result.Ok(var subst) -> new Selection(
-        (DataCall) dataCall.instTeleFrom(name.selfTeleSize(), subst.view()),
-        subst, new ConCallLike.Head(name, dataCall.ulift(), subst));
+        dataCall, subst,
+        new ConCallLike.Head(name, dataCall.ulift(), subst));
       case Result.Err(_) -> {
         // Here, name != null, and is not in the list of checked body
         foundError(new PatternProblem.UnavailableCon(pattern, dataCall));
@@ -491,7 +505,7 @@ private record Selection(
    * Check whether {@param con} is available under {@param type}
    */
   public static @NotNull Result<ImmutableSeq<Term>, State> checkAvail(
-    @NotNull DataCall type, @NotNull ConDefLike con, @NotNull TyckState state
+    @NotNull @Closed DataCall type, @NotNull ConDefLike con, @NotNull TyckState state
   ) {
     return switch (con) {
       case JitCon jitCon -> jitCon.isAvailable(new Normalizer(state), type.args());
@@ -507,7 +521,7 @@ private record Selection(
     };
   }
 
-  private @NotNull Pat randomPat(Term param) {
+  private @NotNull Pat randomPat(@Closed Term param) {
     return new Pat.Bind(nameGen.bindName(param), param);
   }
 

base/src/main/java/org/aya/tyck/pat/iter/PiPusheen.java

@@ -3,14 +3,15 @@
 package org.aya.tyck.pat.iter;
 
 import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.core.annotation.Bound;
 import org.aya.syntax.core.term.DepTypeTerm;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
 import org.jetbrains.annotations.NotNull;
 
-public final class PiPusheen implements Pusheenable<Param, @NotNull Term> {
-  private final @NotNull ImmutableSeq<Param> unpi;
-  private final @NotNull Term result;
+public final class PiPusheen implements Pusheenable<@Bound Param, @NotNull @Bound Term> {
+  private final @NotNull ImmutableSeq<@Bound Param> unpi;
+  private final @NotNull @Bound Term result;
 
   // the index of next param
   private int pusheenIdx = 0;
@@ -20,17 +21,18 @@ public PiPusheen(@NotNull DepTypeTerm.Unpi unpi) {
     this.result = unpi.body();
   }
 
-  @Override public @NotNull Param peek() { return unpi.get(pusheenIdx); }
-  @Override public @NotNull Term body() {
+  @Override public @NotNull @Bound Param peek() { return unpi.get(pusheenIdx); }
+  @Override public @NotNull @Bound Term body() {
     return unpiBody().makePi();
   }
 
-  public @NotNull DepTypeTerm.Unpi unpiBody() {
+  /// Mostly [Bound], unless [#pusheenIdx] is 0 and the [org.aya.syntax.core.term.DepTypeTerm.Unpi] we use is closed.
+  public @NotNull @Bound DepTypeTerm.Unpi unpiBody() {
     return new DepTypeTerm.Unpi(unpi.sliceView(pusheenIdx, unpi.size()).toSeq(), result);
   }
 
   @Override public boolean hasNext() { return pusheenIdx < unpi.size(); }
-  @Override public @NotNull Param next() {
+  @Override public @NotNull @Bound Param next() {
     var result = peek();
     pusheenIdx += 1;
     return result;