diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index d6ac633a4..6428bcdfd 100644 --- 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 index 4fd23d7a3..4ed3d7f36 100644 --- 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 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 teleArgs) { - assert teleArgs.size() == telescopeSize(); - return result.instantiateTele(teleArgs.view()); - } + @Override public @NotNull Term result(Seq teleArgs) { return result.instantiateTele(teleArgs.view()); } @Override public @NotNull SeqView namesView() { return telescope.view().map(Param::name); }