Classes

base/src/main/java/org/aya/tyck/ExprTycker.java

@@ -47,6 +47,7 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.Comparator;
+import java.util.function.BiFunction;
 import java.util.function.Function;
 import java.util.function.Supplier;
 
@@ -134,6 +135,11 @@ case PiTerm(var dom, var cod) -> {
     };
   }
 
+  /**
+   * @param type   expected type
+   * @param result wellTyped + actual type from synthesize
+   * @param expr   original expr, used for error reporting
+   */
   private @NotNull Jdg inheritFallbackUnify(@NotNull Term type, @NotNull Jdg result, @NotNull WithPos<Expr> expr) {
     type = whnf(type);
     var resultType = result.type();
@@ -155,6 +161,22 @@ case PiTerm(var dom, var cod) -> {
         return new Jdg.Default(new LamTerm(closure), eq);
       }
     }
+    // Try coercive subtyping between classes
+    if (type instanceof ClassCall clazz) {
+      // Try coercive subtyping for `SomeClass (foo := 114514)` into `SomeClass`
+      resultType = whnf(resultType);
+      if (resultType instanceof ClassCall resultClazz) {
+        // TODO: check whether resultClazz <: clazz
+        if (true) {
+          // No need to coerce
+          if (clazz.args().size() == resultClazz.args().size()) return result;
+          var forget = resultClazz.args().drop(clazz.args().size());
+          return new Jdg.Default(new ClassCastTerm(clazz.ref(), result.wellTyped(), clazz.args(), forget), type);
+        } else {
+          return makeErrorResult(type, result);
+        }
+      }
+    }
     if (unifyTyReported(type, resultType, expr)) return result;
     return makeErrorResult(type, result);
   }
@@ -315,6 +337,19 @@ yield subscoped(param.ref(), wellParam, () ->
         var type = new DataCall(def, 0, ImmutableSeq.of(elementTy));
         yield new Jdg.Default(new ListTerm(results, match.recog(), type), type);
       }
+      case Expr.New(var classCall) -> {
+        var wellTyped = synthesize(classCall);
+        if (!(wellTyped.wellTyped() instanceof ClassCall call)) {
+          yield fail(expr.data(), new ClassError.NotClassCall(classCall));
+        }
+
+        // check whether the call is fully applied
+        if (call.args().size() != call.ref().members().size()) {
+          yield fail(expr.data(), new ClassError.NotFullyApplied(classCall));
+        }
+
+        yield new Jdg.Default(new NewTerm(call), call);
+      }
       case Expr.Unresolved _ -> Panic.unreachable();
       default -> fail(expr.data(), new NoRuleError(expr, null));
     };
