- Renamed "App" to "Apply" and swapped the order of the arguments to it.

- Also did argument swapping for lux/type;application.

9 files changed, 121 insertions, 120 deletions

diff --git a/luxc/src/lux/analyser/base.clj b/luxc/src/lux/analyser/base.clj
index e762c3870..b71df2b1f 100644
--- a/luxc/src/lux/analyser/base.clj
+++ b/luxc/src/lux/analyser/base.clj
@@ -75,7 +75,7 @@
                   (return ?module))]
     (return (&/T [module* ?name]))))
 
-(let [tag-names #{"Host" "Void" "Unit" "Sum" "Product" "Function" "Bound" "Var" "Ex" "UnivQ" "ExQ" "App" "Named"}]
+(let [tag-names #{"Host" "Void" "Unit" "Sum" "Product" "Function" "Bound" "Var" "Ex" "UnivQ" "ExQ" "Apply" "Named"}]
   (defn type-tag? [module name]
     (and (= "lux" module)
          (contains? tag-names name))))
diff --git a/luxc/src/lux/analyser/case.clj b/luxc/src/lux/analyser/case.clj
index 613e415f5..c60059540 100644
--- a/luxc/src/lux/analyser/case.clj
+++ b/luxc/src/lux/analyser/case.clj
@@ -78,9 +78,9 @@
     (&/$Function (clean! level ?tid bound-idx ?arg)
                  (clean! level ?tid bound-idx ?return))
 
-    (&/$App ?lambda ?param)
-    (&/$App (clean! level ?tid bound-idx ?lambda)
-            (clean! level ?tid bound-idx ?param))
+    (&/$Apply ?param ?lambda)
+    (&/$Apply (clean! level ?tid bound-idx ?param)
+              (clean! level ?tid bound-idx ?lambda))
 
     (&/$Product ?left ?right)
     (&/$Product (clean! level ?tid bound-idx ?left)
@@ -115,9 +115,9 @@
     (&/$Product (beta-reduce! level env ?left)
                 (beta-reduce! level env ?right))
 
-    (&/$App ?type-fn ?type-arg)
-    (&/$App (beta-reduce! level env ?type-fn)
-            (beta-reduce! level env ?type-arg))
+    (&/$Apply ?type-arg ?type-fn)
+    (&/$Apply (beta-reduce! level env ?type-arg)
+              (beta-reduce! level env ?type-fn))
     
     (&/$UnivQ ?local-env ?local-def)
     (|case ?local-env
@@ -165,7 +165,7 @@
                                  (&/$Cons type-fn))
                           local-def))
 
-    (&/$App F A)
+    (&/$Apply A F)
     (|do [type-fn* (apply-type! F A)]
       (apply-type! type-fn* param))
 
@@ -173,7 +173,7 @@
     (apply-type! ?type param)
 
     (&/$Ex id)
-    (return (&/$App type-fn param))
+    (return (&/$Apply param type-fn))
 
     (&/$Var id)
     (|do [=type-fun (deref id)]
@@ -229,7 +229,7 @@
       (return (&type/Variant$ (&/|map distributor
                                       (&type/flatten-sum =type)))))
 
-    (&/$App ?tfun ?targ)
+    (&/$Apply ?targ ?tfun)
     (|do [=type (apply-type! ?tfun ?targ)]
       (adjust-type* up =type))
 
diff --git a/luxc/src/lux/analyser/lux.clj b/luxc/src/lux/analyser/lux.clj
index 2a76ec86a..b2292d879 100644
--- a/luxc/src/lux/analyser/lux.clj
+++ b/luxc/src/lux/analyser/lux.clj
@@ -411,7 +411,7 @@
 
 (defn ^:private unravel-inf-appt [type]
   (|case type
-    (&/$App =input+ (&/$Var _inf-var))
+    (&/$Apply (&/$Var _inf-var) =input+)
     (&/$Cons _inf-var (unravel-inf-appt =input+))
 
     _
@@ -426,7 +426,7 @@
           =func** (&type/clean $output =func*)]
       (return (&/$UnivQ &/$Nil =func**)))
     
-    (&/$App =input+ (&/$Var _inf-var))
+    (&/$Apply (&/$Var _inf-var) =input+)
     (&/fold% (fn [_func _inf-var]
                (|do [:let [$inf-var (&/$Var _inf-var)]
                      =inf-var (&type/resolve-type $inf-var)
@@ -683,8 +683,8 @@
         =value (&&/analyse-1+ analyse ?value)]
     (return (&/|list (coerce ==type =value)))))
 
-(let [input-type (&/$App &type/List &type/Text)
-      output-type (&/$App &type/IO &/$Unit)]
+(let [input-type (&/$Apply &type/Text &type/List)
+      output-type (&/$Apply &/$Unit &type/IO)]
   (defn analyse-program [analyse optimize compile-program ?args ?body]
     (|do [_ &/ensure-statement
           =body (&/with-scope ""
diff --git a/luxc/src/lux/analyser/proc/common.clj b/luxc/src/lux/analyser/proc/common.clj
index a0430feb7..0695de2a6 100644
--- a/luxc/src/lux/analyser/proc/common.clj
+++ b/luxc/src/lux/analyser/proc/common.clj
@@ -21,7 +21,7 @@
   (&type/with-var
     (fn [$var]
       (|do [:let [(&/$Cons op (&/$Nil)) ?values]
-            =op (&&/analyse-1 analyse (&/$App &type/IO $var) op)
+            =op (&&/analyse-1 analyse (&/$Apply $var &type/IO) op)
             _ (&type/check exo-type (&/$Sum &type/Text ;; lux;Left
                                             $var ;; lux;Right
                                             ))
@@ -57,8 +57,8 @@
                                            (&/|list =text =part =start)
                                            (&/|list)))))))
 
-  ^:private analyse-text-index      "index"      (&/$App &type/Maybe &type/Nat)
-  ^:private analyse-text-last-index "last-index" (&/$App &type/Maybe &type/Nat)
+  ^:private analyse-text-index      "index"      (&/$Apply &type/Nat &type/Maybe)
+  ^:private analyse-text-last-index "last-index" (&/$Apply &type/Nat &type/Maybe)
   )
 
 (defn ^:private analyse-text-contains? [analyse exo-type ?values]
@@ -77,7 +77,7 @@
         =text (&&/analyse-1 analyse &type/Text text)
         =from (&&/analyse-1 analyse &type/Nat from)
         =to (&&/analyse-1 analyse &type/Nat to)
-        _ (&type/check exo-type (&/$App &type/Maybe &type/Text))
+        _ (&type/check exo-type (&/$Apply &type/Text &type/Maybe))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["text" "clip"])
@@ -131,7 +131,7 @@
   (|do [:let [(&/$Cons text (&/$Cons idx (&/$Nil))) ?values]
         =text (&&/analyse-1 analyse &type/Text text)
         =idx (&&/analyse-1 analyse &type/Nat idx)
-        _ (&type/check exo-type (&/$App &type/Maybe &type/Char))
+        _ (&type/check exo-type (&/$Apply &type/Char &type/Maybe))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["text" "char"])
@@ -245,7 +245,7 @@
           (return (&/|list (&&/|meta exo-type _cursor
                                      (&&/$proc (&/T <encode-op>) (&/|list =x) (&/|list)))))))
 
-    (let [decode-type (&/$App &type/Maybe <type>)]
+    (let [decode-type (&/$Apply <type> &type/Maybe)]
       (defn <decode> [analyse exo-type ?values]
         (|do [:let [(&/$Cons x (&/$Nil)) ?values]
               =x (&&/analyse-1 analyse &type/Text x)
@@ -331,7 +331,7 @@
       (|do [:let [(&/$Cons array (&/$Cons idx (&/$Nil))) ?values]
             =array (&&/analyse-1 analyse (&type/Array $var) array)
             =idx (&&/analyse-1 analyse &type/Nat idx)
-            _ (&type/check exo-type (&/$App &type/Maybe $var))
+            _ (&type/check exo-type (&/$Apply $var &type/Maybe))
             _cursor &/cursor]
         (return (&/|list (&&/|meta exo-type _cursor
                                    (&&/$proc (&/T ["array" "get"]) (&/|list =array =idx) (&/|list)))))))))
@@ -465,7 +465,7 @@
 
 (defn ^:private analyse-process-future [analyse exo-type ?values]
   (|do [:let [(&/$Cons ?procedure (&/$Nil)) ?values]
-        =procedure (&&/analyse-1 analyse (&/$App &type/IO &type/Top) ?procedure)
+        =procedure (&&/analyse-1 analyse (&/$Apply &type/Top &type/IO) ?procedure)
         _ (&type/check exo-type &/$Unit)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
@@ -474,7 +474,7 @@
 (defn ^:private analyse-process-schedule [analyse exo-type ?values]
   (|do [:let [(&/$Cons ?milliseconds (&/$Cons ?procedure (&/$Nil))) ?values]
         =milliseconds (&&/analyse-1 analyse &type/Nat ?milliseconds)
-        =procedure (&&/analyse-1 analyse (&/$App &type/IO &type/Top) ?procedure)
+        =procedure (&&/analyse-1 analyse (&/$Apply &type/Top &type/IO) ?procedure)
         _ (&type/check exo-type &/$Unit)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
diff --git a/luxc/src/lux/analyser/proc/jvm.clj b/luxc/src/lux/analyser/proc/jvm.clj
index 977c07787..910f5c72f 100644
--- a/luxc/src/lux/analyser/proc/jvm.clj
+++ b/luxc/src/lux/analyser/proc/jvm.clj
@@ -39,7 +39,7 @@
     (&/$ExQ _ type*)
     (ensure-object type*)
 
-    (&/$App F A)
+    (&/$Apply A F)
     (|do [type* (&type/apply-type F A)]
       (ensure-object type*))
 
diff --git a/luxc/src/lux/base.clj b/luxc/src/lux/base.clj
index 87d6786e5..2f2d879fe 100644
--- a/luxc/src/lux/base.clj
+++ b/luxc/src/lux/base.clj
@@ -97,7 +97,7 @@
   ("Ex" 1)
   ("UnivQ" 2)
   ("ExQ" 2)
-  ("App" 2)
+  ("Apply" 2)
   ("Named" 2))
 
 ;; Vars
diff --git a/luxc/src/lux/compiler/cache/type.clj b/luxc/src/lux/compiler/cache/type.clj
index f6f06f03c..04fb01540 100644
--- a/luxc/src/lux/compiler/cache/type.clj
+++ b/luxc/src/lux/compiler/cache/type.clj
@@ -57,7 +57,7 @@
       (&/$Var idx)
       (str "?" idx stop)
 
-      (&/$App left right)
+      (&/$Apply left right)
       (str "%" (serialize-type left) (serialize-type right))
 
       (&/$Named [module name] type*)
@@ -101,7 +101,7 @@
   ^:private deserialize-sum  "+" &/$Sum
   ^:private deserialize-prod "*" &/$Product
   ^:private deserialize-lambda    ">" &/$Function
-  ^:private deserialize-app  "%" &/$App
+  ^:private deserialize-app  "%" &/$Apply
   )
 
 (do-template [<name> <signal> <type>]
diff --git a/luxc/src/lux/host.clj b/luxc/src/lux/host.clj
index f602376fb..7ee553d53 100644
--- a/luxc/src/lux/host.clj
+++ b/luxc/src/lux/host.clj
@@ -70,7 +70,7 @@
       (&/$Named ?name ?type)
       (->java-sig ?type)
 
-      (&/$App ?F ?A)
+      (&/$Apply ?A ?F)
       (|do [type* (&type/apply-type ?F ?A)]
         (->java-sig type*))
 
diff --git a/luxc/src/lux/type.clj b/luxc/src/lux/type.clj
index 85ce1613b..b569d890f 100644
--- a/luxc/src/lux/type.clj
+++ b/luxc/src/lux/type.clj
@@ -63,8 +63,8 @@
                        &/$Unit
                        ;; lux;Cons
                        (&/$Product (&/$Bound 1)
-                                   (&/$App (&/$Bound 0)
-                                           (&/$Bound 1)))))))
+                                   (&/$Apply (&/$Bound 1)
+                                             (&/$Bound 0)))))))
 
 (def Maybe
   (&/$Named (&/T ["lux" "Maybe"])
@@ -78,90 +78,90 @@
 
 (def Type
   (&/$Named (&/T ["lux" "Type"])
-            (let [Type (&/$App (&/$Bound 0) (&/$Bound 1))
-                  TypeList (&/$App List Type)
+            (let [Type (&/$Apply (&/$Bound 1) (&/$Bound 0))
+                  TypeList (&/$Apply Type List)
                   TypePair (&/$Product Type Type)]
-              (&/$App (&/$UnivQ empty-env
-                                (&/$Sum
-                                 ;; Host
-                                 (&/$Product Text TypeList)
-                                 (&/$Sum
-                                  ;; Void
-                                  &/$Unit
+              (&/$Apply &/$Void
+                        (&/$UnivQ empty-env
                                   (&/$Sum
-                                   ;; Unit
-                                   &/$Unit
+                                   ;; Host
+                                   (&/$Product Text TypeList)
                                    (&/$Sum
-                                    ;; Sum
-                                    TypePair
+                                    ;; Void
+                                    &/$Unit
                                     (&/$Sum
-                                     ;; Product
-                                     TypePair
+                                     ;; Unit
+                                     &/$Unit
                                      (&/$Sum
-                                      ;; Function
+                                      ;; Sum
                                       TypePair
                                       (&/$Sum
-                                       ;; Bound
-                                       Nat
+                                       ;; Product
+                                       TypePair
                                        (&/$Sum
-                                        ;; Var
-                                        Nat
+                                        ;; Function
+                                        TypePair
                                         (&/$Sum
-                                         ;; Ex
+                                         ;; Bound
                                          Nat
                                          (&/$Sum
-                                          ;; UnivQ
-                                          (&/$Product TypeList Type)
+                                          ;; Var
+                                          Nat
                                           (&/$Sum
-                                           ;; ExQ
-                                           (&/$Product TypeList Type)
+                                           ;; Ex
+                                           Nat
                                            (&/$Sum
-                                            ;; App
-                                            TypePair
-                                            ;; Named
-                                            (&/$Product Ident Type)))))))))))))
-                                )
-                      &/$Void))))
+                                            ;; UnivQ
+                                            (&/$Product TypeList Type)
+                                            (&/$Sum
+                                             ;; ExQ
+                                             (&/$Product TypeList Type)
+                                             (&/$Sum
+                                              ;; App
+                                              TypePair
+                                              ;; Named
+                                              (&/$Product Ident Type)))))))))))))
+                                  )))))
 
 (def Ann-Value
   (&/$Named (&/T ["lux" "Ann-Value"])
-            (let [Ann-Value (&/$App (&/$Bound 0) (&/$Bound 1))]
-              (&/$App (&/$UnivQ empty-env
-                                (&/$Sum
-                                 ;; BoolA
-                                 Bool
-                                 (&/$Sum
-                                  ;; NatA
-                                  Nat
+            (let [Ann-Value (&/$Apply (&/$Bound 1) (&/$Bound 0))]
+              (&/$Apply &/$Void
+                        (&/$UnivQ empty-env
                                   (&/$Sum
-                                   ;; IntA
-                                   Int
+                                   ;; BoolA
+                                   Bool
                                    (&/$Sum
-                                    ;; DegA
-                                    Deg
+                                    ;; NatA
+                                    Nat
                                     (&/$Sum
-                                     ;; RealA
-                                     Real
+                                     ;; IntA
+                                     Int
                                      (&/$Sum
-                                      ;; CharA
-                                      Char
+                                      ;; DegA
+                                      Deg
                                       (&/$Sum
-                                       ;; TextA
-                                       Text
+                                       ;; RealA
+                                       Real
                                        (&/$Sum
-                                        ;; IdentA
-                                        Ident
+                                        ;; CharA
+                                        Char
                                         (&/$Sum
-                                         ;; ListA
-                                         (&/$App List Ann-Value)
-                                         ;; DictA
-                                         (&/$App List (&/$Product Text Ann-Value)))))))))))
-                                )
-                      &/$Void))))
+                                         ;; TextA
+                                         Text
+                                         (&/$Sum
+                                          ;; IdentA
+                                          Ident
+                                          (&/$Sum
+                                           ;; ListA
+                                           (&/$Apply Ann-Value List)
+                                           ;; DictA
+                                           (&/$Apply (&/$Product Text Ann-Value) List))))))))))
+                                  )))))
 
 (def Anns
   (&/$Named (&/T ["lux" "Anns"])
-            (&/$App List (&/$Product Ident Ann-Value))))
+            (&/$Apply (&/$Product Ident Ann-Value) List)))
 
 (def Macro)
 
