- Added better support for existential quantification.

- No longer requiring type-parameters in JVM interop forms.

10 files changed, 150 insertions, 107 deletions

diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 9940bb354..8959ac61b 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -43,7 +43,7 @@
     _
     (fail (str "[Analyser Error] Not a tag: " (&/show-ast ast)))))
 
-(defn ^:private extract-text [ast]
+(defn ^:private parse-text [ast]
   (|case ast
     [_ (&/$TextS text)]
     (return text)
@@ -78,18 +78,6 @@
   (fn [state]
     (fail* (add-loc (&/get$ &/$cursor state) msg))))
 
-(defn ^:private parse-generic-class [sample]
-  "(-> AST (Lux GenericClass))"
-  (|case sample
-    [_ (&/$FormS (&/$Cons [_ (&/$TextS ?name)]
-                          (&/$Cons [_ (&/$TupleS ?params)]
-                                   (&/$Nil))))]
-    (|do [=params (&/map% parse-generic-class ?params)]
-      (return (&/T ?name =params)))
-
-    _
-    (fail-with-loc (str "[Analyser Error] Wrong syntax for generic class: " (&/show-ast sample)))))
-
 (defn ^:private aba10 [analyse eval! compile-module compile-token exo-type token]
   (|case token
     ;; Arrays
@@ -203,7 +191,7 @@
                                                            (&/$Cons [_ (&/$TupleS ?fields)]
                                                                     (&/$Cons [_ (&/$TupleS ?methods)]
                                                                              (&/$Nil)))))))))
-    (|do [=interfaces (&/map% extract-text ?interfaces)]
+    (|do [=interfaces (&/map% parse-text ?interfaces)]
       (&&host/analyse-jvm-class analyse compile-token ?name ?super-class =interfaces ?anns ?fields ?methods))
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_interface")]
@@ -211,7 +199,7 @@
                                 (&/$Cons [_ (&/$TupleS ?supers)]
                                          (&/$Cons [_ (&/$TupleS ?anns)]
                                                   ?methods)))))
-    (|do [=supers (&/map% extract-text ?supers)]
+    (|do [=supers (&/map% parse-text ?supers)]
       (&&host/analyse-jvm-interface analyse compile-token ?name =supers ?anns ?methods))
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_anon-class")]
@@ -219,7 +207,7 @@
                                 (&/$Cons [_ (&/$TupleS ?interfaces)]
                                          (&/$Cons [_ (&/$TupleS ?methods)]
                                                   (&/$Nil))))))
-    (|do [=interfaces (&/map% extract-text ?interfaces)]
+    (|do [=interfaces (&/map% parse-text ?interfaces)]
       (&&host/analyse-jvm-anon-class analyse compile-token exo-type ?super-class =interfaces ?methods))
 
     ;; Programs
@@ -343,13 +331,12 @@
     (&&host/analyse-jvm-instanceof analyse exo-type ?class ?object)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_new")]
-                       (&/$Cons ?poly-class
-                                (&/$Cons [_ (&/$TupleS ?classes)]
+                       (&/$Cons [_ (&/$TextS ?class)]
+                                (&/$Cons [_ (&/$TupleS ?arg-classes)]
                                          (&/$Cons [_ (&/$TupleS ?args)]
                                                   (&/$Nil))))))
-    (|do [=generic-class (parse-generic-class ?poly-class)
-          =classes (&/map% extract-text ?classes)]
-      (&&host/analyse-jvm-new analyse exo-type =generic-class =classes ?args))
+    (|do [=arg-classes (&/map% parse-text ?arg-classes)]
+      (&&host/analyse-jvm-new analyse exo-type ?class =arg-classes ?args))
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_getstatic")]
                        (&/$Cons [_ (&/$TextS ?class)]
@@ -380,47 +367,43 @@
     (&&host/analyse-jvm-putfield analyse exo-type ?class ?field ?value ?object)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_invokestatic")]
-                       (&/$Cons ?poly-class
+                       (&/$Cons [_ (&/$TextS ?class)]
                                 (&/$Cons [_ (&/$TextS ?method)]
                                          (&/$Cons [_ (&/$TupleS ?arg-classes)]
                                                   (&/$Cons [_ (&/$TupleS ?args)]
                                                            (&/$Nil)))))))
-    (|do [=generic-class (parse-generic-class ?poly-class)
-          =arg-classes (&/map% parse-generic-class ?arg-classes)]
-      (&&host/analyse-jvm-invokestatic analyse exo-type =generic-class ?method =arg-classes ?args))
+    (|do [=arg-classes (&/map% parse-text ?arg-classes)]
+      (&&host/analyse-jvm-invokestatic analyse exo-type ?class ?method =arg-classes ?args))
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_invokevirtual")]
-                       (&/$Cons ?poly-class
+                       (&/$Cons [_ (&/$TextS ?class)]
                                 (&/$Cons [_ (&/$TextS ?method)]
                                          (&/$Cons [_ (&/$TupleS ?arg-classes)]
                                                   (&/$Cons ?object
                                                            (&/$Cons [_ (&/$TupleS ?args)]
                                                                     (&/$Nil))))))))
