Repository: aya-prover/aya-dev
Issue: Pretty printer bug

This assertion
```patch
Index: base/src/test/java/org/aya/core/DistillerTest.java
IDEA additional info:
Subsystem: com.intellij.openapi.diff.impl.patch.CharsetEP
<+>UTF-8
===================================================================
diff --git a/base/src/test/java/org/aya/core/DistillerTest.java b/base/src/test/java/org/aya/core/DistillerTest.java
--- a/base/src/test/java/org/aya/core/DistillerTest.java	(revision 3275eeb0b50bc6cec23bbdacf86aa6c734cc02cb)
+++ b/base/src/test/java/org/aya/core/DistillerTest.java	(date 1662024364066)
@@ -88,6 +88,18 @@
     assertEquals("(Pi (A : Type 0) -> A) = X", test2.toDoc(DistillerOptions.informative()).debugRender());
   }
 
+  @Test public void binop() {
+    var decls = TyckDeclTest.successTyckDecls("""
+      open data Nat | zero | suc Nat
+      open data D   | infix · Nat Nat
+      
+      def g (h : Nat -> D) : Nat => zero
+      def t (n : Nat) => g (n ·)
+      """)._2;
+    var t = ((FnDef) decls.get(3)).body.getLeftValue();
+    assertEquals("g (n ·)", t.toDoc(DistillerOptions.informative()).debugRender());
+  }
+
   private @NotNull Doc declDoc(@Language("TEXT") String text) {
     return Doc.vcat(TyckDeclTest.successTyckDecls(text)._2.map(d -> d.toDoc(DistillerOptions.debug())));
   }

```

would fail:

```
org.opentest4j.AssertionFailedError: 
Expected :g (n ·)
Actual   :g · n
```


Changed files:
base/src/main/java/org/aya/distill/CoreDistiller.java, base/src/test/java/org/aya/core/DistillerTest.java

diff --git a/base/src/main/java/org/aya/distill/CoreDistiller.java b/base/src/main/java/org/aya/distill/CoreDistiller.java
index 22078a01b..5544d83c9 100644
--- a/base/src/main/java/org/aya/distill/CoreDistiller.java
+++ b/base/src/main/java/org/aya/distill/CoreDistiller.java
@@ -73,7 +73,7 @@ public class CoreDistiller extends BaseDistiller<Term> {
             var style = chooseStyle(defVar);
             bodyDoc = style != null
               ? visitArgsCalls(defVar, style, args, Outer.Free)
-              : visitCalls(false, varDoc(defVar), args, Outer.Free,
+              : visitCalls(defVar.isInfix(), varDoc(defVar), args, params.isEmpty() ? outer : Outer.Free,
               options.map.get(DistillerOptions.Key.ShowImplicitArgs));
           }
         } else bodyDoc = term(Outer.Free, body);
diff --git a/base/src/test/java/org/aya/core/DistillerTest.java b/base/src/test/java/org/aya/core/DistillerTest.java
index 8c49a85db..4fe5721b4 100644
--- a/base/src/test/java/org/aya/core/DistillerTest.java
+++ b/base/src/test/java/org/aya/core/DistillerTest.java
@@ -88,6 +88,18 @@ public class DistillerTest {
     assertEquals("(Pi (A : Type 0) -> A) = X", test2.toDoc(DistillerOptions.informative()).debugRender());
   }
 
+  @Test public void binop() {
+    var decls = TyckDeclTest.successTyckDecls("""
+      open data Nat | zero | suc Nat
+      open data D   | infix · Nat Nat
+
+      def g (h : Nat -> D) : Nat => zero
+      def t (n : Nat) => g (n ·)
+      """)._2;
+    var t = ((FnDef) decls.get(3)).body.getLeftValue();
+    assertEquals("g (n ·)", t.toDoc(DistillerOptions.informative()).debugRender());
+  }
+
   private @NotNull Doc declDoc(@Language("TEXT") String text) {
     return Doc.vcat(TyckDeclTest.successTyckDecls(text)._2.map(d -> d.toDoc(DistillerOptions.debug())));
   }