WIP: Copy Covariance from Arend(

base/src/main/java/module-info.java

@@ -42,4 +42,5 @@
   exports org.aya.tyck.trace;
   exports org.aya.tyck.unify;
   exports org.aya.tyck;
+    exports org.aya.tyck.covariance;
 }

base/src/main/java/org/aya/concrete/stmt/TeleDecl.java

@@ -3,6 +3,8 @@
 package org.aya.concrete.stmt;
 
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.mutable.MutableAnySet;
+import kala.collection.mutable.MutableHashSet;
 import kala.collection.mutable.MutableList;
 import kala.control.Either;
 import kala.control.Option;
@@ -13,6 +15,7 @@
 import org.aya.core.term.SortTerm;
 import org.aya.core.term.Term;
 import org.aya.generic.Modifier;
+import org.aya.generic.util.InternalException;
 import org.aya.ref.DefVar;
 import org.aya.resolve.context.Context;
 import org.aya.util.Arg;
@@ -183,6 +186,7 @@ public static final class DataDecl extends TeleDecl<SortTerm> {
     public final @NotNull ImmutableSeq<DataCtor> body;
     /** Yet type-checked constructors */
     public final @NotNull MutableList<@NotNull CtorDef> checkedBody = MutableList.create();
+    private final @NotNull MutableHashSet<@NotNull Integer> covariant = MutableHashSet.create();
 
     public DataDecl(
       @NotNull SourcePos sourcePos, @NotNull SourcePos entireSourcePos,
@@ -204,6 +208,19 @@ public DataDecl(
     @Override public @NotNull DefVar<DataDef, DataDecl> ref() {
       return this.ref;
     }
+
+    public boolean isCovariant(int i) {
+      return covariant.contains(i);
+    }
+
+    public void setCovariant(int i) {
+      setCovariant(i, true);
+    }
+
+    public void setCovariant(int i, boolean covariant) {
+      if (covariant) this.covariant.add(i);
+      else this.covariant.remove(i);
+    }
   }
 
   /**
@@ -236,6 +253,11 @@ public StructDecl(
     @Override public @NotNull DefVar<StructDef, StructDecl> ref() {
       return ref;
     }
+
+    public boolean isCovariantField(StructField field) {
+      assert field.structRef == ref;
+      return field.covariant;
+    }
   }
 
   public static final class StructField
@@ -245,6 +267,7 @@ public static final class StructField
     public @NotNull Expr result;
     public @NotNull Option<Expr> body;
     public final boolean coerce;
+    public boolean covariant = false;
 
     // will change after resolve
     public @NotNull ImmutableSeq<Expr.Param> telescope;

base/src/main/java/org/aya/tyck/covariance/CovarianceChecker.java

@@ -0,0 +1,115 @@
+// Copyright (c) 2020-2022 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.covariance;
+
+import org.aya.core.term.*;
+import org.aya.generic.util.NormalizeMode;
+import org.aya.tyck.tycker.TyckState;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public sealed abstract class CovarianceChecker permits ParametersCovarianceChecker, RecursiveDataChecker {
+  protected final @NotNull TyckState state;
+
+  public CovarianceChecker(@NotNull TyckState state) {
+    this.state = state;
+  }
+
+  protected boolean allowData() {
+    return true;
+  }
+
+  protected abstract boolean checkNonCovariant(@NotNull Term term);
+
+  protected boolean checkOtherwise(@NotNull Term term) {
+    return checkNonCovariant(term);
+  }
+
+  protected boolean checkLevels(@NotNull SortTerm levels, @Nullable Callable.DefCall defCall) {
+    return false;
+  }
+
+  protected boolean checkLevels(int levels, @NotNull Callable.DefCall defCall) {
+    return false;
+  }
+
+  private boolean checkConstructor(@NotNull Term term) {
+    return switch (term.normalize(state, NormalizeMode.WHNF)) {
+      case LamTerm lam -> checkConstructor(lam.body());
+      case TupTerm tup -> {
+        for (var item : tup.items()) {
+          if (checkConstructor(item.term())) {
+            yield true;
+          }
+        }
+        yield false;
+      }
+      case ConCall conCall -> {
+        for (var argument : conCall.conArgs()) {
+          if (checkConstructor(argument.term())) {
+            yield true;
+          }
+        }
+        yield false;
+      }
+      case NewTerm newTerm -> {
+        for (var field : newTerm.params().keysView()) {
+          assert field.concrete.signature() != null;
+          if (checkConstructor(field.concrete.signature().result())) {
+            yield true;
+          }
+        }
+        yield false;
+      }
+      case default -> check(term);
+    };
+  }
+
+  public boolean check(@NotNull Term term) {
+    return switch (term.normalize(state, NormalizeMode.WHNF)) {
+      case SortTerm sort -> checkLevels(sort, null);
+      case PiTerm pi -> check(pi.body());
+      case SigmaTerm sigma -> false;
+      case DataCall dataCall when allowData() -> {
+        if (checkLevels(dataCall.ulift(), dataCall)) {
+          yield true;
+        }
+        int i = 0;
+        for (var argument : dataCall.args()) {
+          if (dataCall.ref().concrete.isCovariant(i)) {
+            if (checkConstructor(argument.term())) {
+              yield true;
+            }
+          } else {
+            if (checkNonCovariant(argument.term())) {
+              yield true;
+            }
+          }
+          i++;
+        }
+        yield false;
+      }
+      case StructCall structCall -> {
+        if (checkLevels(structCall.ulift(), structCall)) {
+          yield true;
+        }
+        var structConcrete = structCall.ref().concrete;
+        for (var field : structConcrete.fields) {
+          if (structConcrete.isCovariantField(field)) {
+            assert field.signature != null;
+            if (checkConstructor(field.signature.result())) {
+              yield true;
+            }
+          } else {
+            assert field.signature != null;
+            if (checkNonCovariant(field.signature.result())) {
+              yield true;
+            }
+          }
+        }
+        yield false;
+      }
+      case default -> checkOtherwise(term);
+    };
+  }
+}

base/src/main/java/org/aya/tyck/covariance/ParametersCovarianceChecker.java

@@ -0,0 +1,60 @@
+// Copyright (c) 2020-2022 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.covariance;
+
+import kala.collection.mutable.MutableHashSet;
+import org.aya.core.term.*;
+import org.aya.core.visitor.TermConsumer;
+import org.aya.ref.AnyVar;
+import org.aya.tyck.tycker.TyckState;
+import org.jetbrains.annotations.NotNull;
+
+public final class ParametersCovarianceChecker extends CovarianceChecker {
+  private final @NotNull MutableHashSet<@NotNull AnyVar> vars;
+
+  public ParametersCovarianceChecker(@NotNull TyckState state, @NotNull MutableHashSet<@NotNull AnyVar> vars) {
+    super(state);
+    this.vars = vars;
+  }
+
+  @Override
+  protected boolean checkNonCovariant(@NotNull Term term) {
+    new TermConsumer() {
+      @Override public void pre(@NotNull Term term1) {
+        if (term1 instanceof RefTerm refTerm) vars.remove(refTerm.var());
+        if (term1 instanceof RefTerm.Field fieldRef) vars.remove(fieldRef.ref());
+      }
+    }.accept(term);
+    return vars.isEmpty();
+  }
+
+  @Override
+  protected boolean checkOtherwise(@NotNull Term term) {
+    while (true) {
+      switch (term) {
+        case AppTerm app -> {
+          if (checkNonCovariant(app.arg().term())) {
+            return true;
+          }
+          term = app.of();
+        }
+        case PAppTerm pApp -> {
+          for (var arg : pApp.args()) {
+            if (checkNonCovariant(arg.term())) {
+              return true;
+            }
+          }
+          term = pApp.of();
+        }
+        case ProjTerm proj -> term = proj.of();
+        case FieldTerm access -> term = access.of();
+        case RefTerm refTerm -> {
+          return false;
+        }
+        case default -> {
+          return checkNonCovariant(term);
+        }
+      }
+    }
+  }
+}

base/src/main/java/org/aya/tyck/covariance/RecursiveDataChecker.java

@@ -0,0 +1,31 @@
+// Copyright (c) 2020-2022 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.covariance;
+
+import org.aya.concrete.stmt.TeleDecl;
+import org.aya.core.term.Term;
+import org.aya.tyck.covariance.CovarianceChecker;
+import org.aya.tyck.error.NonPositiveDataError;
+import org.aya.tyck.tycker.TyckState;
+import org.aya.util.reporter.Reporter;
+import org.jetbrains.annotations.NotNull;
+
+public final class RecursiveDataChecker extends CovarianceChecker {
+  private final @NotNull TeleDecl.DataCtor ctor;
+  private final @NotNull Reporter reporter;
+
+  @Override
+  protected boolean checkNonCovariant(@NotNull Term term) {
+    if (term.findUsages(ctor.dataRef) > 0) {
+      reporter.report(new NonPositiveDataError(ctor.sourcePos(), ctor, term));
+      return true;
+    }
+    return false;
+  }
+
+  public RecursiveDataChecker(@NotNull TyckState state, @NotNull Reporter reporter, TeleDecl.@NotNull DataCtor ctor) {
+    super(state);
+    this.reporter = reporter;
+    this.ctor = ctor;
+  }
+}

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

@@ -0,0 +1,26 @@
+// Copyright (c) 2020-2022 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.concrete.stmt.TeleDecl;
+import org.aya.core.term.Term;
+import org.aya.pretty.doc.Doc;
+import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public record NonPositiveDataError(
+  @Override @NotNull SourcePos sourcePos,
+  @NotNull TeleDecl.DataCtor ctor,
+  @NotNull Term term
+) implements TyckError {
+  @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    return Doc.sep(
+      Doc.english("Non-positive recursive occurrence of data type "),
+      ctor.dataRef.concrete.toDoc(options),
+      Doc.english(" in constructor "),
+      ctor.toDoc(options),
+      Doc.english(" at "),
+      term.toDoc(options));
+  }
+}