- Added generics support for object field access (getting & setting).

- Added generics support for object method invocation.

6 files changed, 319 insertions, 234 deletions

diff --git a/source/lux/host/jvm.lux b/source/lux/host/jvm.lux
index 57d0e9c5d..cb818eb2b 100644
--- a/source/lux/host/jvm.lux
+++ b/source/lux/host/jvm.lux
@@ -256,6 +256,7 @@
   (_jvm_invokevirtual "java.lang.Throwable" "getStackTrace" [] t []))
 
 (def #export (throwable->text t)
+  (-> (^ java.lang.Throwable) Text)
   ($ text:++
     (_jvm_invokevirtual "java.lang.Object" "toString" [] t [])
     "\n"
diff --git a/src/lux/analyser.clj b/src/lux/analyser.clj
index 0aa883c23..4e1093cec 100644
--- a/src/lux/analyser.clj
+++ b/src/lux/analyser.clj
@@ -72,88 +72,88 @@
   (|case token
     ;; Arrays
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_znewarray")] (&/$Cons ?length (&/$Nil))))
-    (&&host/analyse-jvm-znewarray analyse ?length)
+    (&&host/analyse-jvm-znewarray analyse exo-type ?length)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_zastore")] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil))))))
-    (&&host/analyse-jvm-zastore analyse ?array ?idx ?elem)
+    (&&host/analyse-jvm-zastore analyse exo-type ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_zaload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
-    (&&host/analyse-jvm-zaload analyse ?array ?idx)
+    (&&host/analyse-jvm-zaload analyse exo-type ?array ?idx)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_bnewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
-    (&&host/analyse-jvm-bnewarray analyse ?length)
+    (&&host/analyse-jvm-bnewarray analyse exo-type ?length)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_bastore")] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil))))))
-    (&&host/analyse-jvm-bastore analyse ?array ?idx ?elem)
+    (&&host/analyse-jvm-bastore analyse exo-type ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_baload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
-    (&&host/analyse-jvm-baload analyse ?array ?idx)
+    (&&host/analyse-jvm-baload analyse exo-type ?array ?idx)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_snewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
-    (&&host/analyse-jvm-snewarray analyse ?length)
+    (&&host/analyse-jvm-snewarray analyse exo-type ?length)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_sastore")] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil))))))
-    (&&host/analyse-jvm-sastore analyse ?array ?idx ?elem)
+    (&&host/analyse-jvm-sastore analyse exo-type ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_saload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
-    (&&host/analyse-jvm-saload analyse ?array ?idx)
+    (&&host/analyse-jvm-saload analyse exo-type ?array ?idx)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_inewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
-    (&&host/analyse-jvm-inewarray analyse ?length)
+    (&&host/analyse-jvm-inewarray analyse exo-type ?length)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_iastore")] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil))))))
-    (&&host/analyse-jvm-iastore analyse ?array ?idx ?elem)
+    (&&host/analyse-jvm-iastore analyse exo-type ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_iaload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
-    (&&host/analyse-jvm-iaload analyse ?array ?idx)
+    (&&host/analyse-jvm-iaload analyse exo-type ?array ?idx)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_lnewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
-    (&&host/analyse-jvm-lnewarray analyse ?length)
+    (&&host/analyse-jvm-lnewarray analyse exo-type ?length)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_lastore")] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil))))))
-    (&&host/analyse-jvm-lastore analyse ?array ?idx ?elem)
+    (&&host/analyse-jvm-lastore analyse exo-type ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_laload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
-    (&&host/analyse-jvm-laload analyse ?array ?idx)
+    (&&host/analyse-jvm-laload analyse exo-type ?array ?idx)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_fnewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
-    (&&host/analyse-jvm-fnewarray analyse ?length)
+    (&&host/analyse-jvm-fnewarray analyse exo-type ?length)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_fastore")] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil))))))
-    (&&host/analyse-jvm-fastore analyse ?array ?idx ?elem)
+    (&&host/analyse-jvm-fastore analyse exo-type ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_faload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
-    (&&host/analyse-jvm-faload analyse ?array ?idx)
+    (&&host/analyse-jvm-faload analyse exo-type ?array ?idx)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_dnewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
-    (&&host/analyse-jvm-dnewarray analyse ?length)
+    (&&host/analyse-jvm-dnewarray analyse exo-type ?length)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_dastore")] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil))))))
-    (&&host/analyse-jvm-dastore analyse ?array ?idx ?elem)
+    (&&host/analyse-jvm-dastore analyse exo-type ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_daload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
-    (&&host/analyse-jvm-daload analyse ?array ?idx)
+    (&&host/analyse-jvm-daload analyse exo-type ?array ?idx)
     
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_cnewarray")] (&/$Cons [_ (&/$SymbolS _ ?class)] (&/$Cons ?length (&/$Nil)))))
-    (&&host/analyse-jvm-cnewarray analyse ?length)
+    (&&host/analyse-jvm-cnewarray analyse exo-type ?length)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_castore")] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil))))))
-    (&&host/analyse-jvm-castore analyse ?array ?idx ?elem)
+    (&&host/analyse-jvm-castore analyse exo-type ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_caload")] (&/$Cons ?array (&/$Cons ?idx (&/$Nil)))))
-    (&&host/analyse-jvm-caload analyse ?array ?idx)
+    (&&host/analyse-jvm-caload analyse exo-type ?array ?idx)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_anewarray")] (&/$Cons [_ (&/$TextS ?class)] (&/$Cons ?length (&/$Nil)))))
-    (&&host/analyse-jvm-anewarray analyse ?class ?length)
+    (&&host/analyse-jvm-anewarray analyse exo-type ?class ?length)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_aastore")] (&/$Cons [_ (&/$TextS ?class)] (&/$Cons ?array (&/$Cons ?idx (&/$Cons ?elem (&/$Nil)))))))
-    (&&host/analyse-jvm-aastore analyse ?class ?array ?idx ?elem)
+    (&&host/analyse-jvm-aastore analyse exo-type ?class ?array ?idx ?elem)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_aaload")] (&/$Cons [_ (&/$TextS ?class)] (&/$Cons ?array (&/$Cons ?idx (&/$Nil))))))
-    (&&host/analyse-jvm-aaload analyse ?class ?array ?idx)
+    (&&host/analyse-jvm-aaload analyse exo-type ?class ?array ?idx)
 
     (&/$FormS (&/$Cons [_ (&/$SymbolS _ "_jvm_arraylength")] (&/$Cons ?array (&/$Nil))))
-    (&&host/analyse-jvm-arraylength analyse ?array)
+    (&&host/analyse-jvm-arraylength analyse exo-type ?array)
 
     _
     (do (prn 'aba8 (&/adt->text token))
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index 9490c37c8..cf361da22 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -69,14 +69,23 @@
                                output)))))
     ))
 
-(defn ^:private ensure-object [token]
-  "(-> Analysis (Lux (,)))"
-  (|case token
-    [_ (&/$DataT _ _)]
-    (return nil)
+(defn ^:private ensure-object [type]
+  "(-> Type (Lux (, Text (List Type))))"
+  (|case type
+    (&/$DataT payload)
+    (return payload)
+
+    (&/$NamedT _ type*)
+    (ensure-object type*)
+
+    (&/$UnivQ _ type*)
+    (ensure-object type*)
+
+    (&/$ExQ _ type*)
+    (ensure-object type*)
 
     _
-    (fail "[Analyser Error] Expecting object")))
+    (fail (str "[Analyser Error] Expecting object: " (&type/show-type type)))))
 
 (defn ^:private as-object [type]
   "(-> Type Type)"
@@ -110,6 +119,35 @@
     _
     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 0 (&/|list))
+                                 gtype-vars)]
+    (return clean-types)))
+
+(defn ^:private make-gtype [class-name type-args]
+  "(-> Text (List Type) Type)"
+  (&/fold (fn [base-type type-arg]
+            (|case type-arg
+              (&/$BoundT _)
+              (&type/Univ$ &type/empty-env base-type)
+              
+              _
+              base-type))
+          (&type/Data$ class-name type-args)
+          type-args))
+
 ;; [Resources]
 (do-template [<name> <output-tag> <input-class> <output-class>]
   (let [input-type (&type/Data$ <input-class> &/Nil$)
@@ -163,117 +201,142 @@
   analyse-jvm-dgt  &&/$jvm-dgt  "java.lang.Double"  "java.lang.Boolean"
   )
 
+(defn ^:private analyse-field-access-helper [obj-type gvars gtype]
+  "(-> Type (List (^ java.lang.reflect.Type)) (^ java.lang.reflect.Type) (Lux Type))"
+  (|case obj-type
+    (&/$DataT class targs)
+    (if (= (&/|length targs) (&/|length gvars))
+      (|let [gtype-env (&/fold2 (fn [m g t] (&/Cons$ (&/T (.getName g) t) m))
+                                (&/|table)
+                                gvars
+                                targs)]
+        (&host-type/instance-param &type/existential gtype-env gtype))
+      (fail (str "[Type Error] Mismatched number of type-parameters: " (&/|length gvars) " - " (&type/show-type obj-type))))
+
+    _
+    (fail (str "[Type Error] Type is not an object type: " (&type/show-type obj-type)))))
+
 (defn analyse-jvm-getstatic [analyse exo-type class field]
   (|do [class-loader &/loader
-        =type (&host/lookup-static-field class-loader class field)
+        [gvars gtype] (&host/lookup-static-field class-loader class field)
+        ;; :let [_ (prn 'analyse-jvm-getstatic class field (&/->seq gvars) gtype)]
+        :let [=type (&host-type/class->type (cast Class gtype))]
         :let [output-type =type]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
-    (return (&/|list (&&/|meta output-type _cursor
+    (return (&/|list (&&/|meta exo-type _cursor
                                (&/V &&/$jvm-getstatic (&/T class field output-type)))))))
 
 (defn analyse-jvm-getfield [analyse exo-type class field object]
   (|do [class-loader &/loader
-        =type (&host/lookup-static-field class-loader class field)
         =object (&&/analyse-1 analyse object)
+        _ (ensure-object (&&/expr-type* =object))
+        [gvars gtype] (&host/lookup-field class-loader class field)
+        =type (analyse-field-access-helper (&&/expr-type* =object) gvars gtype)
         :let [output-type =type]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
-    (return (&/|list (&&/|meta output-type _cursor
+    (return (&/|list (&&/|meta exo-type _cursor
                                (&/V &&/$jvm-getfield (&/T class field =object output-type)))))))
 
 (defn analyse-jvm-putstatic [analyse exo-type class field value]
   (|do [class-loader &/loader
-        =type (&host/lookup-static-field class-loader class field)
+        [gvars gtype] (&host/lookup-static-field class-loader class field)
+        :let [=type (&host-type/class->type (cast Class gtype))]
         =value (&&/analyse-1 analyse =type value)
         :let [output-type &type/Unit]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
-    (return (&/|list (&&/|meta output-type _cursor
+    (return (&/|list (&&/|meta exo-type _cursor
                                (&/V &&/$jvm-putstatic (&/T class field =value output-type)))))))
 
 (defn analyse-jvm-putfield [analyse exo-type class field value object]
   (|do [class-loader &/loader
-        =type (&host/lookup-static-field class-loader class field)
         =object (&&/analyse-1 analyse object)
+        _ (ensure-object (&&/expr-type* =object))
+        [gvars gtype] (&host/lookup-field class-loader class field)
+        =type (analyse-field-access-helper (&&/expr-type* =object) gvars gtype)
         =value (&&/analyse-1 analyse =type value)
         :let [output-type &type/Unit]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
-    (return (&/|list (&&/|meta output-type _cursor
+    (return (&/|list (&&/|meta exo-type _cursor
                                (&/V &&/$jvm-putfield (&/T class field =value =object (&&/expr-type* =object))))))))
 
-(defn analyse-jvm-invokestatic [analyse exo-type class method classes args]
-  (|do [class-loader &/loader
-        =return+exceptions (&host/lookup-static-method class-loader class method classes)
-        :let [[=return exceptions] =return+exceptions]
-        ;; :let [_ (prn 'analyse-jvm-invokestatic (&/adt->text =return+exceptions))]
-        _ (ensure-catching exceptions)
-        ;; :let [_ (matchv ::M/objects [=return]
-        ;;           [[&/$DataT _return-class &/Nil$]]
-        ;;           (prn 'analyse-jvm-invokestatic class method _return-class))]
-        =args (&/map2% (fn [_class _arg]
-                         (&&/analyse-1 analyse (&type/Data$ _class &/Nil$) _arg))
-                       classes
-                       args)
-        :let [output-type =return]
-        _ (&type/check exo-type (as-otype+ output-type))
-        _cursor &/cursor]
-    (return (&/|list (&&/|meta output-type _cursor
-                               (&/V &&/$jvm-invokestatic (&/T class method classes =args output-type)))))))
-
 (defn analyse-jvm-instanceof [analyse exo-type class object]
   (|do [=object (&&/analyse-1+ analyse object)
-        _ (ensure-object =object)
+        _ (ensure-object (&&/expr-type* =object))
         :let [output-type &type/Bool]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
     (return (&/|list (&&/|meta output-type _cursor
                                (&/V &&/$jvm-instanceof (&/T class =object)))))))
 
-(do-template [<name> <tag>]
-  (defn <name> [analyse exo-type class method classes object args]
-    (|do [class-loader &/loader
-          =return+exceptions (&host/lookup-virtual-method class-loader class method classes)
-          ;; :let [_ (prn '<name> [class method] (&/adt->text =return+exceptions))]
-          :let [[=return exceptions] =return+exceptions]
-          _ (ensure-catching exceptions)
-          =object (&&/analyse-1 analyse (&type/Data$ class &/Nil$) object)
-          =args (&/map2% (fn [c o] (&&/analyse-1 analyse (&type/Data$ c &/Nil$) o))
-                         classes args)
-          :let [output-type =return]
-          ;; :let [_ (prn '<name> [class method] '=return (&type/show-type =return))]
-          ;; :let [_ (prn '<name> '(as-otype+ output-type) (&type/show-type (as-otype+ output-type)))]
-          _ (&type/check exo-type (as-otype+ output-type))
-          _cursor &/cursor]
-      (return (&/|list (&&/|meta output-type _cursor
-                                 (&/V <tag> (&/T class method classes =object =args output-type)))))))
+(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)
+          =args (&/map2% (partial &&/analyse-1 analyse) arg-types args)
+          =gret (&host-type/instance-param &type/existential gtype-env gret)]
+      (return (&/T =gret =args)))
+    
+    (&/$Cons ^TypeVariable gtv gtype-vars*)
+    (&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))))
+    ))
 
-  analyse-jvm-invokevirtual   &&/$jvm-invokevirtual
-  analyse-jvm-invokeinterface &&/$jvm-invokeinterface
-  )
+(let [dummy-type-param (&type/Data$ "java.lang.Object" (&/|list))]
+  (do-template [<name> <tag>]
+    (defn <name> [analyse exo-type class method classes object args]
+      (|do [class-loader &/loader
+            [gret exceptions parent-gvars gvars gargs] (if (= "<init>" method)
+                                                         (return (&/T Void/TYPE &/Nil$ &/Nil$ &/Nil$ &/Nil$))
+                                                         (&host/lookup-virtual-method class-loader class method classes))
+            ;; :let [_ (prn '<name> [class method] (&/adt->text =return+exceptions))]
+            _ (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 class sub-class sub-params)
+            :let [gtype-env (&/fold2 (fn [m g t] (&/Cons$ (&/T g t) m))
+                                     (&/|table)
+                                     parent-gvars
+                                     super-params*)]
+            [output-type =args] (analyse-method-call-helper analyse gret gtype-env gvars gargs args)
+            ;; :let [_ (prn '<name> [class method] (&type/show-type exo-type) (&type/show-type output-type))]
+            ;; :let [_ (prn '<name> '(as-otype+ output-type) (&type/show-type (as-otype+ output-type)))]
+            _ (&type/check exo-type (as-otype+ output-type))
+            _cursor &/cursor]
+        (return (&/|list (&&/|meta exo-type _cursor
+                                   (&/V <tag> (&/T class method classes =object =args output-type)))))))
+
+    analyse-jvm-invokevirtual   &&/$jvm-invokevirtual
+    analyse-jvm-invokeinterface &&/$jvm-invokeinterface
+    analyse-jvm-invokespecial   &&/$jvm-invokespecial
+    ))
 
-(defn analyse-jvm-invokespecial [analyse exo-type class method classes object args]
+(defn analyse-jvm-invokestatic [analyse exo-type class method classes args]
   (|do [class-loader &/loader
-        =return+exceptions (if (= "<init>" method)
-                             (return (&/T &type/Unit &/Nil$))
-                             (&host/lookup-virtual-method class-loader class method classes))
-        :let [[=return exceptions] =return+exceptions]
-        ;; :let [_ (prn 'analyse-jvm-invokespecial (&/adt->text =return+exceptions))]
+        [gret exceptions parent-gvars gvars gargs] (&host/lookup-static-method class-loader class method classes)
+        ;; :let [_ (prn 'analyse-jvm-invokestatic (&/adt->text =return+exceptions))]
         _ (ensure-catching exceptions)
-        =object (&&/analyse-1 analyse (&type/Data$ class &/Nil$) object)
-        =args (&/map2% (fn [c o]
-                         (&&/analyse-1 analyse (&type/Data$ c &/Nil$) o))
-                       classes args)
-        :let [output-type =return]
+        ;; :let [_ (matchv ::M/objects [=return]
+        ;;           [[&/$DataT _return-class &/Nil$]]
+        ;;           (prn 'analyse-jvm-invokestatic class method _return-class))]
+        =args (&/map2% (fn [_class _arg]
+                         (&&/analyse-1 analyse (&type/Data$ _class &/Nil$) _arg))
+                       classes
+                       args)
+        :let [output-type (&host-type/class->type (cast Class gret))]
         _ (&type/check exo-type (as-otype+ output-type))
         _cursor &/cursor]
-    (return (&/|list (&&/|meta output-type _cursor
-                               (&/V &&/$jvm-invokespecial (&/T class method classes =object =args output-type)))))))
+    (return (&/|list (&&/|meta exo-type _cursor
+                               (&/V &&/$jvm-invokestatic (&/T class method classes =args output-type)))))))
 
 (defn analyse-jvm-null? [analyse exo-type object]
   (|do [=object (&&/analyse-1+ analyse object)
-        _ (ensure-object =object)
+        _ (ensure-object (&&/expr-type* =object))
         :let [output-type &type/Bool]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
@@ -287,35 +350,6 @@
     (return (&/|list (&&/|meta output-type _cursor
                                (&/V &&/$jvm-null nil))))))
 
-(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 0 (&/|list))
-                                 gtype-vars)]
-    (return clean-types)))
-
-(defn ^:private make-gtype [class-name type-args]
-  "(-> Text (List Type) Type)"
-  (&/fold (fn [base-type type-arg]
-            (|case type-arg
-              (&/$BoundT _)
-              (&type/Univ$ &type/empty-env base-type)
-              
-              _
-              base-type))
-          (&type/Data$ class-name type-args)
-          type-args))
-
 (defn ^:private analyse-jvm-new-helper [analyse gtype gtype-env gtype-vars gtype-args args]
   (|case gtype-vars
     (&/$Nil)
@@ -345,7 +379,7 @@
         ;; :let [_ (prn 'analyse-jvm-new/POST class (->> classes &/->seq vec) (&type/show-type output-type))]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
-    (return (&/|list (&&/|meta output-type _cursor
+    (return (&/|list (&&/|meta exo-type _cursor
                                (&/V &&/$jvm-new (&/T class classes =args)))))))
 
 (do-template [<class> <new-name> <new-tag> <load-name> <load-tag> <store-name> <store-tag>]
@@ -353,25 +387,28 @@
         array-type (&type/Data$ &host-type/array-data-tag (&/|list elem-type))
         length-type &type/Int
         idx-type &type/Int]
-    (defn <new-name> [analyse length]
+    (defn <new-name> [analyse exo-type length]
       (|do [=length (&&/analyse-1 analyse length-type length)
+            _ (&type/check exo-type array-type)
             _cursor &/cursor]
-        (return (&/|list (&&/|meta array-type _cursor
+        (return (&/|list (&&/|meta exo-type _cursor
                                    (&/V <new-tag> =length))))))
 
-    (defn <load-name> [analyse array idx]
+    (defn <load-name> [analyse exo-type array idx]
       (|do [=array (&&/analyse-1 analyse array-type array)
             =idx (&&/analyse-1 analyse idx-type idx)
+            _ (&type/check exo-type elem-type)
             _cursor &/cursor]
-        (return (&/|list (&&/|meta elem-type _cursor
+        (return (&/|list (&&/|meta exo-type _cursor
                                    (&/V <load-tag> (&/T =array =idx)))))))
 
-    (defn <store-name> [analyse array idx elem]
+    (defn <store-name> [analyse exo-type array idx elem]
       (|do [=array (&&/analyse-1 analyse array-type array)
             =idx (&&/analyse-1 analyse idx-type idx)
             =elem (&&/analyse-1 analyse elem-type elem)
+            _ (&type/check exo-type array-type)
             _cursor &/cursor]
-        (return (&/|list (&&/|meta array-type _cursor
+        (return (&/|list (&&/|meta exo-type _cursor
                                    (&/V <store-tag> (&/T =array =idx =elem)))))))
     )
 
@@ -387,44 +424,46 @@
 
 (let [length-type &type/Int
       idx-type &type/Int]
-  (defn analyse-jvm-anewarray [analyse class length]
+  (defn analyse-jvm-anewarray [analyse exo-type class length]
     (let [elem-type (&type/Data$ class &/Nil$)
           array-type (&type/Data$ &host-type/array-data-tag (&/|list elem-type))]
       (|do [=length (&&/analyse-1 analyse length-type length)
+            _ (&type/check exo-type array-type)
             _cursor &/cursor]
-        (return (&/|list (&&/|meta array-type _cursor
+        (return (&/|list (&&/|meta exo-type _cursor
                                    (&/V &&/$jvm-anewarray (&/T class =length))))))))
 
-  (defn analyse-jvm-aaload [analyse class array idx]
-    (let [elem-type (&type/Data$ class &/Nil$)
-          array-type (&type/Data$ &host-type/array-data-tag (&/|list elem-type))]
-      (|do [=array (&&/analyse-1 analyse array-type array)
-            =idx (&&/analyse-1 analyse idx-type idx)
-            _cursor &/cursor]
-        (return (&/|list (&&/|meta elem-type _cursor
-                                   (&/V &&/$jvm-aaload (&/T class =array =idx))))))))
+  (defn analyse-jvm-aaload [analyse exo-type class array idx]
+    (|do [=array (&&/analyse-1+ analyse array)
+          [arr-class arr-params] (ensure-object (&&/expr-type* =array))
+          _ (&/assert! (= &host-type/array-data-tag arr-class) (str "[Analyser Error] Expected array. Instead got: " arr-class))
+          :let [(&/$Cons inner-arr-type (&/$Nil)) arr-params]
+          =idx (&&/analyse-1 analyse idx-type idx)
+          _ (&type/check exo-type inner-arr-type)
+          _cursor &/cursor]
+      (return (&/|list (&&/|meta exo-type _cursor
+                                 (&/V &&/$jvm-aaload (&/T class =array =idx)))))))
 
-  (defn analyse-jvm-aastore [analyse class array idx elem]
+  (defn analyse-jvm-aastore [analyse exo-type class array idx elem]
     (let [elem-type (&type/Data$ class &/Nil$)
           array-type (&type/Data$ &host-type/array-data-tag (&/|list elem-type))]
       (|do [=array (&&/analyse-1 analyse array-type array)
             =idx (&&/analyse-1 analyse idx-type idx)
             =elem (&&/analyse-1 analyse elem-type elem)
+            _ (&type/check exo-type array-type)
             _cursor &/cursor]
-        (return (&/|list (&&/|meta array-type _cursor
+        (return (&/|list (&&/|meta exo-type _cursor
                                    (&/V &&/$jvm-aastore (&/T class =array =idx =elem)))))))))
 
-(let [length-type (&type/Data$ "java.lang.Long" &/Nil$)]
-  (defn analyse-jvm-arraylength [analyse array]
-    (&type/with-var
-      (fn [$var]
-        (let [elem-type $var
-              array-type (&type/Data$ &host-type/array-data-tag (&/|list elem-type))]
-          (|do [=array (&&/analyse-1 analyse array-type array)
-                _cursor &/cursor]
-            (return (&/|list (&&/|meta length-type _cursor
-                                       (&/V &&/$jvm-arraylength =array)
-                                       )))))))))
+(defn analyse-jvm-arraylength [analyse exo-type array]
+  (|do [=array (&&/analyse-1+ analyse array)
+        [arr-class arr-params] (ensure-object (&&/expr-type* =array))
+        _ (&/assert! (= &host-type/array-data-tag arr-class) (str "[Analyser Error] Expected array. Instead got: " arr-class))
+        _ (&type/check exo-type &type/Int)
+        _cursor &/cursor]
+    (return (&/|list (&&/|meta exo-type _cursor
+                               (&/V &&/$jvm-arraylength =array)
+                               )))))
 
 (defn ^:private analyse-modifiers [modifiers]
   (&/fold% (fn [so-far modif]
@@ -734,7 +773,7 @@
 (do-template [<name> <tag>]
   (defn <name> [analyse exo-type ?monitor]
     (|do [=monitor (&&/analyse-1+ analyse ?monitor)
-          _ (ensure-object =monitor)
+          _ (ensure-object (&&/expr-type* =monitor))
           :let [output-type &type/Unit]
           _ (&type/check exo-type output-type)
           _cursor &/cursor]
diff --git a/src/lux/host.clj b/src/lux/host.clj
index 74a8af66a..00f1307ad 100644
--- a/src/lux/host.clj
+++ b/src/lux/host.clj
@@ -11,7 +11,7 @@
             (lux [base :as & :refer [|do return* return fail fail* |let |case]]
                  [type :as &type])
             [lux.type.host :as &host-type])
-  (:import (java.lang.reflect Field Method Constructor Modifier)
+  (:import (java.lang.reflect Field Method Constructor Modifier Type)
            java.util.regex.Pattern
            (org.objectweb.asm Opcodes
                               Label
@@ -25,29 +25,6 @@
 (def class-name-separator ".")
 (def class-separator "/")
 
-;; [Utils]
-(def class-name-re #"((\[+)L([\.a-zA-Z0-9]+);|([\.a-zA-Z0-9]+))")
-
-(defn ^:private class->type [^Class class]
-  "(-> Class Type)"
-  (do ;; (prn 'class->type/_0 class (.getSimpleName class) (.getName class))
-      (if-let [[_ _ arr-brackets arr-base simple-base] (re-find class-name-re (.getName class))]
-        (let [base (or arr-base simple-base)]
-          ;; (prn 'class->type/_1 class base arr-brackets)
-          (let [output-type (if (.equals "void" base)
-                              &type/Unit
-                              (reduce (fn [inner _] (&type/Data$ &host-type/array-data-tag (&/|list inner)))
-                                      (&type/Data$ base &/Nil$)
-                                      (range (count (or arr-brackets ""))))
-                              )]
-            ;; (prn 'class->type/_2 class (&type/show-type output-type))
-            output-type)
-          ))))
-
-(defn ^:private method->type [^Method method]
-  "(-> Method Type)"
-  (class->type (.getReturnType method)))
-
 ;; [Resources]
 (do-template [<name> <old-sep> <new-sep>]
   (let [regex (-> <old-sep> Pattern/quote re-pattern)]
@@ -121,12 +98,14 @@
 
 (do-template [<name> <static?>]
   (defn <name> [class-loader target field]
-    (if-let [type* (first (for [^Field =field (.getDeclaredFields (Class/forName (&host-type/as-obj target) true class-loader))
-                                :when (and (.equals ^Object field (.getName =field))
-                                           (.equals ^Object <static?> (Modifier/isStatic (.getModifiers =field))))]
-                            (.getType =field)))]
-      (return (class->type type*))
-      (fail (str "[Host Error] Field does not exist: " target "." field))))
+    (|let [target-class (Class/forName (&host-type/as-obj target) true class-loader)]
+      (if-let [^Type gtype (first (for [^Field =field (.getDeclaredFields target-class)
+                                        :when (and (.equals ^Object field (.getName =field))
+                                                   (.equals ^Object <static?> (Modifier/isStatic (.getModifiers =field))))]
+                                    (.getGenericType =field)))]
+        (|let [gvars (->> target-class .getTypeParameters seq &/->list)]
+          (return (&/T gvars gtype)))
+        (fail (str "[Host Error] Field does not exist: " target "." field)))))
 
   lookup-static-field true
   lookup-field        false
@@ -135,18 +114,26 @@
 (do-template [<name> <static?>]
   (defn <name> [class-loader target method-name args]
     ;; (prn '<name> target method-name)
-    (if-let [method (first (for [^Method =method (.getDeclaredMethods (Class/forName (&host-type/as-obj target) true class-loader))
-                                 :when (and (.equals ^Object method-name (.getName =method))
-                                            (.equals ^Object <static?> (Modifier/isStatic (.getModifiers =method)))
-                                            (let [param-types (&/->list (seq (.getParameterTypes =method)))]
-                                              (and (= (&/|length args) (&/|length param-types))
-                                                   (&/fold2 #(and %1 (.equals ^Object %2 %3))
-                                                            true
-                                                            args
-                                                            (&/|map #(.getName ^Class %) param-types)))))]
-                             =method))]
-      (return (&/T (method->type method) (->> method .getExceptionTypes &/->list (&/|map #(.getName %)))))
-      (fail (str "[Host Error] Method does not exist: " target "." method-name))))
+    (|let [target-class (Class/forName (&host-type/as-obj target) true class-loader)]
+      (if-let [^Method method (first (for [^Method =method (.getDeclaredMethods (Class/forName (&host-type/as-obj target) true class-loader))
+                                           :when (and (.equals ^Object method-name (.getName =method))
+                                                      (.equals ^Object <static?> (Modifier/isStatic (.getModifiers =method)))
+                                                      (let [param-types (&/->list (seq (.getParameterTypes =method)))]
+                                                        (and (= (&/|length args) (&/|length param-types))
+                                                             (&/fold2 #(and %1 (.equals ^Object %2 %3))
+                                                                      true
+                                                                      args
+                                                                      (&/|map #(.getName ^Class %) param-types)))))]
+                                       =method))]
+        (|let [parent-gvars (->> target-class .getTypeParameters seq &/->list)
+               gvars (->> method .getTypeParameters seq &/->list)
+               gargs (->> method .getGenericParameterTypes seq &/->list)]
+          (return (&/T (.getGenericReturnType method)
+                       (->> method .getExceptionTypes &/->list (&/|map #(.getName %)))
+                       parent-gvars
+                       gvars
+                       gargs)))
+        (fail (str "[Host Error] Method does not exist: " target "." method-name)))))
 
   lookup-static-method  true
   lookup-virtual-method false
@@ -255,7 +242,7 @@
                               (.visitEnd))))
                         methods)
               bytecode (.toByteArray (doto =class .visitEnd))]
-        loader &/loader
+        ^ClassLoader loader &/loader
         !classes &/classes
         :let [real-name (str (->class-name module) "." name)
               _ (swap! !classes assoc real-name bytecode)
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 723e169c4..7eae7e181 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -649,31 +649,40 @@
           (|do [actual* (apply-type actual $arg)]
             (check* class-loader fixpoints invariant?? expected actual*))))
 
-      [(&/$DataT e!name e!params) (&/$DataT a!name a!params)]
-      (cond (= "#Null" a!name)
-            (if (not (&&host/primitive-type? e!name))
-              (return (&/T fixpoints nil))
-              (fail (check-error expected actual)))
-
-            (= "#Null" e!name)
-            (if (= "#Null" a!name)
-              (return (&/T fixpoints nil))
-              (fail (check-error expected actual)))
-
-            :else
-            (let [e!name (&&host/as-obj e!name)
-                  a!name (&&host/as-obj a!name)]
-              (cond (and (.equals ^Object e!name a!name)
-                         (= (&/|length e!params) (&/|length a!params)))
-                    (|do [_ (&/map2% (partial check* class-loader fixpoints true) e!params a!params)]
-                      (return (&/T fixpoints nil)))
-
-                    (not invariant??)
-                    (|do [actual& (&&host/->super-type existential class-loader e!name a!name a!params)]
-                      (check* class-loader fixpoints invariant?? expected actual&))
-
-                    :else
-                    (fail (str "[Type Error] Names don't match: " e!name " =/= " a!name)))))
+      [(&/$DataT e!data) (&/$DataT a!data)]
+      (&&host/check-host-types (partial check* class-loader fixpoints true)
+                               check-error
+                               fixpoints
+                               existential
+                               class-loader
+                               invariant??
+                               e!data
+                               a!data)
+      ;; [(&/$DataT e!name e!params) (&/$DataT a!name a!params)]
+      ;; (cond (= "#Null" a!name)
+      ;;       (if (not (&&host/primitive-type? e!name))
+      ;;         (return (&/T fixpoints nil))
+      ;;         (fail (check-error expected actual)))
+
+      ;;       (= "#Null" e!name)
+      ;;       (if (= "#Null" a!name)
+      ;;         (return (&/T fixpoints nil))
+      ;;         (fail (check-error expected actual)))
+
+      ;;       :else
+      ;;       (let [e!name (&&host/as-obj e!name)
+      ;;             a!name (&&host/as-obj a!name)]
+      ;;         (cond (and (.equals ^Object e!name a!name)
+      ;;                    (= (&/|length e!params) (&/|length a!params)))
+      ;;               (|do [_ (&/map2% (partial check* class-loader fixpoints true) e!params a!params)]
+      ;;                 (return (&/T fixpoints nil)))
+
+      ;;               (not invariant??)
+      ;;               (|do [actual* (&&host/->super-type existential class-loader e!name a!name a!params)]
+      ;;                 (check* class-loader fixpoints invariant?? expected actual*))
+
+      ;;               :else
+      ;;               (fail (str "[Type Error] Names don't match: " e!name " =/= " a!name)))))
 
       [(&/$LambdaT eI eO) (&/$LambdaT aI aO)]
       (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)]
diff --git a/src/lux/type/host.clj b/src/lux/type/host.clj
index 486205494..3121a2213 100644
--- a/src/lux/type/host.clj
+++ b/src/lux/type/host.clj
@@ -17,9 +17,6 @@
 (def null-data-tag "#Null")
 
 ;; [Utils]
-(defn ^:private Data$ [name params]
-  (&/V &/$DataT (&/T name params)))
-
 (defn ^:private trace-lineage* [^Class super-class ^Class sub-class]
   "(-> Class Class (List Class))"
   ;; Either they're both interfaces, of they're both classes
@@ -56,7 +53,9 @@
 
 (defn ^:private trace-lineage [^Class sub-class ^Class super-class]
   "(-> Class Class (List Class))"
-  (&/|reverse (trace-lineage* super-class sub-class)))
+  (if (= sub-class super-class)
+    (&/|list)
+    (&/|reverse (trace-lineage* super-class sub-class))))
 
 (let [matcher (fn [m ^TypeVariable jt lt] (&/Cons$ (&/T (.getName jt) lt) m))]
   (defn ^:private match-params [sub-type-params params]
@@ -65,15 +64,30 @@
     (&/fold2 matcher (&/|table) sub-type-params params)))
 
 ;; [Exports]
+(let [class-name-re #"((\[+)L([\.a-zA-Z0-9]+);|([\.a-zA-Z0-9]+))"
+      Unit (&/V &/$TupleT (&/|list))]
+  (defn class->type [^Class class]
+    "(-> Class Type)"
+    (do ;; (prn 'class->type/_0 class (.getSimpleName class) (.getName class))
+        (if-let [[_ _ arr-brackets arr-base simple-base] (re-find class-name-re (.getName class))]
+          (let [base (or arr-base simple-base)]
+            ;; (prn 'class->type/_1 class base arr-brackets)
+            (if (.equals "void" base)
+              Unit
+              (reduce (fn [inner _] (&/V &/$DataT (&/T array-data-tag (&/|list inner))))
+                      (&/V &/$DataT (&/T base &/Nil$))
+                      (range (count (or arr-brackets "")))))
+            )))))
+
 (defn instance-param [existential matchings refl-type]
   "(-> (List (, Text Type)) (^ java.lang.reflect.Type) (Lux Type))"
   ;; (prn 'instance-param refl-type (class refl-type))
   (cond (instance? Class refl-type)
-        (return (Data$ (.getName ^Class refl-type) (&/|list)))
+        (return (class->type refl-type))
 
         (instance? GenericArrayType refl-type)
         (let [inner-type (instance-param existential matchings (.getGenericComponentType ^GenericArrayType refl-type))]
-          (return (Data$ array-data-tag (&/|list inner-type))))
+          (return (&/V &/$DataT (&/T array-data-tag (&/|list inner-type)))))
         
         (instance? ParameterizedType refl-type)
         (|do [:let [refl-type* ^ParameterizedType refl-type]
@@ -81,8 +95,8 @@
                            .getActualTypeArguments
                            seq &/->list
                            (&/map% (partial instance-param existential matchings)))]
-          (return (Data$ (->> refl-type* ^Class (.getRawType) .getName)
-                         params*)))
+          (return (&/V &/$DataT (&/T (->> refl-type* ^Class (.getRawType) .getName)
+                                     params*))))
         
         (instance? TypeVariable refl-type)
         (let [gvar (.getName ^TypeVariable refl-type)]
@@ -140,8 +154,8 @@
         sub-class+ (Class/forName sub-class true class-loader)]
     (if (.isAssignableFrom super-class+ sub-class+)
       (let [lineage (trace-lineage sub-class+ super-class+)]
-        (|do [[sub-class* sub-params*] (raise existential lineage sub-class+ sub-params)]
-          (return (Data$ (.getName sub-class*) sub-params*))))
+        (|do [[^Class sub-class* sub-params*] (raise existential lineage sub-class+ sub-params)]
+          (return (&/V &/$DataT (&/T (.getName sub-class*) sub-params*)))))
       (fail (str "[Type Error] Classes don't have a subtyping relationship: " sub-class " </=" super-class)))))
 
 (defn as-obj [class]
@@ -160,3 +174,38 @@
 (let [primitive-types #{"boolean" "byte" "short" "int" "long" "float" "double" "char"}]
   (defn primitive-type? [type-name]
     (contains? primitive-types type-name)))
+
+(defn check-host-types [check check-error fixpoints existential class-loader invariant?? expected actual]
+  (|let [[e!name e!params] expected
+         [a!name a!params] actual]
+    (cond (= "java.lang.Object" e!name)
+          (return (&/T fixpoints nil))
+
+          (= null-data-tag a!name)
+          (if (not (primitive-type? e!name))
+            (return (&/T fixpoints nil))
+            (fail (check-error (&/V &/$DataT expected) (&/V &/$DataT actual))))
+
+          (= null-data-tag e!name)
+          (if (= null-data-tag a!name)
+            (return (&/T fixpoints nil))
+            (fail (check-error (&/V &/$DataT expected) (&/V &/$DataT actual))))
+
+          (and (= array-data-tag e!name)
+               (not= array-data-tag a!name))
+          (fail (check-error (&/V &/$DataT expected) (&/V &/$DataT actual)))
+          
+          :else
+          (let [e!name (as-obj e!name)
+                a!name (as-obj a!name)]
+            (cond (and (.equals ^Object e!name a!name)
+                       (= (&/|length e!params) (&/|length a!params)))
+                  (|do [_ (&/map2% check e!params a!params)]
+                    (return (&/T fixpoints nil)))
+
+                  (not invariant??)
+                  (|do [actual* (->super-type existential class-loader e!name a!name a!params)]
+                    (check (&/V &/$DataT expected) actual*))
+
+                  :else
+                  (fail (str "[Type Error] Names don't match: " e!name " =/= " a!name)))))))