@@ -225,7 +225,7 @@
   (fn [state]
     (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
       (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id (&/$Some type) %)
-                                                             ts))
+                                                              ts))
                           state)
                nil)
       ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length)))
@@ -235,7 +235,7 @@
   (fn [state]
     (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
       (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id &/$None %)
-                                                             ts))
+                                                              ts))
                           state)
                nil)
       ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length)))
@@ -347,10 +347,10 @@
           =return (clean* ?tid ?return)]
       (return (&/$Function =arg =return)))
 
-    (&/$App ?lambda ?param)
+    (&/$Apply ?param ?lambda)
     (|do [=lambda (clean* ?tid ?lambda)
           =param (clean* ?tid ?param)]
-      (return (&/$App =lambda =param)))
+      (return (&/$Apply =param =lambda)))
 
     (&/$Product ?left ?right)
     (|do [=left (clean* ?tid ?left)
@@ -395,9 +395,9 @@
 
 (defn ^:private unravel-app [fun-type]
   (|case fun-type
-    (&/$App ?left ?right)
-    (|let [[?fun-type ?args] (unravel-app ?left)]
-      (&/T [?fun-type (&/|++ ?args (&/|list ?right))]))
+    (&/$Apply ?arg ?func)
+    (|let [[?fun-type ?args] (unravel-app ?func)]
+      (&/T [?fun-type (&/$Cons ?arg ?args)]))
 
     _
     (&/T [fun-type &/$Nil])))
@@ -482,7 +482,7 @@
     (&/$Bound idx)
     (str idx)
 
-    (&/$App _ _)
+    (&/$Apply _ _)
     (|let [[?call-fun ?call-args] (unravel-app type)]
       (str "(" (show-type ?call-fun) " " (->> ?call-args (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
     
@@ -539,8 +539,8 @@
                      [(&/$Ex xid) (&/$Ex yid)]
                      (= xid yid)
 
-                     [(&/$App xlambda xparam) (&/$App ylambda yparam)]
-                     (and (type= xlambda ylambda) (type= xparam yparam))
+                     [(&/$Apply xparam xlambda) (&/$Apply yparam ylambda)]
+                     (and (type= xparam yparam) (type= xlambda ylambda))
                      
                      [(&/$UnivQ xenv xbody) (&/$UnivQ yenv ybody)]
                      (type= xbody ybody)
@@ -606,8 +606,8 @@
     (&/$Product ?left ?right)
     (&/$Product (beta-reduce env ?left) (beta-reduce env ?right))
 
-    (&/$App ?type-fn ?type-arg)
-    (&/$App (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
+    (&/$Apply ?type-arg ?type-fn)
+    (&/$Apply (beta-reduce env ?type-arg) (beta-reduce env ?type-fn))
     
     (&/$UnivQ ?local-env ?local-def)
     (|case ?local-env
@@ -654,7 +654,7 @@
                               (&/$Cons type-fn))
                          local-def))
 
-    (&/$App F A)
+    (&/$Apply A F)
     (|do [type-fn* (apply-type F A)]
       (apply-type type-fn* param))
 
@@ -663,14 +663,15 @@
 
     ;; TODO: This one must go...
     (&/$Ex id)
-    (return (&/$App type-fn param))
+    (return (&/$Apply param type-fn))
 
     (&/$Var id)
     (|do [=type-fun (deref id)]
       (apply-type =type-fun param))
     
     _
-    (&/fail-with-loc (str "[Type System] Not a type function:\n" (show-type type-fn) "\n"))))
+    (&/fail-with-loc (str "[Type System] Not a type function:\n" (show-type type-fn) "\n"
+                          "for arg: " (show-type param)))))
 
 (def ^:private init-fixpoints &/$Nil)
 
@@ -732,15 +733,15 @@
                (check* fixpoints invariant?? expected bound))
              state)))
 