-    (|do [=generic-class (parse-generic-class ?poly-class)
-          =arg-classes (&/map% parse-generic-class ?arg-classes)]
-      (&&host/analyse-jvm-invokevirtual analyse exo-type =generic-class ?method =arg-classes ?object ?args))
+    (|do [=arg-classes (&/map% parse-text ?arg-classes)]
+      (&&host/analyse-jvm-invokevirtual analyse exo-type ?class ?method =arg-classes ?object ?args))
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_invokeinterface")]
-                       (&/$Cons ?poly-class
+                       (&/$Cons [_ (&/$TextS ?class)]
                                 (&/$Cons [_ (&/$TextS ?method)]
                                          (&/$Cons [_ (&/$TupleS ?arg-classes)]
                                                   (&/$Cons ?object
                                                            (&/$Cons [_ (&/$TupleS ?args)]
                                                                     (&/$Nil))))))))
-    (|do [=generic-class (parse-generic-class ?poly-class)
-          =arg-classes (&/map% parse-generic-class ?arg-classes)]
-      (&&host/analyse-jvm-invokeinterface analyse exo-type =generic-class ?method =arg-classes ?object ?args))
+    (|do [=arg-classes (&/map% parse-text ?arg-classes)]
+      (&&host/analyse-jvm-invokeinterface analyse exo-type ?class ?method =arg-classes ?object ?args))
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_invokespecial")]
-                       (&/$Cons ?poly-class
+                       (&/$Cons [_ (&/$TextS ?class)]
                                 (&/$Cons [_ (&/$TextS ?method)]
                                          (&/$Cons [_ (&/$TupleS ?arg-classes)]
                                                   (&/$Cons ?object
                                                            (&/$Cons [_ (&/$TupleS ?args)]
                                                                     (&/$Nil))))))))
-    (|do [=generic-class (parse-generic-class ?poly-class)
-          =arg-classes (&/map% parse-generic-class ?arg-classes)]
-      (&&host/analyse-jvm-invokespecial analyse exo-type =generic-class ?method =arg-classes ?object ?args))
+    (|do [=arg-classes (&/map% parse-text ?arg-classes)]
+      (&&host/analyse-jvm-invokespecial analyse exo-type ?class ?method =arg-classes ?object ?args))
 
     ;; Exceptions
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_try")]
diff --git a/src/lux/analyser/case.clj b/src/lux/analyser/case.clj
index 7e5fd924b..d975d8989 100644
--- a/src/lux/analyser/case.clj
+++ b/src/lux/analyser/case.clj
@@ -69,6 +69,11 @@
         (|do [=type (&type/apply-type type $var)]
           (adjust-type* (&/Cons$ (&/T _aenv 1 $var) (&/|map update-up-frame up)) =type))))
 