@@ -342,9 +377,9 @@ yield subscoped(param.ref(), wellParam, () ->
       case LocalVar ref when localLet.contains(ref) -> generateApplication(args, localLet.get(ref)).lift(lift);
       case LocalVar lVar -> generateApplication(args,
         new Jdg.Default(new FreeTerm(lVar), localCtx().get(lVar))).lift(lift);
-      case CompiledVar(var content) -> new AppTycker<>(state, sourcePos, args.size(), lift, (params, k) ->
+      case CompiledVar(var content) -> new AppTycker<>(this, sourcePos, args.size(), lift, (params, k) ->
         computeArgs(sourcePos, args, params, k)).checkCompiledApplication(content);
-      case DefVar<?, ?> defVar -> new AppTycker<>(state, sourcePos, args.size(), lift, (params, k) ->
+      case DefVar<?, ?> defVar -> new AppTycker<>(this, sourcePos, args.size(), lift, (params, k) ->
         computeArgs(sourcePos, args, params, k)).checkDefApplication(defVar);
       default -> throw new UnsupportedOperationException("TODO");
     };
@@ -359,10 +394,11 @@ case CompiledVar(var content) -> new AppTycker<>(state, sourcePos, args.size(),
 
   private Jdg computeArgs(
     @NotNull SourcePos pos, @NotNull ImmutableSeq<Expr.NamedArg> args,
-    @NotNull AbstractTele params, @NotNull Function<Term[], Jdg> k
+    @NotNull AbstractTele params, @NotNull BiFunction<Term[], Term, Jdg> k
   ) throws NotPi {
     int argIx = 0, paramIx = 0;
     var result = new Term[params.telescopeSize()];
+    Term firstType = null;
     while (argIx < args.size() && paramIx < params.telescopeSize()) {
       var arg = args.get(argIx);
       var param = params.telescopeRich(paramIx, result);
@@ -373,33 +409,39 @@ private Jdg computeArgs(
           break;
         } else if (arg.name() == null) {
           // here, arg.explicit() == true and param.explicit() == false
+          if (paramIx == 0) firstType = param.type();
           result[paramIx++] = insertImplicit(param, arg.sourcePos());
           continue;
         }
       }
       if (arg.name() != null && !param.nameEq(arg.name())) {
+        if (paramIx == 0) firstType = param.type();
         result[paramIx++] = insertImplicit(param, arg.sourcePos());
         continue;
       }
-      result[paramIx++] = inherit(arg.arg(), param.type()).wellTyped();
+      var what = inherit(arg.arg(), param.type());
+      if (paramIx == 0) firstType = param.type();
+      result[paramIx++] = what.wellTyped();
       argIx++;
     }
     // Trailing implicits
     while (paramIx < params.telescopeSize()) {
       if (params.telescopeLicit(paramIx)) break;
       var param = params.telescopeRich(paramIx, result);
+      if (paramIx == 0) firstType = param.type();
       result[paramIx++] = insertImplicit(param, pos);
     }
     var extraParams = MutableStack.<Pair<LocalVar, Term>>create();
     if (argIx < args.size()) {
-      return generateApplication(args.drop(argIx), k.apply(result));
+      return generateApplication(args.drop(argIx), k.apply(result, firstType));
     } else while (paramIx < params.telescopeSize()) {
       var param = params.telescopeRich(paramIx, result);
       var atarashiVar = LocalVar.generate(param.name());
       extraParams.push(new Pair<>(atarashiVar, param.type()));
+      if (paramIx == 0) firstType = param.type();
       result[paramIx++] = new FreeTerm(atarashiVar);
     }
-    var generated = k.apply(result);
+    var generated = k.apply(result, firstType);
     while (extraParams.isNotEmpty()) {
       var pair = extraParams.pop();
       generated = new Jdg.Default(

base/src/main/java/org/aya/tyck/StmtTycker.java

@@ -173,7 +173,7 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker
         new Param("self", classCall, false),
         classRef.concrete.sourcePos()
       );
-    new MemberDef(classRef, member.ref, signature.params(), signature.result());
+    new MemberDef(classRef, member.ref, classRef.concrete.members.indexOf(member), signature.params(), signature.result());
     member.ref.signature = signature;
   }
 

base/src/main/java/org/aya/tyck/error/ClassError.java

@@ -0,0 +1,28 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.tyck.error;
+
+import org.aya.pretty.doc.Doc;
+import org.aya.syntax.concrete.Expr;
+import org.aya.util.error.SourcePos;
+import org.aya.util.error.WithPos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public interface ClassError extends TyckError {
+  @NotNull WithPos<Expr> problemExpr();
+
+  @Override default @NotNull SourcePos sourcePos() { return problemExpr().sourcePos(); }
+
+  record NotClassCall(@Override @NotNull WithPos<Expr> problemExpr) implements ClassError {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.english("Unable to new a non-class type:"), Doc.code(problemExpr.data().toDoc(options)));
+    }
+  }
+
+  record NotFullyApplied(@Override @NotNull WithPos<Expr> problemExpr) implements ClassError {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.english("Unable to new an incomplete class type:"), Doc.code(problemExpr.data().toDoc(options)));
+    }
+  }
+}

base/src/main/java/org/aya/tyck/tycker/AppTycker.java

@@ -5,34 +5,39 @@
 import kala.collection.Seq;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableArray;
+import kala.collection.immutable.ImmutableSeq;
 import kala.function.CheckedBiFunction;
 import org.aya.generic.stmt.Shaped;
 import org.aya.syntax.compile.JitCon;
 import org.aya.syntax.compile.JitData;
 import org.aya.syntax.compile.JitFn;
 import org.aya.syntax.compile.JitPrim;
 import org.aya.syntax.concrete.stmt.decl.*;
