TYCK: fix #697

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

@@ -7,6 +7,7 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.Buffer;
 import kala.collection.mutable.MutableMap;
+import kala.control.Either;
 import kala.tuple.Tuple;
 import kala.tuple.Tuple2;
 import kala.tuple.Tuple3;
@@ -504,8 +505,9 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
           // that implies paramLicit == false
           var holeApp = mockTerm(pi.param(), namedArg.expr().sourcePos());
           app = CallTerm.make(app, new Arg<>(holeApp, false));
-          pi = instPi(pi, subst, holeApp);
-          if (pi == null) return new Result(new ErrorTerm(expr), f.type);
+          var newPi = instPi(pi, subst, holeApp);
+          if (newPi.isLeft()) pi = newPi.getLeftValue();
+          else return wantButNo(expr, newPi.getRightValue(), "function type");
         } else {
           // TODO[ice]: no implicit argument expected, but inserted.
           throw new TyckerException();
@@ -514,9 +516,12 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
       var elabArg = checkNoZonk(namedArg.expr(), pi.param().type()).wellTyped;
       app = CallTerm.make(app, new Arg<>(elabArg, argLicit));
       // so, in the end, the pi term is not updated, its body would be the eliminated type
-      if (iter.hasNext()) pi = instPi(pi, subst, elabArg);
-      if (pi == null) return new Result(new ErrorTerm(expr), f.type);
-      else subst.map().put(pi.param().ref(), elabArg);
+      if (iter.hasNext()) {
+        var newPi = instPi(pi, subst, elabArg);
+        if (newPi.isLeft()) pi = newPi.getLeftValue();
+        else return wantButNo(expr, newPi.getRightValue(), "function type");
+      }
+      subst.map().put(pi.param().ref(), elabArg);
     }
     return unifyTyMaybeInsert(term, pi.body().subst(subst), app, expr);
   }
@@ -528,9 +533,11 @@ private Result visitAccess(Expr struct, String fieldName, Expr.@NotNull ProjExpr
     return localCtx.freshHole(param.type(), genName, pos)._2;
   }
 
-  private FormTerm.@Nullable Pi instPi(@NotNull FormTerm.Pi pi, Substituter.TermSubst subst, @NotNull Term arg) {
+  private Either<FormTerm.Pi, Term>
+  instPi(@NotNull FormTerm.Pi pi, Substituter.TermSubst subst, @NotNull Term arg) {
     subst.add(pi.param().ref(), arg);
-    return pi.body().subst(subst).normalize(NormalizeMode.WHNF) instanceof FormTerm.Pi newPi ? newPi : null;
+    var term = pi.body().subst(subst).normalize(NormalizeMode.WHNF);
+    return term instanceof FormTerm.Pi pai ? Either.left(pai) : Either.right(term);
   }
 
   @Rule.Check(partialSynth = true)

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

@@ -2,13 +2,11 @@
 // Use of this source code is governed by the GNU GPLv3 license that can be found in the LICENSE file.
 package org.aya.tyck.error;
 
-import kala.tuple.Unit;
 import org.aya.api.distill.DistillerOptions;
 import org.aya.api.error.ExprProblem;
 import org.aya.api.util.NormalizeMode;
 import org.aya.concrete.Expr;
 import org.aya.core.term.Term;
-import org.aya.core.visitor.Zonker;
 import org.aya.pretty.doc.Doc;
 import org.jetbrains.annotations.NotNull;
 
@@ -23,9 +21,9 @@ public record BadTypeError(
 
   @Override public @NotNull Doc describe() {
     return Doc.vcat(
-      Doc.sep(Doc.plain("Expected type:"), actualType.toDoc(DistillerOptions.DEFAULT)),
-      Doc.sep(Doc.plain("Normalized:"), actualType.normalize(NormalizeMode.NF).toDoc(DistillerOptions.DEFAULT)),
       Doc.sep(Doc.plain("Want:"), expectedType),
+      Doc.sep(Doc.plain("Got:"), actualType.toDoc(DistillerOptions.DEFAULT)),
+      Doc.sep(Doc.plain("Normalized:"), actualType.normalize(NormalizeMode.NF).toDoc(DistillerOptions.DEFAULT)),
       Doc.sep(Doc.english("Because we want to type a term such as:"), expr.toDoc(DistillerOptions.DEFAULT))
     );
   }

base/src/test/resources/failure/tyck/issue697.aya

@@ -0,0 +1,30 @@
+prim I
+prim left
+prim right
+prim arcoe
+struct Path (A : I -> Type) (a : A left) (b : A right) : Type
+  | at (i : I) : A i {
+    | left => a
+    | right => b
+  }
+def path {A : I -> Type} (p : Pi (i : I) -> A i)
+  => new Path A (p left) (p right) { | at i => p i }
+def `=` Eq {A : Type} (a b : A) : Type => Path (\ i => A) a b
+bind = looser application
+def idp {A : Type} {a : A} : a = a => path (\ i => a)
+
+def hfill2d {A : Type}
+  {a b c d : A}
+  (p : Eq a b)
+  (q : Eq b d)
+  (r : Eq a c)
+  (i j : I) : A
+  => (arcoe (\ k => Eq (r.at k) (q.at k)) p i).at j
+def hcomp2d {A : Type}
+  {a b c d : A}
+  (p : Eq a b)
+  (q : Eq b d)
+  (r : Eq a c) : Eq c d
+  => path (hfill2d p q r right)
+
+def sym {A : Type} {a b : A} (p : Eq a b) : Eq b a => hcomp2d (idp a) idp p

base/src/test/resources/failure/tyck/issue697.aya.txt

@@ -0,0 +1,12 @@
+In file $FILE:30:63 ->
+
+  28 |   => path (hfill2d p q r right)
+  29 | 
+  30 | def sym {A : Type} {a b : A} (p : Eq a b) : Eq b a => hcomp2d (idp a) idp p
+                                                                      ^---^
+
+Error: Want: function type
+       Got: Path (λ _ ⇒ A$) a$ a$
+       Normalized: Path (λ _ ⇒ A$) a$ a$
+       Because we want to type a term such as: idp a
+What are you doing?

base/src/test/resources/failure/tyck/want-but-no.aya.txt

@@ -3,8 +3,8 @@ In file $FILE:1:19 ->
   1 | def test : Type => \ x => x
                          ^------^
 
-Error: Expected type: Type
+Error: Want: pi type
+       Got: Type
        Normalized: Type
-       Want: pi type
        Because we want to type a term such as: λ x ⇒ x
 What are you doing?