-        [(&/$App (&/$Ex eid) eA) (&/$App (&/$Ex aid) aA)]
+        [(&/$Apply eA (&/$Ex eid)) (&/$Apply aA (&/$Ex aid))]
         (if (= eid aid)
           (check* fixpoints invariant?? eA aA)
           (check-error "" expected actual))
 
-        [(&/$App (&/$Var ?id) A1) (&/$App F2 A2)]
+        [(&/$Apply A1 (&/$Var ?id)) (&/$Apply A2 F2)]
         (fn [state]
           (|case ((|do [F1 (deref ?id)]
-                    (check* fixpoints invariant?? (&/$App F1 A1) actual))
+                    (check* fixpoints invariant?? (&/$Apply A1 F1) actual))
                   state)
             (&/$Right state* output)
             (return* state* output)
@@ -764,10 +765,10 @@
                  (check* fixpoints* invariant?? e* a*))
                state))))
         
-        [(&/$App F1 A1) (&/$App (&/$Var ?id) A2)]
+        [(&/$Apply A1 F1) (&/$Apply A2 (&/$Var ?id))]
         (fn [state]
           (|case ((|do [F2 (deref ?id)]
-                    (check* fixpoints invariant?? expected (&/$App F2 A2)))
+                    (check* fixpoints invariant?? expected (&/$Apply A2 F2)))
                   state)
             (&/$Right state* output)
             (return* state* output)
@@ -779,7 +780,7 @@
                (check* fixpoints* invariant?? e* a*))
              state)))
         