+import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.repr.AyaShape;
-import org.aya.syntax.core.term.FreeTerm;
-import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.*;
 import org.aya.syntax.core.term.call.*;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.telescope.AbstractTele;
 import org.aya.tyck.Jdg;
 import org.aya.tyck.TyckState;
+import org.aya.unify.Synthesizer;
 import org.aya.util.error.Panic;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.function.Function;
+import java.util.function.BiFunction;
 
 public record AppTycker<Ex extends Exception>(
-  @NotNull TyckState state, @NotNull SourcePos pos,
-  int argsCount, int lift, @NotNull Factory<Ex> makeArgs
-) {
+  @Override @NotNull TyckState state,
+  @NotNull AbstractTycker tycker,
+  @NotNull SourcePos pos,
+  int argsCount, int lift,
+  @NotNull Factory<Ex> makeArgs
+) implements Stateful {
   /**
    * <pre>
    * Signature (0th param) --------> Argument Parser (this interface)
@@ -45,7 +50,14 @@ public record AppTycker<Ex extends Exception>(
    */
   @FunctionalInterface
   public interface Factory<Ex extends Exception> extends
-    CheckedBiFunction<AbstractTele, Function<Term[], Jdg>, Jdg, Ex> {
+    CheckedBiFunction<AbstractTele, BiFunction<Term[], Term, Jdg>, Jdg, Ex> {
+  }
+
+  public AppTycker(
+    @NotNull AbstractTycker tycker, @NotNull SourcePos pos,
+    int argsCount, int lift, @NotNull Factory<Ex> makeArgs
+  ) {
+    this(tycker.state, tycker, pos, argsCount, lift, makeArgs);
   }
 
   public @NotNull Jdg checkCompiledApplication(@NotNull AbstractTele def) throws Ex {
@@ -93,7 +105,7 @@ public interface Factory<Ex extends Exception> extends
     // ownerTele + selfTele
     var fullSignature = conVar.signature().lift(lift);
 
-    return makeArgs.applyChecked(fullSignature, args -> {
+    return makeArgs.applyChecked(fullSignature, (args, _) -> {
       var realArgs = ImmutableArray.from(args);
       var ownerArgs = realArgs.take(conVar.ownerTeleSize());
       var conArgs = realArgs.drop(conVar.ownerTeleSize());
@@ -109,14 +121,14 @@ public interface Factory<Ex extends Exception> extends
   }
   private @NotNull Jdg checkPrimCall(@NotNull PrimDefLike primVar) throws Ex {
     var signature = primVar.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> new Jdg.Default(
+    return makeArgs.applyChecked(signature, (args, _) -> new Jdg.Default(
       state.primFactory.unfold(new PrimCall(primVar, 0, ImmutableArray.from(args)), state),
       signature.result(args)
     ));
   }
   private @NotNull Jdg checkDataCall(@NotNull DataDefLike data) throws Ex {
     var signature = data.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> new Jdg.Default(
+    return makeArgs.applyChecked(signature, (args, _) -> new Jdg.Default(
       new DataCall(data, 0, ImmutableArray.from(args)),
       signature.result(args)
     ));
@@ -125,7 +137,7 @@ public interface Factory<Ex extends Exception> extends
     @NotNull FnDefLike fnDef, @Nullable Shaped.Applicable<FnDefLike> operator
   ) throws Ex {
     var signature = fnDef.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> {
+    return makeArgs.applyChecked(signature, (args, _) -> {
       var argsSeq = ImmutableArray.from(args);
       var result = signature.result(args);
       if (operator != null) {
@@ -137,10 +149,10 @@ public interface Factory<Ex extends Exception> extends
   }
 
   private @NotNull Jdg checkClassCall(@NotNull ClassDefLike clazz) throws Ex {
-    var appliedParams = ofClassMembers(clazz, argsCount).lift(lift);
     var self = LocalVar.generate("self");
+    var appliedParams = ofClassMembers(self, clazz, argsCount).lift(lift);
     state.classThis.push(self);
-    var result = makeArgs.applyChecked(appliedParams, args -> new Jdg.Default(
+    var result = makeArgs.applyChecked(appliedParams, (args, _) -> new Jdg.Default(
       new ClassCall(clazz, 0, ImmutableArray.from(args).map(x -> x.bind(self))),
       appliedParams.result(args)
     ));
@@ -150,23 +162,29 @@ public interface Factory<Ex extends Exception> extends
 
   private @NotNull Jdg checkProjCall(@NotNull MemberDefLike member) throws Ex {
     var signature = member.signature().lift(lift);
-    return makeArgs.applyChecked(signature, args -> {
+    return makeArgs.applyChecked(signature, (args, fstTy) -> {
       assert args.length >= 1;
+      var ofTy = whnf(fstTy);
+      if (!(ofTy instanceof ClassCall classTy)) throw new UnsupportedOperationException("report");   // TODO
       var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]);
       return new Jdg.Default(
-        new MemberCall(args[0], member, 0, fieldArgs),
+        MemberCall.make(classTy, args[0], member, 0, fieldArgs),
         signature.result(args)
       );
     });
   }
 
-  static @NotNull AbstractTele ofClassMembers(@NotNull ClassDefLike def, int memberCount) {
+  private @NotNull AbstractTele ofClassMembers(@NotNull LocalVar self, @NotNull ClassDefLike def, int memberCount) {
+    var synthesizer = new Synthesizer(tycker);
     return switch (def) {
-      case ClassDef.Delegate delegate -> new TakeMembers(delegate.core(), memberCount);
+      case ClassDef.Delegate delegate -> new TakeMembers(self, delegate.core(), memberCount, synthesizer);
     };
   }
 
-  record TakeMembers(@NotNull ClassDef clazz, @Override int telescopeSize) implements AbstractTele {
+  record TakeMembers(
+    @NotNull LocalVar self, @NotNull ClassDef clazz,
+    @Override int telescopeSize, @NotNull Synthesizer synthesizer
+  ) implements AbstractTele {
     @Override public boolean telescopeLicit(int i) { return true; }
     @Override public @NotNull String telescopeName(int i) {
       assert i < telescopeSize;
@@ -175,18 +193,26 @@ record TakeMembers(@NotNull ClassDef clazz, @Override int telescopeSize) impleme
 
     // class Foo
     // | foo : A
-    // | + : A -> A -> A
+    // | infix + : A -> A -> A
     // | bar : Fn (x : Foo A) -> (x.foo) self.+ (self.foo)
     //                  instantiate these!   ^       ^
     @Override public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
       // teleArgs are former members
       assert i < telescopeSize;
       var member = clazz.members().get(i);
-      return TyckDef.defSignature(member.ref()).makePi(Seq.of(new FreeTerm(clazz.ref().concrete.self)));
+      return TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new NewTerm(
+        new ClassCall(new ClassDef.Delegate(clazz.ref()), 0,
+          ImmutableSeq.fill(clazz.members().size(), idx -> Closure.mkConst(idx < i ? teleArgs.get(idx) : ErrorTerm.DUMMY))
+        )
+      ))).makePi(Seq.empty());
     }
+
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
-      // Use SigmaTerm::lub
-      throw new UnsupportedOperationException("TODO");
+      return clazz.members().view()
+        .drop(telescopeSize)
+        .map(member -> TyckDef.defSignature(member.ref()).inst(ImmutableSeq.of(new FreeTerm(self))).makePi(Seq.empty()))
+        .map(ty -> (SortTerm) synthesizer.synth(ty))
+        .foldLeft(SortTerm.Type0, SigmaTerm::lub);
     }
     @Override public @NotNull SeqView<String> namesView() {
       return clazz.members().sliceView(0, telescopeSize).map(i -> i.ref().name());

base/src/main/java/org/aya/unify/Synthesizer.java

@@ -136,6 +136,8 @@
       case MetaLitTerm mlt -> mlt.type();
       case StringTerm str -> state().primFactory.getCall(PrimDef.ID.STRING);
       case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
+      case NewTerm newTerm -> newTerm.inner();
+      case ClassCastTerm castTerm -> new ClassCall(castTerm.ref(), 0, castTerm.remember());
     };
   }