+    (&/$ExQ _aenv _abody)
+    (|do [$var &type/existential
+          =type (&type/apply-type type $var)]
+      (adjust-type* up =type))
+
     (&/$TupleT ?members)
     (|do [(&/$TupleT ?members*) (&/fold% (fn [_abody ena]
                                            (|let [[_aenv _aidx (&/$VarT _avar)] ena]
diff --git a/src/lux/analyser/env.clj b/src/lux/analyser/env.clj
index ec0dc4a92..f6a1adfc6 100644
--- a/src/lux/analyser/env.clj
+++ b/src/lux/analyser/env.clj
@@ -6,7 +6,7 @@
 (ns lux.analyser.env
   (:require clojure.core.match
             clojure.core.match.array
-            (lux [base :as & :refer [|do return return* fail |case]])
+            (lux [base :as & :refer [|do return return* fail fail* |case]])
             [lux.analyser.base :as &&]))
 
 ;; [Exports]
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index 92550f0fb..291b7c768 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -78,6 +78,10 @@
     (&/$ExQ _ type*)
     (ensure-object type*)
 
+    (&/$AppT F A)
+    (|do [type* (&type/apply-type F A)]
+      (ensure-object type*))
+
     _
     (fail (str "[Analyser Error] Expecting object: " (&type/show-type type)))))
 
@@ -113,6 +117,23 @@
     _
     type))
 
+(defn ^:private clean-gtype-var [idx gtype-var]
+  (|let [(&/$VarT id) gtype-var]
+    (|do [? (&type/bound? id)]
+      (if ?
+        (|do [real-type (&type/deref id)]
+          (return (&/T idx real-type)))
+        (return (&/T (+ 2 idx) (&type/Bound$ idx)))))))
+
+(defn ^:private clean-gtype-vars [gtype-vars]
+  (|do [[_ clean-types] (&/fold% (fn [idx+types gtype-var]
+                                   (|do [:let [[idx types] idx+types]
+                                         [idx* real-type] (clean-gtype-var idx gtype-var)]
+                                     (return (&/T idx* (&/Cons$ real-type types)))))
+                                 (&/T 1 (&/|list))
+                                 gtype-vars)]
+    (return clean-types)))
+
 (defn ^:private make-gtype [class-name type-args]
   "(-> Text (List Type) Type)"
   (&/fold (fn [base-type type-arg]
@@ -248,11 +269,7 @@
     (return (&/|list (&&/|meta output-type _cursor
                                (&/V &&/$jvm-instanceof (&/T class =object)))))))
 
-(defn ^:private instance-generic-type [desc]
-  (|let [[gc-name gc-params] desc]
-    (&type/Data$ gc-name (&/|map instance-generic-type gc-params))))
-
-(defn ^:private analyse-method-call-helper [analyse gret gc-params gtype-env gtype-vars gtype-args args]
+(defn ^:private analyse-method-call-helper [analyse gret gtype-env gtype-vars gtype-args args]
   (|case gtype-vars
     (&/$Nil)
     (|do [arg-types (&/map% (partial &host-type/instance-param &type/existential gtype-env) gtype-args)
@@ -261,60 +278,59 @@
       (return (&/T =gret =args)))
     
     (&/$Cons ^TypeVariable gtv gtype-vars*)
-    (|let [gtype-env* (&/Cons$ (&/T (.getName gtv) (->> gc-params &/|head instance-generic-type))
-                               gtype-env)]
-      (analyse-method-call-helper analyse gret (&/|tail gc-params) gtype-env* gtype-vars* gtype-args args))
+    (&type/with-var
+      (fn [$var]
+        (|let [gtype-env* (&/Cons$ (&/T (.getName gtv) $var) gtype-env)]
+          (analyse-method-call-helper analyse gret gtype-env* gtype-vars* gtype-args args))))
     ))
 
 (let [dummy-type-param (&type/Data$ "java.lang.Object" (&/|list))]
   (do-template [<name> <tag> <only-interface?>]
-    (defn <name> [analyse exo-type generic-class method arg-classes object args]
+    (defn <name> [analyse exo-type class method classes object args]
       (|do [class-loader &/loader
-            :let [[gc-name gc-params] generic-class]
-            _ (try (assert! (let [=class (Class/forName gc-name true class-loader)]
+            _ (try (assert! (let [=class (Class/forName class true class-loader)]
                               (= <only-interface?> (.isInterface =class)))
                             (if <only-interface?>
                               (str "[Analyser Error] Can only invoke method \"" method "\"" " on interface.")
                               (str "[Analyser Error] Can only invoke method \"" method "\"" " on class.")))
                 (catch Exception e
-                  (fail (str "[Analyser Error] Unknown class: " gc-name))))
+                  (fail (str "[Analyser Error] Unknown class: " class))))
             [gret exceptions parent-gvars gvars gargs] (if (= "<init>" method)
                                                          (return (&/T Void/TYPE &/Nil$ &/Nil$ &/Nil$ &/Nil$))
-                                                         (&host/lookup-virtual-method class-loader gc-name method arg-classes))
+                                                         (&host/lookup-virtual-method class-loader class method classes))
             _ (ensure-catching exceptions)
             =object (&&/analyse-1+ analyse object)
             [sub-class sub-params] (ensure-object (&&/expr-type* =object))
-            (&/$DataT super-class* super-params*) (&host-type/->super-type &type/existential class-loader gc-name sub-class sub-params)
-            :let [_ (prn '<name> sub-class '-> super-class* (&/|length parent-gvars) (&/|length super-params*))
+            (&/$DataT super-class* super-params*) (&host-type/->super-type &type/existential class-loader class sub-class sub-params)
+            :let [;; _ (prn '<name> sub-class '-> super-class* (&/|length parent-gvars) (&/|length super-params*))
                   gtype-env (&/fold2 (fn [m ^TypeVariable g t] (&/Cons$ (&/T (.getName g) t) m))
                                      (&/|table)
                                      parent-gvars
                                      super-params*)]
-            [output-type =args] (analyse-method-call-helper analyse gret gc-params gtype-env gvars gargs args)
+            [output-type =args] (analyse-method-call-helper analyse gret gtype-env gvars gargs args)
             _ (&type/check exo-type (as-otype+ output-type))
             _cursor &/cursor]
         (return (&/|list (&&/|meta exo-type _cursor
-                                   (&/V <tag> (&/T gc-name method arg-classes =object =args output-type)))))))
+                                   (&/V <tag> (&/T class method classes =object =args output-type)))))))
 
     analyse-jvm-invokevirtual   &&/$jvm-invokevirtual   false
     analyse-jvm-invokespecial   &&/$jvm-invokespecial   false
     analyse-jvm-invokeinterface &&/$jvm-invokeinterface true
     ))
 
-(defn analyse-jvm-invokestatic [analyse exo-type generic-class method arg-classes args]
+(defn analyse-jvm-invokestatic [analyse exo-type class method classes args]
   (|do [class-loader &/loader
-        :let [[gc-name gc-params] generic-class]
-        [gret exceptions parent-gvars gvars gargs] (&host/lookup-static-method class-loader gc-name method arg-classes)
+        [gret exceptions parent-gvars gvars gargs] (&host/lookup-static-method class-loader class method classes)
         _ (ensure-catching exceptions)
         =args (&/map2% (fn [_class _arg]
                          (&&/analyse-1 analyse (&host-type/class-name->type _class) _arg))
-                       arg-classes
+                       classes
                        args)
-        :let [output-type (&host-type/class->type (cast Class gret))]
+        output-type (&host-type/instance-param &type/existential (&/|table) gret)
         _ (&type/check exo-type (as-otype+ output-type))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
-                               (&/V &&/$jvm-invokestatic (&/T gc-name method arg-classes =args output-type)))))))
+                               (&/V &&/$jvm-invokestatic (&/T class method classes =args output-type)))))))
 
 (defn analyse-jvm-null? [analyse exo-type object]
   (|do [=object (&&/analyse-1+ analyse object)
@@ -332,32 +348,31 @@
     (return (&/|list (&&/|meta output-type _cursor
                                (&/V &&/$jvm-null nil))))))
 
-(defn ^:private analyse-jvm-new-helper [analyse gc-name gc-params gtype-env gtype-vars gtype-args args]
-  (prn 'analyse-jvm-new-helper gc-name (&/->seq gc-params) (&/->seq (&/|map #(.getName ^TypeVariable %) gtype-vars)))
+(defn ^:private analyse-jvm-new-helper [analyse gtype gtype-env gtype-vars gtype-args args]
   (|case gtype-vars
     (&/$Nil)
     (|do [arg-types (&/map% (partial &host-type/instance-param &type/existential gtype-env) gtype-args)
           =args (&/map2% (partial &&/analyse-1 analyse) arg-types args)
-          :let [gtype-vars* (->> gtype-env (&/|map &/|second))]]
-      (return (&/T (make-gtype gc-name gtype-vars*)
+          gtype-vars* (->> gtype-env (&/|map &/|second) (clean-gtype-vars))]
+      (return (&/T (make-gtype gtype gtype-vars*)
                    =args)))
     
     (&/$Cons ^TypeVariable gtv gtype-vars*)
-    (|let [gtype-env* (&/Cons$ (&/T (.getName gtv) (->> gc-params &/|head instance-generic-type))
-                               gtype-env)]
-      (analyse-jvm-new-helper analyse gc-name (&/|tail gc-params) gtype-env* gtype-vars* gtype-args args))
+    (&type/with-var
+      (fn [$var]
+        (|let [gtype-env* (&/Cons$ (&/T (.getName gtv) $var) gtype-env)]
+          (analyse-jvm-new-helper analyse gtype gtype-env* gtype-vars* gtype-args args))))
     ))
 
-(defn analyse-jvm-new [analyse exo-type generic-class arg-classes args]
+(defn analyse-jvm-new [analyse exo-type class classes args]
   (|do [class-loader &/loader
-        :let [[gc-name gc-params] generic-class]
-        [exceptions gvars gargs] (&host/lookup-constructor class-loader gc-name arg-classes)
+        [exceptions gvars gargs] (&host/lookup-constructor class-loader class classes)
         _ (ensure-catching exceptions)
-        [output-type =args] (analyse-jvm-new-helper analyse gc-name gc-params (&/|table) gvars gargs args)
+        [output-type =args] (analyse-jvm-new-helper analyse class (&/|table) gvars gargs args)
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
-                               (&/V &&/$jvm-new (&/T gc-name arg-classes =args)))))))
+                               (&/V &&/$jvm-new (&/T class classes =args)))))))
 
 (let [length-type &type/Int
       idx-type &type/Int]
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index f7e138e45..5e47e2361 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -192,6 +192,12 @@
         (|do [$var &type/existential
               exo-type** (&type/apply-type exo-type* $var)]
           (analyse-variant analyse (&/V &/$Right exo-type**) idx ?values))
+
+        (&/$ExQ _)
+        (&type/with-var
+          (fn [$var]
+            (|do [exo-type** (&type/apply-type exo-type* $var)]
+              (analyse-variant analyse (&/V &/$Right exo-type**) idx ?values))))
         
         _
         (fail (str "[Analyser Error] Can't create a variant if the expected type is " (&type/show-type exo-type*)))))))
