tyck: remove the incorrect assertion

aya-prover · Jun 19, 2024 · 6d1ead2 · 6d1ead2
1 parent 0924102
commit 6d1ead2
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -164,6 +164,7 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker
     signature = signature.pusheen(tycker::whnf)
       .descent(tycker::zonk)
       .bindTele(SeqView.of(tycker.state.classThis.pop()));
+    // TODO: prepend {this: Class} to the telescope
     new MemberDef(classRef, member.ref, signature.rawParams(), signature.result());
     member.ref.signature = signature;
   }

diff --git a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java
@@ -106,10 +106,7 @@ record Locns(@NotNull ImmutableSeq<Param> telescope, @NotNull Term result) imple
       // TODO: +1 on this
       return telescope.get(i).type().instantiateTele(teleArgs.sliceView(0, i));
     }
-    @Override public @NotNull Term result(Seq<Term> teleArgs) {
-      assert teleArgs.size() == telescopeSize();
-      return result.instantiateTele(teleArgs.view());
-    }
+    @Override public @NotNull Term result(Seq<Term> teleArgs) { return result.instantiateTele(teleArgs.view()); }
     @Override public @NotNull SeqView<String> namesView() {
       return telescope.view().map(Param::name);
     }