No More Duplicated Vars

[HoshinoTented]

There are some problems because of the duplicated vars, why don't we just add an assertion and save our time?

[HoshinoTented]

Maybe we should solve all the duplicated vars problems and then merge this...

[ice1000]

I just realized something. You have GlobalConfig and tests will enable it

[ice1000]

I have a lot of other tests/sanity checks that I want to add. I believe we should have a general mechanism for that.

Maybe tracing should be part of this config

[ice1000]

There are already some limited scope checks. There can be more.

[ice1000]

I have fixed some problems caused by duplicated vars. There are more, but I would love to merge these changes and have another PR that enables the assertion back and we'll see what we can do in the future.

What do you think? @HoshinoTented

[ice1000]

bors r+

Tests passed locally.

[codecov]

Codecov Report

Merging #665 (562d076) into main (7c01dac) will increase coverage by 0.01%.
The diff coverage is 54.54%.

@@             Coverage Diff              @@
##               main     #665      +/-   ##
============================================
+ Coverage     82.15%   82.17%   +0.01%     
  Complexity     3383     3383              
============================================
  Files           288      288              
  Lines         10537    10534       -3     
  Branches       1259     1258       -1     
============================================
- Hits           8657     8656       -1     
+ Misses         1168     1166       -2     
  Partials        712      712              

Impacted Files	Coverage Δ
...se/src/main/java/org/aya/tyck/env/MapLocalCtx.java	100.00% <ø> (ø)
...se/src/main/java/org/aya/tyck/env/SeqLocalCtx.java	78.57% <ø> (+5.23%)	⬆️
base/src/main/java/org/aya/tyck/env/LocalCtx.java	73.84% <54.54%> (+1.11%)	⬆️

Help us with your feedback. Take ten seconds to tell us how you rate us. Have a feature suggestion? Share it here.

[bors]

Build succeeded:

• commit-check
• gradle-check

[ice1000]

What I've done locally:

diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index 4010646a4..8fc19b804 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -108,34 +108,39 @@ public final class StmtTycker extends TracedTycker {
       case TeleDecl.DataDecl decl -> {
         var signature = decl.signature;
         assert signature != null;
-        var body = decl.body.map(clause -> (CtorDef) tyck(clause, tycker));
+        var body = decl.body.map(clause -> traced(clause, tycker, this::checkCtor));
         yield new DataDef(decl.ref, signature.param(), signature.result(), body);
       }
       case TeleDecl.PrimDecl decl -> decl.ref.core;
       case TeleDecl.StructDecl decl -> {
         var signature = decl.signature;
         assert signature != null;
-        var body = decl.fields.map(field -> (FieldDef) tyck(field, tycker));
+        var body = decl.fields.map(field -> traced(field, tycker, (f, e) ->
+          checkField(f, e, false)));
         yield new StructDef(decl.ref, signature.param(), signature.result(), body);
       }
       // Do nothing, data constructors is just a header.
       case TeleDecl.DataCtor ctor -> ctor.ref.core;
-      case TeleDecl.StructField field -> {
-        // TODO[ice]: remove this hack
-        if (field.ref.core != null) yield field.ref.core;
-        var signature = field.signature;
-        assert signature != null; // already handled in the entrance of this method
-        var structRef = field.structRef;
-        var structSig = structRef.concrete.signature;
-        assert structSig != null;
-        loadTele(tycker, structSig);
-        var result = signature.result();
-        var body = field.body.map(e -> tycker.inherit(e, result).wellTyped());
-        yield new FieldDef(structRef, field.ref, structSig.param(), signature.param(), result, body, field.coerce);
-      }
+      case TeleDecl.StructField field -> checkField(field, tycker, true);
     };
   }

+  private @NotNull FieldDef checkField(TeleDecl.StructField field, @NotNull ExprTycker tycker, boolean load) {
+    // TODO[ice]: remove this hack
+    if (field.ref.core != null) return field.ref.core;
+    var structRef = field.structRef;
+    var structSig = structRef.concrete.signature;
+    assert structSig != null;
+    // tyckHeader implies loadTele
+    if (field.signature == null) tyckHeader(field, tycker);
+    else if (load) loadTele(tycker, structSig);
+    var signature = field.signature;
+    assert signature != null;
+    var result = signature.result();
+    var body = field.body.map(e -> tycker.inherit(e, result).wellTyped());
+    return new FieldDef(structRef, field.ref, structSig.param(), signature.param(), result, body, field.coerce);
+  }
+
   // Apply a simple checking strategy for maximal metavar inference.
   public @NotNull FnDef simpleFn(@NotNull ExprTycker tycker, TeleDecl.FnDecl fn) {
     return traced(fn, tycker, this::doSimpleFn);
@@ -223,7 +228,7 @@ public final class StmtTycker extends TracedTycker {
         tycker.solveMetas();
         tycker.ctx = new SeqLocalCtx();
       }
-      case TeleDecl.DataCtor ctor -> checkCtor(tycker, ctor);
+      case TeleDecl.DataCtor ctor -> checkCtor(ctor, tycker);
       case TeleDecl.StructField field -> {
         if (field.signature != null) break;
         var structRef = field.structRef;
@@ -239,9 +244,13 @@ public final class StmtTycker extends TracedTycker {
     tracing(TreeBuilder::reduce);
   }

-  /** Extracted for the extreme complexity. */
-  private void checkCtor(@NotNull ExprTycker tycker, TeleDecl.DataCtor ctor) {
-    if (ctor.ref.core != null) return;
+  /**
+   * Extracted for the extreme complexity.
+   *
+   * @return
+   */
+  private @NotNull CtorDef checkCtor(TeleDecl.DataCtor ctor, @NotNull ExprTycker tycker) {
+    if (ctor.ref.core != null) return ctor.ref.core;
     var dataRef = ctor.dataRef;
     var dataConcrete = dataRef.concrete;
     var dataSig = dataConcrete.signature;
@@ -305,7 +314,9 @@ public final class StmtTycker extends TracedTycker {
       reporter.report(new CubicalError.PathConDominateError(ctor.clauses.sourcePos()));
       elabClauses = PartialTerm.DUMMY_SPLIT;
     }
-    dataConcrete.checkedBody.append(new CtorDef(dataRef, ctor.ref, pat, patternTele, tele, split, dataCall, ctor.coerce));
+    var def = new CtorDef(dataRef, ctor.ref, pat, patternTele, tele, split, dataCall, ctor.coerce);
+    dataConcrete.checkedBody.append(def);
+    return def;
   }

   private static void loadTele(@NotNull ExprTycker tycker, Def.Signature<?> dataSig) {

[ice1000]

It still doesn't work, but it is anyway an attempt to fix record fields being type checked in a messy order. A record field tyck can happen when:

• Record body is being checked
• Record field header is being checked before record body being checked
• Record field body is being checked before header being checked
• Record field body is being checked after header is already checked in another call to doTyck

...

I don't think it worth fixing because we're going to overhaul records as classes anyway...

[ice1000]

perfect!