@@ -320,6 +326,11 @@
                   (return (&/T type** =args)))
                 ))))
 
+        (&/$ExQ _)
+        (|do [$var &type/existential
+              type* (&type/apply-type ?fun-type* $var)]
+          (analyse-apply* analyse exo-type type* ?args))
+
         (&/$LambdaT ?input-t ?output-t)
         (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*)
               =arg (with-attempt
@@ -343,14 +354,15 @@
           (|case $def
             (&/$MacroD macro)
             (|do [macro-expansion #(-> macro (.apply ?args) (.apply %))
-                  ;; :let [_ (when (or (= "do" (aget real-name 1))
-                  ;;                   ;; (= "..?" (aget real-name 1))
-                  ;;                   ;; (= "try$" (aget real-name 1))
-                  ;;                   )
-                  ;;           (->> (&/|map &/show-ast macro-expansion)
-                  ;;                (&/|interpose "\n")
-                  ;;                (&/fold str "")
-                  ;;                (prn (&/ident->text real-name))))]
+                  :let [_ (when (or (= "invoke-static$" (aget real-name 1))
+                                    (= "invoke-virtual$" (aget real-name 1))
+                                    (= "new$" (aget real-name 1))
+                                    (= "let%" (aget real-name 1))
+                                    (= "jvm-import" (aget real-name 1)))
+                            (->> (&/|map &/show-ast macro-expansion)
+                                 (&/|interpose "\n")
+                                 (&/fold str "")
+                                 (prn (&/ident->text real-name))))]
                   ]
               (&/flat-map% (partial analyse exo-type) macro-expansion))
 
@@ -423,6 +435,12 @@
         (|do [$var &type/existential
               exo-type** (&type/apply-type exo-type* $var)]
           (analyse-lambda* analyse exo-type** ?self ?arg ?body))
+
+        (&/$ExQ _)
+        (&type/with-var
+          (fn [$var]
+            (|do [exo-type** (&type/apply-type exo-type* $var)]
+              (analyse-lambda* analyse exo-type** ?self ?arg ?body))))
         
         (&/$LambdaT ?arg-t ?return-t)
         (|do [[=scope =captured =body] (&&lambda/with-lambda ?self exo-type*
diff --git a/src/lux/base.clj b/src/lux/base.clj
index b8ca60465..e3c6dcd5b 100644
--- a/src/lux/base.clj
+++ b/src/lux/base.clj
@@ -1000,7 +1000,7 @@
   |any?   false or)
 
 (defn m-comp [f g]
-  (All [a b c] (-> (-> b (Lux c)) (-> a (Lux b)) (-> a (Lux c))))
+  "(All [a b c] (-> (-> b (Lux c)) (-> a (Lux b)) (-> a (Lux c))))"
   (fn [x]
     (|do [y (g x)]
       (f y))))
diff --git a/src/lux/compiler/host.clj b/src/lux/compiler/host.clj
index 6b05f0c8a..f06852ae9 100644
--- a/src/lux/compiler/host.clj
+++ b/src/lux/compiler/host.clj
@@ -203,7 +203,8 @@
 
 (defn compile-jvm-invokestatic [compile ?class ?method ?classes ?args ?output-type]
   (|do [^MethodVisitor *writer* &/get-writer
-        :let [method-sig (str "(" (&/fold str "" (&/|map &host/->type-signature ?classes)) ")" (&host/->java-sig ?output-type))]
+        =output-type (&host/->java-sig ?output-type)
+        :let [method-sig (str "(" (&/fold str "" (&/|map &host/->type-signature ?classes)) ")" =output-type)]
         _ (&/map2% (fn [class-name arg]
                      (|do [ret (compile arg)
                            :let [_ (prepare-arg! *writer* class-name)]]
@@ -218,7 +219,8 @@
   (defn <name> [compile ?class ?method ?classes ?object ?args ?output-type]
     (|do [:let [?class* (&host/->class (&host-type/as-obj ?class))]
           ^MethodVisitor *writer* &/get-writer
-          :let [method-sig (str "(" (&/fold str "" (&/|map &host/->type-signature ?classes)) ")" (&host/->java-sig ?output-type))]
+          =output-type (&host/->java-sig ?output-type)
+          :let [method-sig (str "(" (&/fold str "" (&/|map &host/->type-signature ?classes)) ")" =output-type)]
           _ (compile ?object)
           :let [_ (when (not= "<init>" ?method)
                     (.visitTypeInsn *writer* Opcodes/CHECKCAST ?class*))]
@@ -362,8 +364,9 @@
 
 (defn compile-jvm-getstatic [compile ?class ?field ?output-type]
   (|do [^MethodVisitor *writer* &/get-writer
+        =output-type (&host/->java-sig ?output-type)
         :let [_ (doto *writer*
-                  (.visitFieldInsn Opcodes/GETSTATIC (&host/->class (&host-type/as-obj ?class)) ?field (&host/->java-sig ?output-type))
+                  (.visitFieldInsn Opcodes/GETSTATIC (&host/->class (&host-type/as-obj ?class)) ?field =output-type)
                   (prepare-return! ?output-type))]]
     (return nil)))
 
@@ -371,16 +374,18 @@
   (|do [:let [class* (&host/->class (&host-type/as-obj ?class))]
         ^MethodVisitor *writer* &/get-writer
         _ (compile ?object)
+        =output-type (&host/->java-sig ?output-type)
         :let [_ (doto *writer*
                   (.visitTypeInsn Opcodes/CHECKCAST class*)
-                  (.visitFieldInsn Opcodes/GETFIELD class* ?field (&host/->java-sig ?output-type))
+                  (.visitFieldInsn Opcodes/GETFIELD class* ?field =output-type)
                   (prepare-return! ?output-type))]]
     (return nil)))
 
 (defn compile-jvm-putstatic [compile ?class ?field ?value ?output-type]
   (|do [^MethodVisitor *writer* &/get-writer
         _ (compile ?value)
-        :let [_ (.visitFieldInsn *writer* Opcodes/PUTSTATIC (&host/->class (&host-type/as-obj ?class)) ?field (&host/->java-sig ?output-type))]
+        =output-type (&host/->java-sig ?output-type)
+        :let [_ (.visitFieldInsn *writer* Opcodes/PUTSTATIC (&host/->class (&host-type/as-obj ?class)) ?field =output-type)]
         :let [_ (.visitInsn *writer* Opcodes/ACONST_NULL)]]
     (return nil)))
 
@@ -391,7 +396,8 @@
         :let [_ (.visitInsn *writer* Opcodes/DUP)]
         _ (compile ?value)
         :let [_ (.visitTypeInsn *writer* Opcodes/CHECKCAST class*)]
-        :let [_ (.visitFieldInsn *writer* Opcodes/PUTFIELD class* ?field (&host/->java-sig ?output-type))]]
+        =output-type (&host/->java-sig ?output-type)
+        :let [_ (.visitFieldInsn *writer* Opcodes/PUTFIELD class* ?field =output-type)]]
     (return nil)))
 
 (defn compile-jvm-instanceof [compile class object]
diff --git a/src/lux/compiler/lux.clj b/src/lux/compiler/lux.clj
index a2dc3fe73..508ca8a5f 100644
--- a/src/lux/compiler/lux.clj
+++ b/src/lux/compiler/lux.clj
@@ -217,9 +217,9 @@
 
 (defn check-cast [type]
   "(-> Type (Lux (,)))"
-  (|do [^MethodVisitor writer &/get-writer]
-    (let [^String type-class* (&host/->java-sig type)
-          type-class (cond (.startsWith type-class* "[")
+  (|do [^MethodVisitor writer &/get-writer
+        ^String type-class* (&host/->java-sig type)]
+    (let [type-class (cond (.startsWith type-class* "[")
                            type-class*
                            
                            (.endsWith type-class* ";")
diff --git a/src/lux/host.clj b/src/lux/host.clj
index 12af574fb..310024700 100644
--- a/src/lux/host.clj
+++ b/src/lux/host.clj
@@ -69,36 +69,40 @@
 
 (let [object-array (str "[" "L" (->class "java.lang.Object") ";")]
   (defn ->java-sig [^objects type]
-    "(-> Type Text)"
+    "(-> Type (Lux Text))"
     (|case type
       (&/$DataT ?name params)
-      (cond (= &host-type/array-data-tag ?name) (|let [[level base] (unfold-array type)
-                                                       base-sig (|case base
-                                                                  (&/$DataT base-class _)
-                                                                  (->type-signature base-class)
-
-                                                                  _
-                                                                  (->java-sig base))]
-                                                  (str (->> (&/|repeat level "[") (&/fold str ""))
-                                                       base-sig))
-            (= &host-type/null-data-tag ?name)  (->type-signature "java.lang.Object")
-            :else                    (->type-signature ?name))
+      (cond (= &host-type/array-data-tag ?name) (|do [:let [[level base] (unfold-array type)]
+                                                      base-sig (|case base
+                                                                 (&/$DataT base-class _)
+                                                                 (return (->type-signature base-class))
+
+                                                                 _
+                                                                 (->java-sig base))]
+                                                  (return (str (->> (&/|repeat level "[") (&/fold str ""))
+                                                               base-sig)))
+            (= &host-type/null-data-tag ?name)  (return (->type-signature "java.lang.Object"))
+            :else                               (return (->type-signature ?name)))
 
       (&/$LambdaT _ _)
-      (->type-signature function-class)
+      (return (->type-signature function-class))
 
       (&/$TupleT (&/$Nil))
-      "V"
+      (return "V")
 
       (&/$VariantT _)
-      object-array
+      (return object-array)
 
       (&/$TupleT _)
-      object-array
+      (return object-array)
 
       (&/$NamedT ?name ?type)
       (->java-sig ?type)
 
+      (&/$AppT ?F ?A)
+      (|do [type* (&type/apply-type ?F ?A)]
+        (->java-sig type*))
+
       _
       (assert false (str '->java-sig " " (&type/show-type type)))
       )))
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 6ae542b68..80316f039 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -322,6 +322,9 @@
     
     (&/$UnivQ ?env ?body)
     (str "(All " (show-type ?body) ")")
+
+    (&/$ExQ ?env ?body)
+    (str "(Ex " (show-type ?body) ")")
     
     (&/$NamedT ?name ?type)
     (&/ident->text ?name)
@@ -404,6 +407,9 @@
 
 (defn beta-reduce [env type]
   (|case type
+    (&/$DataT ?name ?params)
+    (Data$ ?name (&/|map (partial beta-reduce env) ?params))
+
     (&/$VariantT ?members)
     (Variant$ (&/|map (partial beta-reduce env) ?members))
 
@@ -444,6 +450,12 @@
                               (&/Cons$ type-fn))
                          local-def))
 
+    (&/$ExQ local-env local-def)
+    (return (beta-reduce (->> local-env
+                              (&/Cons$ param)
+                              (&/Cons$ type-fn))
+                         local-def))
+
     (&/$AppT F A)
     (|do [type-fn* (apply-type F A)]
       (apply-type type-fn* param))