cast: generate dummy terms

Co-authored-by: Hoshino Tented <[email protected]>

syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java

@@ -14,12 +14,12 @@ public sealed interface ClassDefLike extends AnyDef permits JitClass, ClassDef.D
 
   default @NotNull Term telescope(int i, @NotNull Seq<Term> restriction) {
     var member = members().get(i);
-    // Our code should not refer the subterm of [self], the only meaningful part is [self.forget()]
+    // Our code should not refer any out-of-scope field, the only meaningful part is [self.forget().take(i)]
     // Also, we don't use NewTerm, cause the type of the self-parameter is a class call without any restriction.
-    var self = new ClassCastTerm(this, ErrorTerm.DUMMY, ImmutableSeq.empty(),
-      restriction.view().take(i).map(Closure::mkConst).toImmutableSeq()
-    );
+    var implList = ImmutableSeq.fill(members().size(), idx ->
+      Closure.mkConst(idx < i ? restriction.get(idx) : ErrorTerm.DUMMY));
 
+    var self = new ClassCastTerm(this, ErrorTerm.DUMMY, ImmutableSeq.empty(), implList);
     return member.signature().inst(ImmutableSeq.of(self)).makePi(Seq.empty());
   }
 

syntax/src/main/java/org/aya/syntax/core/term/ClassCastTerm.java

@@ -24,8 +24,7 @@ public record ClassCastTerm(
   @NotNull ImmutableSeq<Closure> forget
 ) implements StableWHNF, Term {
   public ClassCastTerm {
-    // TODO: uncomment
-    // assert forget.isNotEmpty();
+    assert forget.isNotEmpty();
   }
 
   public @NotNull ClassCastTerm update(

syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java

@@ -27,10 +27,8 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
   }
 
   public static @NotNull Term make(
-    @NotNull ClassCall typeOfOf,
-    @NotNull Term of,
-    @NotNull MemberDefLike ref,
-    int ulift,
+    @NotNull ClassCall typeOfOf, @NotNull Term of,
+    @NotNull MemberDefLike ref, int ulift,
     @NotNull ImmutableSeq<@NotNull Term> args
   ) {
     var impl = typeOfOf.get(ref);