A def call short of its arguments converts up to eta (#1190)

bend2/bend.ts

@@ -3094,21 +3094,48 @@ function compare_go(mode: "EQ" | "LE", book: Book, lhs: HTerm, rhs: HTerm, dep:
     b = lit_step(b);
   }
   switch (a.$) {
-    case "Var": {
-      return b.$ === "Var" && a.i === b.i;
-    }
-    // a bare def is under-applied, so a function: two defs convert when
-    // they agree on fresh arguments (eta, as for a lambda)
-    case "Ref": {
-      if (b.$ !== "Ref" || a.k === b.k) {
-        return b.$ === "Ref";
+    // a stuck call: same head and arguments, else eta if a def is short of them
+    case "Var":
+    case "Ref":
+    case "App": {
+      let x: HTerm = a;
+      let y: HTerm = b;
+      let i = 0;
+      let j = 0;
+      let same = true;
+      while (x.$ === "App" || y.$ === "App") {
+        same = same && x.$ === "App" && y.$ === "App" && compare_go("EQ", book, x.x, y.x, dep);
+        if (x.$ === "App") {
+          x = x.f;
+          i++;
+        }
+        if (y.$ === "App") {
+          y = y.f;
+          j++;
+        }
       }
-      const n = Math.max(book.tlds[a.k]?.n ?? 0, book.tlds[b.k]?.n ?? 0);
-      let [f, g]: HTerm[] = [a, b];
-      for (let j = 0; j < n; j++) {
-        [f, g] = [App(f, Var("_", dep + j)), App(g, Var("_", dep + j))];
+      if (x.$ === "Var") {
+        same = same && y.$ === "Var" && x.i === y.i;
+      } else if (x.$ === "Ref") {
+        same = same && y.$ === "Ref" && x.k === y.k;
+      } else {
+        same = same && compare_go("EQ", book, x, y, dep);
       }
-      return n > 0 && compare_go(mode, book, f, g, dep + n);
+      if (same) {
+        return true;
+      }
+      let n = 0;
+      if (x.$ === "Ref") {
+        n = (book.tlds[x.k]?.n ?? 0) - i;
+      }
+      if (y.$ === "Ref") {
+        n = Math.max(n, (book.tlds[y.k]?.n ?? 0) - j);
+      }
+      for (let k = 0; k < n; k++) {
+        a = App(a, Var("_", dep + k));
+        b = App(b, Var("_", dep + k));
+      }
+      return n > 0 && compare_go(mode, book, a, b, dep + n);
     }
     case "Typ": {
       if (b.$ !== "Typ") {
@@ -3153,15 +3180,6 @@ function compare_go(mode: "EQ" | "LE", book: Book, lhs: HTerm, rhs: HTerm, dep:
           && compare_go(mode, book, b.A, a.A, dep)
           && compare_go(mode, book, a.B(x), b.B(x), dep + 1);
     }
-    // a stuck call is canonical: its head def compares by name, not by eta
-    case "App": {
-      if (b.$ !== "App") {
-        return false;
-      }
-      const head = a.f.$ === "Ref" && b.f.$ === "Ref" ? a.f.k === b.f.k
-        : compare_go("EQ", book, a.f, b.f, dep);
-      return head && compare_go("EQ", book, a.x, b.x, dep);
-    }
     case "ADT": {
       if (b.$ !== "ADT" || a.k !== b.k || a.x.length !== b.x.length) {
         return false;

tests/check/partial_call_eta.bend

@@ -0,0 +1,40 @@
+# a partly applied def is a function, as a bare def is: l(U) and r(U)
+# convert when they agree on a fresh argument. once only bare defs got
+# eta, so l == r held but l(U) == r(U) did not, and an inline {==}
+# proof, merging the shared cells of l and r, changed what a Box<r(U)>
+# read as: the inline proof passed and the named one failed (#1190)
+type U is Data:
+  U{}
+
+def l(A: Type, B: Type) -> Type:
+  A
+
+def r(A: Type, B: Type) -> Type:
+  A
+
+type Box<-h: Type -> Type> is Type:
+  Box{}
+
+def G(-f: Type -> Type -> Type, -g: Type -> Type -> Type) -> Type:
+  {f == g : Type -> Type -> Type} -> Box<g(U)>
+
+def make() -> G(l, r):
+  e => Box{}
+
+def proof() -> {l == r : Type -> Type -> Type}:
+  {==}
+
+def inline() -> Box<l(U)>:
+  make()({==})
+
+def named() -> Box<l(U)>:
+  make()(proof())
+
+def partial() -> {l(U) == r(U) : Type -> Type}:
+  {==}
+
+def direct(x: Box<r(U)>) -> Box<l(U)>:
+  x
+
+#|ALL PROOFS CHECK
+#|Use --verdict for mathematical validity.

tests/check/partial_call_eta_distinct.bend

@@ -0,0 +1,34 @@
+# l(U) and r(U) disagree on a fresh argument, so they do not convert,
+# however a proof of {l == r} is given (none is): the inline {==} fails
+# and leaves Box<r(U)> as it was (#1190)
+type U is Data:
+  U{}
+
+def l(A: Type, B: Type) -> Type:
+  A
+
+def r(A: Type, B: Type) -> Type:
+  B
+
+type Box<-h: Type -> Type> is Type:
+  Box{}
+
+def G(-f: Type -> Type -> Type, -g: Type -> Type -> Type) -> Type:
+  {f == g : Type -> Type -> Type} -> Box<g(U)>
+
+def make() -> G(l, r):
+  e => Box{}
+
+def inline() -> Box<l(U)>:
+  make()({==})
+
+#|SOME PROOFS FAIL
+#|Error:
+#|- expected : l
+#|- observed : r
+#|Location: inline
+#|22 | def inline() -> Box<l(U)>:
+#|23>|   make()({==})
+#|   |          ^^^^
+#|24 | 
+#|exit 1