-        [(&/$App F A) _]
+        [(&/$Apply A F) _]
         (let [fp-pair (&/T [expected actual])
               _ (when (> (&/|length fixpoints) 64)
                   (&/|log! (println-str 'FIXPOINTS (->> (&/|keys fixpoints)
@@ -789,7 +790,7 @@
                                                                          (show-type a)))))
                                                         (&/|interpose "\n\n")
                                                         (&/fold str ""))))
-                  (assert false (prn-str 'check* '[(&/$App F A) _] (&/|length fixpoints) (show-type expected) (show-type actual))))]
+                  (assert false (prn-str 'check* '[(&/$Apply A F) _] (&/|length fixpoints) (show-type expected) (show-type actual))))]
           (|case (fp-get fp-pair fixpoints)
             (&/$Some ?)
             (if ?
@@ -800,10 +801,10 @@
             (|do [expected* (apply-type F A)]
               (check* (fp-put fp-pair true fixpoints) invariant?? expected* actual))))
 
-        [_ (&/$App (&/$Ex aid) A)]
+        [_ (&/$Apply A (&/$Ex aid))]
         (check-error "" expected actual)
 
-        [_ (&/$App F A)]
+        [_ (&/$Apply A F)]
         (|do [actual* (apply-type F A)]
           (check* fixpoints invariant?? expected actual*))
 
