Allow flexibily "pushing" telescopes from return type

[ice1000]

Basically,

def f : A -> B
| a => b

Will be allowed (by translating into f (a : A) : B. To make it compatible with old behavior, we need

def f (a : A) : B -> C
| a => \b => c

to be accepted. This code will be translated into

def f (a : A) (b : B) : C
| a => \b => c

So we need to allow that. My idea is to push all lambdas into patterns.

[imkiva]

@ice1000 Should the second example be

def f (a : A) (b : B) : C
  | a, b => c

?

Or are we going to allow "pulling" lambda params from unmatched patterns?

[ice1000]

Or are we going to allow "pulling" lambda params from unmatched patterns?

Yes. In case it's not a lambda we insert arguments

[ice1000]

Or are we going to allow "pulling" lambda params from unmatched patterns?

Yes. In case it's not a lambda we insert arguments

Pull lambda during desugaring, insert arguments during type checking of Lhs.

[imkiva]

This sounds like what Agda did. Do you think this flexibility will add burdens to index unification?

[ice1000]

This sounds like what Agda did. Do you think this flexibility will add burdens to index unification?

I think no. The size of the telescope is still always known, it's just no longer equal to what you've written there.

Inductive types are not changed because they always return a universe

[ice1000]

diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
index 3b004b045..abf4838f7 100644
--- a/base/src/main/java/org/aya/tyck/StmtTycker.java
+++ b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -6,6 +6,7 @@ import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableArrayList;
 import kala.control.Either;
 import kala.control.Option;
+import kala.value.MutableValue;
 import org.aya.concrete.Expr;
 import org.aya.concrete.Pattern;
 import org.aya.concrete.stmt.ClassDecl;
@@ -29,6 +30,7 @@ import org.aya.tyck.pat.Conquer;
 import org.aya.tyck.pat.PatClassifier;
 import org.aya.tyck.pat.PatTycker;
 import org.aya.tyck.trace.Trace;
+import org.aya.util.Arg;
 import org.aya.util.Ordering;
 import org.aya.util.TreeBuilder;
 import org.aya.util.error.SourcePos;
@@ -187,9 +189,25 @@ public record StmtTycker(@NotNull Reporter reporter, Trace.@Nullable Builder tra
         // In the future, we may generate a "constant" meta and try to solve it
         //  if the result type is a pure meta.
         if (fn.body.isRight()) {
+          var beforeTeleSize = resultTele.size();
           var tele = MutableArrayList.from(resultTele);
           resultRes = PiTerm.unpi(tycker.zonk(resultRes), tele);
           resultTele = tele.toImmutableArray();
+          var afterTeleSize = resultTele.size();
+          var teleSizeDelta = afterTeleSize - beforeTeleSize;
+          if (teleSizeDelta > 0) {
+            var clauses = fn.body.getRightValue().map(cls -> {
+              if (cls.expr.isEmpty()) return cls;
+              var expr = cls.expr.get();
+              var pats = MutableArrayList.from(cls.patterns);
+              expr = Expr.unlam(expr, teleSizeDelta, param -> pats.append(new Arg<>(
+                new Pattern.Bind(param.sourcePos(), param.ref(), param.type(), MutableValue.create()
+                ), param.explicit())));
+              var remainingDelta = teleSizeDelta - (pats.size() - cls.patterns.size());
+              // TODO??
+              return new Pattern.Clause(cls.sourcePos, pats.toImmutableArray(), Option.some(expr));
+            });
+          }
         }
         fn.signature = new Def.Signature(resultTele, resultRes);
         if (resultTele.isEmpty() && fn.body.isRight() && fn.body.getRightValue().isEmpty())

[ice1000]

Reopen!