@@ -894,7 +895,7 @@
 (defn actual-type [type]
   "(-> Type (Lux Type))"
   (|case type
-    (&/$App ?all ?param)
+    (&/$Apply ?param ?all)
     (|do [type* (apply-type ?all ?param)]
       (actual-type type*))
 
@@ -976,24 +977,24 @@
 
 (defn ^:private push-app [inf-type inf-var]
   (|case inf-type
-    (&/$App inf-type* inf-var*)
-    (&/$App (push-app inf-type* inf-var) inf-var*)
+    (&/$Apply inf-var* inf-type*)
+    (&/$Apply inf-var* (push-app inf-type* inf-var))
 
     _
-    (&/$App inf-type inf-var)))
+    (&/$Apply inf-var inf-type)))
 
 (defn ^:private push-name [name inf-type]
   (|case inf-type
-    (&/$App inf-type* inf-var*)
-    (&/$App (push-name name inf-type*) inf-var*)
+    (&/$Apply inf-var* inf-type*)
+    (&/$Apply inf-var* (push-name name inf-type*))
 
     _
     (&/$Named name inf-type)))
 
 (defn ^:private push-univq [env inf-type]
   (|case inf-type
-    (&/$App inf-type* inf-var*)
-    (&/$App (push-univq env inf-type*) inf-var*)
+    (&/$Apply inf-var* inf-type*)
+    (&/$Apply inf-var* (push-univq env inf-type*))
 
     _
     (&/$UnivQ env inf-type)))