- Primitive data-types can now be parameterized by other types.

10 files changed, 190 insertions, 195 deletions

diff --git a/source/lux.lux b/source/lux.lux
index f5cc8d3d1..39cbb7765 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -9,23 +9,23 @@
 
 ## Basic types
 (_lux_def Bool (10 ["lux" "Bool"]
-                   (0 "java.lang.Boolean")))
+                   (0 "java.lang.Boolean" (0))))
 (_lux_export Bool)
 
 (_lux_def Int (10 ["lux" "Int"]
-                  (0 "java.lang.Long")))
+                  (0 "java.lang.Long" (0))))
 (_lux_export Int)
 
 (_lux_def Real (10 ["lux" "Real"]
-                   (0 "java.lang.Double")))
+                   (0 "java.lang.Double" (0))))
 (_lux_export Real)
 
 (_lux_def Char (10 ["lux" "Char"]
-                   (0 "java.lang.Character")))
+                   (0 "java.lang.Character" (0))))
 (_lux_export Char)
 
 (_lux_def Text (10 ["lux" "Text"]
-                   (0 "java.lang.String")))
+                   (0 "java.lang.String" (0))))
 (_lux_export Text)
 
 (_lux_def Unit (10 ["lux" "Unit"]
@@ -71,7 +71,7 @@
 (_lux_declare-tags [#None #Some] Maybe)
 
 ## (deftype #rec Type
-##   (| (#DataT Text)
+##   (| (#DataT (, Text (List Type)))
 ##      (#VariantT (List Type))
 ##      (#TupleT (List Type))
 ##      (#LambdaT Type Type)
@@ -90,7 +90,7 @@
           TypeList
           (9 (7 (0)
                 (1 (1 ## "lux;DataT"
-                    Text
+                    (2 (1 Text (1 TypeList (0))))
                     (1 ## "lux;VariantT"
                      TypeList
                      (1 ## "lux;TupleT"
@@ -279,11 +279,11 @@
 (_lux_def Host
   (#NamedT ["lux" "Host"]
            (#TupleT (#Cons [## "lux;writer"
-                            (#DataT "org.objectweb.asm.ClassWriter")
+                            (#DataT "org.objectweb.asm.ClassWriter" #Nil)
                             (#Cons [## "lux;loader"
-                                    (#DataT "java.lang.ClassLoader")
+                                    (#DataT "java.lang.ClassLoader" #Nil)
                                     (#Cons [## "lux;classes"
-                                            (#DataT "clojure.lang.Atom")
+                                            (#DataT "clojure.lang.Atom" #Nil)
                                             #Nil])])]))))
 (_lux_declare-tags [#writer #loader #classes] Host)
 
@@ -912,14 +912,6 @@
     _
     (fail "Wrong syntax for @list&")))
 
-(defmacro' #export (^ tokens)
-  (_lux_case tokens
-    (#Cons [_ (#SymbolS "" class-name)] #Nil)
-    (return (@list (form$ (@list (tag$ ["lux" "DataT"]) (text$ class-name)))))
-
-    _
-    (fail "Wrong syntax for ^")))
-
 (defmacro' #export (, tokens)
   (return (@list (form$ (@list (tag$ ["lux" "TupleT"])
                                (foldL (lambda'' [tail head] (form$ (@list (tag$ ["lux" "Cons"]) head tail)))
@@ -1352,6 +1344,17 @@
       (wrap (wrap-meta (form$ (@list (tag$ ["lux" "RecordS"]) (untemplate-list =fields))))))
     ))
 
+(defmacro' #export (^ tokens)
+  (_lux_case tokens
+    (#Cons [_ (#SymbolS "" class-name)] #Nil)
+    (return (@list (form$ (@list (tag$ ["lux" "DataT"]) (text$ class-name) (tag$ ["lux" "Nil"])))))
+
+    (#Cons [_ (#SymbolS "" class-name)] params)
+    (return (@list (form$ (@list (tag$ ["lux" "DataT"]) (text$ class-name) (untemplate-list params)))))
+
+    _
+    (fail "Wrong syntax for ^")))
+
 (def'' (get-module-name state)
   ($' Lux Text)
   (_lux_case state
@@ -3192,8 +3195,8 @@
 (def (type->ast type)
   (-> Type AST)
   (case type
-    (#DataT name)
-    (` (#DataT (~ (text$ name))))
+    (#DataT name params)
+    (` (#DataT (~ (text$ name)) (~ (untemplate-list (map type->ast params)))))
     
     (#;VariantT cases)
     (` (#VariantT (~ (untemplate-list (map type->ast cases)))))
diff --git a/source/lux/data/list.lux b/source/lux/data/list.lux
index 54f8fed4c..e538007bf 100644
--- a/source/lux/data/list.lux
+++ b/source/lux/data/list.lux
@@ -333,3 +333,6 @@
 
     _
     (#;Left "Wrong syntax for zip")))
+
+(def #export zip2 (zip 2))
+(def #export zip3 (zip 3))
diff --git a/source/lux/meta/ast.lux b/source/lux/meta/ast.lux
index 398acf6cc..6d9271847 100644
--- a/source/lux/meta/ast.lux
+++ b/source/lux/meta/ast.lux
@@ -99,7 +99,7 @@
              (foldL (lambda [old [x' y']]
                       (and old (= x' y')))
                     true
-                    ((zip 2) xs' ys')))])
+                    (zip2 xs' ys')))])
       [[#;FormS] [#;TupleS]]
 
       [[_ (#;RecordS xs')] [_ (#;RecordS ys')]]
@@ -107,7 +107,7 @@
            (foldL (lambda [old [[xl' xr'] [yl' yr']]]
                     (and old (= xl' yl') (= xr' yr')))
                   true
-                  ((zip 2) xs' ys')))
+                  (zip2 xs' ys')))
       
       _
       false)))
diff --git a/source/lux/meta/type.lux b/source/lux/meta/type.lux
index 4147e37d4..a1c34b1ac 100644
--- a/source/lux/meta/type.lux
+++ b/source/lux/meta/type.lux
@@ -10,7 +10,7 @@
               (data (text #open ("text:" Text/Monoid Text/Eq))
                     (number/int #open ("int:" Int/Eq Int/Show))
                     maybe
-                    (list #refer #all #open ("list:" List/Monad)))
+                    (list #refer #all #open ("list:" List/Monad List/Fold)))
               ))
 
 (open List/Fold)
@@ -19,8 +19,13 @@
 (defstruct #export Type/Show (Show Type)
   (def (show type)
     (case type
-      (#;DataT name)
-      ($ text:++ "(^ " name ")")
+      (#;DataT name params)
+      (case params
+        #;Nil
+        ($ text:++ "(^ " name ")")
+
+        _
+        ($ text:++ "(^ " name " " (|> params (list:map show) (interpose " ") (list:foldL text:++ "")) ")"))
 
       (#;TupleT members)
       (case members
@@ -66,8 +71,13 @@
 (defstruct #export Type/Eq (Eq Type)
   (def (= x y)
     (case [x y]
-      [(#;DataT xname) (#;DataT yname)]
-      (text:= xname yname)
+      [(#;DataT xname xparams) (#;DataT yname yparams)]
+      (and (text:= xname yname)
+           (int:= (size xparams) (size yparams))
+           (foldL (lambda [prev [x y]]
+                    (and prev (= x y)))
+                  true
+                  (zip2 xparams yparams)))
 
       (\or [(#;VarT xid) (#;VarT yid)]
        [(#;ExT xid) (#;ExT yid)]
@@ -90,7 +100,7 @@
            (foldL (lambda [prev [x y]]
                     (and prev (= x y)))
                   true
-                  ((zip 2) xmembers ymembers)))
+                  (zip2 xmembers ymembers)))
 
       (\or [(#;UnivQ xenv xbody) (#;UnivQ yenv ybody)]
        [(#;ExQ xenv xbody) (#;ExQ yenv ybody)])
@@ -98,7 +108,7 @@
            (foldL (lambda [prev [x y]]
                     (and prev (= x y)))
                   (= xbody ybody)
-                  ((zip 2) xenv yenv)))
+                  (zip2 xenv yenv)))
 
       _
       false
diff --git a/src/lux/analyser/host.clj b/src/lux/analyser/host.clj
index 9a05a6695..610f3c660 100644
--- a/src/lux/analyser/host.clj
+++ b/src/lux/analyser/host.clj
@@ -34,7 +34,7 @@
 (defn ^:private ensure-object [token]
   "(-> Analysis (Lux (,)))"
   (|case token
-    [_ (&/$DataT _)]
+    [_ (&/$DataT _ _)]
     (return nil)
 
     _
@@ -43,8 +43,8 @@
 (defn ^:private as-object [type]
   "(-> Type Type)"
   (|case type
-    (&/$DataT class)
-    (&/V &/$DataT (&type/as-obj class))
+    (&/$DataT class params)
+    (&type/Data$ (&type/as-obj class) params)
 
     _
     type))
@@ -66,16 +66,16 @@
 (defn ^:private as-otype+ [type]
   "(-> Type Type)"
   (|case type
-    (&/$DataT tname)
-    (&/V &/$DataT (as-otype tname))
+    (&/$DataT name params)
+    (&type/Data$ (as-otype name) params)
 
     _
     type))
 
 ;; [Resources]
 (do-template [<name> <output-tag> <input-class> <output-class>]
-  (let [input-type (&/V &/$DataT <input-class>)
-        output-type (&/V &/$DataT <output-class>)]
+  (let [input-type (&type/Data$ <input-class> (&/|list))
+        output-type (&type/Data$ <output-class> (&/|list))]
     (defn <name> [analyse exo-type ?x ?y]
       (|do [=x (&&/analyse-1 analyse input-type ?x)
             =y (&&/analyse-1 analyse input-type ?y)
@@ -160,10 +160,10 @@
         =classes (&/map% extract-text ?classes)
         =return (&host/lookup-static-method class-loader ?class ?method =classes)
         ;; :let [_ (matchv ::M/objects [=return]
-        ;;           [[&/$DataT _return-class]]
+        ;;           [[&/$DataT _return-class (&/|list)]]
         ;;           (prn 'analyse-jvm-invokestatic ?class ?method _return-class))]
         =args (&/map2% (fn [_class _arg]
-                         (&&/analyse-1 analyse (&/V &/$DataT _class) _arg))
+                         (&&/analyse-1 analyse (&type/Data$ _class (&/|list)) _arg))
                        =classes
                        ?args)
         :let [output-type =return]
@@ -182,8 +182,8 @@
     (|do [class-loader &/loader
           =classes (&/map% extract-text ?classes)
           =return (&host/lookup-virtual-method class-loader ?class ?method =classes)
-          =object (&&/analyse-1 analyse (&/V &/$DataT ?class) ?object)
-          =args (&/map2% (fn [?c ?o] (&&/analyse-1 analyse (&/V &/$DataT ?c) ?o))
+          =object (&&/analyse-1 analyse (&type/Data$ ?class (&/|list)) ?object)
+          =args (&/map2% (fn [?c ?o] (&&/analyse-1 analyse (&type/Data$ ?c (&/|list)) ?o))
                          =classes ?args)
           :let [output-type =return]
           _ (&type/check exo-type (as-otype+ output-type))]
@@ -199,9 +199,9 @@
         =return (if (= "<init>" ?method)
                   (return &type/Unit)
                   (&host/lookup-virtual-method class-loader ?class ?method =classes))
-        =object (&&/analyse-1 analyse (&/V &/$DataT ?class) ?object)
+        =object (&&/analyse-1 analyse (&type/Data$ ?class (&/|list)) ?object)
         =args (&/map2% (fn [?c ?o]
-                         (&&/analyse-1 analyse (&/V &/$DataT ?c) ?o))
+                         (&&/analyse-1 analyse (&type/Data$ ?c (&/|list)) ?o))
                        =classes ?args)
         :let [output-type =return]
         _ (&type/check exo-type (as-otype+ output-type))]
@@ -215,19 +215,19 @@
     (return (&/|list (&/T (&/V &&/$jvm-null? =object) output-type)))))
 
 (defn analyse-jvm-null [analyse exo-type]
-  (|do [:let [output-type (&/V &/$DataT "null")]
+  (|do [:let [output-type (&type/Data$ "null" (&/|list))]
         _ (&type/check exo-type output-type)]
     (return (&/|list (&/T (&/V &&/$jvm-null nil) output-type)))))
 
 (defn analyse-jvm-new [analyse exo-type ?class ?classes ?args]
   (|do [=classes (&/map% extract-text ?classes)
         =args (&/map% (partial analyse-1+ analyse) ?args)
-        :let [output-type (&/V &/$DataT ?class)]
+        :let [output-type (&type/Data$ ?class (&/|list))]
         _ (&type/check exo-type output-type)]
     (return (&/|list (&/T (&/V &&/$jvm-new (&/T ?class =classes =args)) output-type)))))
 
 (defn analyse-jvm-new-array [analyse ?class ?length]
-  (return (&/|list (&/T (&/V &&/$jvm-new-array (&/T ?class ?length)) (&/V "array" (&/T (&/V &/$DataT ?class)
+  (return (&/|list (&/T (&/V &&/$jvm-new-array (&/T ?class ?length)) (&/V "array" (&/T (&type/Data$ ?class (&/|list))
                                                                                        (&/V &/$Nil nil)))))))
 
 (defn analyse-jvm-aastore [analyse ?array ?idx ?elem]
@@ -313,11 +313,11 @@
                                    =method-body (&/with-scope (str ?name "_" ?idx)
                                                   (&/fold (fn [body* input*]
                                                             (|let [[iname itype] input*]
-                                                              (&&env/with-local iname (&/V &/$DataT (as-otype itype))
+                                                              (&&env/with-local iname (&type/Data$ (as-otype itype) (&/|list))
                                                                 body*)))
                                                           (if (= "void" ?method-output)
                                                             (analyse-1+ analyse ?method-body)
-                                                            (&&/analyse-1 analyse (&/V &/$DataT (as-otype ?method-output)) ?method-body))
+                                                            (&&/analyse-1 analyse (&type/Data$ (as-otype ?method-output) (&/|list)) ?method-body))
                                                           (&/|reverse (if (:static? =method-modifiers)
                                                                         =method-inputs
                                                                         (&/Cons$ (&/T ";this" ?super-class)
@@ -360,7 +360,7 @@
   (|do [:let [[?catches ?finally] ?catches+?finally]
         =body (&&/analyse-1 analyse exo-type ?body)
         =catches (&/map% (fn [[?ex-class ?ex-arg ?catch-body]]
-                           (|do [=catch-body (&&env/with-local ?ex-arg (&/V &/$DataT ?ex-class)
+                           (|do [=catch-body (&&env/with-local ?ex-arg (&type/Data$ ?ex-class (&/|list))
                                                (&&/analyse-1 analyse exo-type ?catch-body))
                                  idx &&env/next-local-idx]
                              (return (&/T ?ex-class idx =catch-body))))
@@ -374,7 +374,7 @@
 (defn analyse-jvm-throw [analyse exo-type ?ex]
   (|do [=ex (analyse-1+ analyse ?ex)
         :let [[_obj _type] =ex]
-        _ (&type/check (&/V &/$DataT "java.lang.Throwable") _type)]
+        _ (&type/check (&type/Data$ "java.lang.Throwable" (&/|list)) _type)]
     (return (&/|list (&/T (&/V &&/$jvm-throw =ex) &type/$Void)))))
 
 (do-template [<name> <tag>]
@@ -390,9 +390,9 @@
   )
 
 (do-template [<name> <tag> <from-class> <to-class>]
-  (let [output-type (&/V &/$DataT <to-class>)]
+  (let [output-type (&type/Data$ <to-class> (&/|list))]
     (defn <name> [analyse exo-type ?value]
-      (|do [=value (&&/analyse-1 analyse (&/V &/$DataT <from-class>) ?value)
+      (|do [=value (&&/analyse-1 analyse (&type/Data$ <from-class> (&/|list)) ?value)
             _ (&type/check exo-type output-type)]
         (return (&/|list (&/T (&/V <tag> =value) output-type))))))
 
@@ -417,9 +417,9 @@
   )
 
 (do-template [<name> <tag> <from-class> <to-class>]
-  (let [output-type (&/V &/$DataT <to-class>)]
+  (let [output-type (&type/Data$ <to-class> (&/|list))]
     (defn <name> [analyse exo-type ?value]
-      (|do [=value (&&/analyse-1 analyse (&/V &/$DataT <from-class>) ?value)
+      (|do [=value (&&/analyse-1 analyse (&type/Data$ <from-class> (&/|list)) ?value)
             _ (&type/check exo-type output-type)]
         (return (&/|list (&/T (&/V <tag> =value) output-type))))))
 
diff --git a/src/lux/analyser/lux.clj b/src/lux/analyser/lux.clj
index b8239d1a9..6205adccb 100644
--- a/src/lux/analyser/lux.clj
+++ b/src/lux/analyser/lux.clj
@@ -364,7 +364,7 @@
             (|do [;; :let [_ (prn 'MACRO-EXPAND|PRE (&/ident->text real-name))]
                   macro-expansion #(-> macro (.apply ?args) (.apply %))
                   ;; :let [_ (prn 'MACRO-EXPAND|POST (&/ident->text real-name))]
-                  ;; :let [_ (when (or (= "defsig" (aget real-name 1))
+                  ;; :let [_ (when (or (= "zip" (aget real-name 1))
                   ;;                   ;; (= "..?" (aget real-name 1))
                   ;;                   ;; (= "try$" (aget real-name 1))
                   ;;                   )
@@ -431,13 +431,9 @@
     (|do [exo-type* (&type/actual-type exo-type)]
       (|case exo-type
         (&/$UnivQ _)
-        (&type/with-var
-          (fn [$var]
-            (|do [exo-type** (&type/apply-type exo-type* $var)]
-              (analyse-lambda* analyse exo-type** ?self ?arg ?body))))
-        ;; (|do [$var &type/existential
-        ;;       exo-type** (&type/apply-type exo-type* $var)]
-        ;;   (analyse-lambda* analyse exo-type** ?self ?arg ?body))
+        (|do [$var &type/existential
+              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/compiler/host.clj b/src/lux/compiler/host.clj
index 0529ac900..db54af8ac 100644
--- a/src/lux/compiler/host.clj
+++ b/src/lux/compiler/host.clj
@@ -52,31 +52,31 @@
       (&/$TupleT (&/$Nil))
       (.visitInsn *writer* Opcodes/ACONST_NULL)
 
-      (&/$DataT "boolean")
+      (&/$DataT "boolean" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class boolean-class) "valueOf" (str "(Z)" (&host/->type-signature boolean-class)))
       
-      (&/$DataT "byte")
+      (&/$DataT "byte" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class byte-class) "valueOf" (str "(B)" (&host/->type-signature byte-class)))
 
-      (&/$DataT "short")
+      (&/$DataT "short" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class short-class) "valueOf" (str "(S)" (&host/->type-signature short-class)))
 
-      (&/$DataT "int")
+      (&/$DataT "int" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class int-class) "valueOf" (str "(I)" (&host/->type-signature int-class)))
 
-      (&/$DataT "long")
+      (&/$DataT "long" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class long-class) "valueOf" (str "(J)" (&host/->type-signature long-class)))
 
-      (&/$DataT "float")
+      (&/$DataT "float" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class float-class) "valueOf" (str "(F)" (&host/->type-signature float-class)))
 
-      (&/$DataT "double")
+      (&/$DataT "double" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class double-class) "valueOf" (str "(D)" (&host/->type-signature double-class)))
 
-      (&/$DataT "char")
+      (&/$DataT "char" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host/->class char-class) "valueOf" (str "(C)" (&host/->type-signature char-class)))
       
-      (&/$DataT _)
+      (&/$DataT _ (&/$Nil))
       nil
 
       (&/$NamedT ?name ?type)
diff --git a/src/lux/compiler/type.clj b/src/lux/compiler/type.clj
index d75f6afef..6c128df80 100644
--- a/src/lux/compiler/type.clj
+++ b/src/lux/compiler/type.clj
@@ -39,48 +39,44 @@
   "(-> Analysis Analysis Analysis)"
   (variant$ &/$Cons (tuple$ (&/|list head tail))))
 
+(defn ^:private List$ [elems]
+  (&/fold (fn [tail head]
+            (Cons$ head tail))
+          $Nil
+          (&/|reverse elems)))
+
 ;; [Exports]
 (defn ->analysis [type]
   "(-> Type Analysis)"
   (|case type
-    (&/$DataT ?class)
-    (variant$ &/$DataT (text$ ?class))
+    (&/$DataT class params)
+    (variant$ &/$DataT (tuple$ (&/|list (text$ class)
+                                        (List$ (&/|map ->analysis params)))))
     
-    (&/$TupleT ?members)
-    (variant$ &/$TupleT
-              (&/fold (fn [tail head]
-                        (Cons$ (->analysis head) tail))
-                      $Nil
-                      (&/|reverse ?members)))
-
-    (&/$VariantT ?members)
-    (variant$ &/$VariantT
-              (&/fold (fn [tail head]
-                        (Cons$ (->analysis head) tail))
-                      $Nil
-                      (&/|reverse ?members)))
-
-    (&/$LambdaT ?input ?output)
-    (variant$ &/$LambdaT (tuple$ (&/|list (->analysis ?input) (->analysis ?output))))
-
-    (&/$UnivQ ?env ?body)
+    (&/$TupleT members)
+    (variant$ &/$TupleT (List$ (&/|map ->analysis members)))
+
+    (&/$VariantT members)
+    (variant$ &/$VariantT (List$ (&/|map ->analysis members)))
+
+    (&/$LambdaT input output)
+    (variant$ &/$LambdaT (tuple$ (&/|list (->analysis input) (->analysis output))))
+
+    (&/$UnivQ env body)
     (variant$ &/$UnivQ
-              (tuple$ (&/|list (&/fold (fn [tail head]
-                                         (Cons$ (->analysis head) tail))
-                                       $Nil
-                                       (&/|reverse ?env))
-                               (->analysis ?body))))
+              (tuple$ (&/|list (List$ (&/|map ->analysis env))
+                               (->analysis body))))
 
-    (&/$BoundT ?idx)
-    (variant$ &/$BoundT (int$ ?idx))
+    (&/$BoundT idx)
+    (variant$ &/$BoundT (int$ idx))
 
-    (&/$AppT ?fun ?arg)
-    (variant$ &/$AppT (tuple$ (&/|list (->analysis ?fun) (->analysis ?arg))))
+    (&/$AppT fun arg)
+    (variant$ &/$AppT (tuple$ (&/|list (->analysis fun) (->analysis arg))))
 
-    (&/$NamedT [?module ?name] ?type)
-    (variant$ &/$NamedT (tuple$ (&/|list (tuple$ (&/|list (text$ ?module) (text$ ?name)))
-                                         (->analysis ?type))))
+    (&/$NamedT [module name] type*)
+    (variant$ &/$NamedT (tuple$ (&/|list (tuple$ (&/|list (text$ module) (text$ name)))
+                                         (->analysis type*))))
 
     _
-    (assert false (&type/show-type type))
+    (assert false (prn '->analysis (&type/show-type type) (&/adt->text type)))
     ))
diff --git a/src/lux/host.clj b/src/lux/host.clj
index 2290f2f0a..0936d90eb 100644
--- a/src/lux/host.clj
+++ b/src/lux/host.clj
@@ -29,8 +29,9 @@
                                             (.getSimpleName class)))]
     (if (.equals "void" base)
       (return &type/Unit)
-      (return (&/V &/$DataT (str (reduce str "" (repeat (int (/ (count arr-level) 2)) "["))
-                                    base)))
+      (return (&type/Data$ (str (reduce str "" (repeat (int (/ (count arr-level) 2)) "["))
+                                base)
+                           (&/|list)))
       )))
 
 (defn ^:private method->type [^Method method]
@@ -70,7 +71,7 @@
 (defn ->java-sig [^objects type]
   "(-> Type Text)"
   (|case type
-    (&/$DataT ?name)
+    (&/$DataT ?name params)
     (->type-signature ?name)
 
     (&/$LambdaT _ _)
diff --git a/src/lux/type.clj b/src/lux/type.clj
index 3b7349fca..0da579cf4 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -24,8 +24,8 @@
     false))
 
 (def ^:private empty-env (&/V &/$Nil nil))
-(defn Data$ [name]
-  (&/V &/$DataT name))
+(defn Data$ [name params]
+  (&/V &/$DataT (&/T name params)))
 (defn Bound$ [idx]
   (&/V &/$BoundT idx))
 (defn Var$ [id]
@@ -46,13 +46,13 @@
   (&/V &/$NamedT (&/T name type)))
 
 
-(def Bool (Named$ (&/T "lux" "Bool") (&/V &/$DataT "java.lang.Boolean")))
-(def Int (Named$ (&/T "lux" "Int") (&/V &/$DataT "java.lang.Long")))
-(def Real (Named$ (&/T "lux" "Real") (&/V &/$DataT "java.lang.Double")))
-(def Char (Named$ (&/T "lux" "Char") (&/V &/$DataT "java.lang.Character")))
-(def Text (Named$ (&/T "lux" "Text") (&/V &/$DataT "java.lang.String")))
-(def Unit (Named$ (&/T "lux" "Unit") (&/V &/$TupleT (&/|list))))
-(def $Void (Named$ (&/T "lux" "Void") (&/V &/$VariantT (&/|list))))
+(def Bool (Named$ (&/T "lux" "Bool") (Data$ "java.lang.Boolean" (&/|list))))
+(def Int (Named$ (&/T "lux" "Int") (Data$ "java.lang.Long" (&/|list))))
+(def Real (Named$ (&/T "lux" "Real") (Data$ "java.lang.Double" (&/|list))))
+(def Char (Named$ (&/T "lux" "Char") (Data$ "java.lang.Character" (&/|list))))
+(def Text (Named$ (&/T "lux" "Text") (Data$ "java.lang.String" (&/|list))))
+(def Unit (Named$ (&/T "lux" "Unit") (Tuple$ (&/|list))))
+(def $Void (Named$ (&/T "lux" "Void") (Variant$ (&/|list))))
 (def Ident (Named$ (&/T "lux" "Ident") (Tuple$ (&/|list Text Text))))
 
 (def IO
@@ -90,7 +90,7 @@
             (App$ (Univ$ empty-env
                          (Variant$ (&/|list
                                     ;; DataT
-                                    Text
+                                    (Tuple$ (&/|list Text TypeList))
                                     ;; VariantT
                                     TypeList
                                     ;; TupleT
@@ -221,11 +221,11 @@
           (Tuple$
            (&/|list
             ;; "lux;writer"
-            (Data$ "org.objectweb.asm.ClassWriter")
+            (Data$ "org.objectweb.asm.ClassWriter" (&/|list))
             ;; "lux;loader"
-            (Data$ "java.lang.ClassLoader")
+            (Data$ "java.lang.ClassLoader" (&/|list))
             ;; "lux;classes"
-            (Data$ "clojure.lang.Atom")))))
+            (Data$ "clojure.lang.Atom" (&/|list))))))
 
 (def DefData*
   (Univ$ empty-env
@@ -405,9 +405,7 @@
                                        ))))
                                (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings)))]
          (fn [state]
-           (return* (&/update$ &/$type-vars #(->> %
-                                                  ;; (&/update$ &/$counter dec)
-                                                  (&/set$ &/$mappings (&/|remove id mappings*)))
+           (return* (&/update$ &/$type-vars #(&/set$ &/$mappings (&/|remove id mappings*) %)
                                state)
                     nil)))
        state))))
@@ -418,12 +416,6 @@
         _ (delete-var id)]
     (return output)))
 
-(defn with-vars [amount k]
-  (|do [=vars (&/map% (constantly create-var) (&/|range amount))
-        output (k (&/|map #(Var$ %) =vars))
-        _ (&/map% delete-var (&/|reverse =vars))]
-    (return output)))
-
 (defn clean* [?tid type]
   (|case type
     (&/$VarT ?id)
@@ -486,8 +478,13 @@
 
 (defn show-type [^objects type]
   (|case type
-    (&/$DataT name)
-    (str "(^ " name ")")
+    (&/$DataT name params)
+    (|case params
+      (&/$Nil)
+      (str "(^ " name ")")
+
+      _
+      (str "(^ " name " " (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
     
     (&/$TupleT elems)
     (if (&/|empty? elems)
@@ -535,8 +532,10 @@
                      (and (= ?xmodule ?ymodule)
                           (= ?xname ?yname))
 
-                     [(&/$DataT xname) (&/$DataT yname)]
-                     (.equals ^Object xname yname)
+                     [(&/$DataT xname xparams) (&/$DataT yname yparams)]
+                     (and (.equals ^Object xname yname)
+                          (= (&/|length xparams) (&/|length yparams))
+                          (&/fold2 #(and %1 (type= %2 %3)) true xparams yparams))
 
                      [(&/$TupleT xelems) (&/$TupleT yelems)]
                      (&/fold2 (fn [old x y] (and old (type= x y)))
@@ -677,7 +676,7 @@
 
 (def ^:private init-fixpoints (&/|list))
 
-(defn ^:private check* [class-loader fixpoints expected actual]
+(defn ^:private check* [class-loader fixpoints invariant?? expected actual]
   (if (clojure.lang.Util/identical expected actual)
     (return (&/T fixpoints nil))
     (|case [expected actual]
@@ -704,13 +703,13 @@
               (return (&/T fixpoints nil)))
             
             [(&/$Some etype) (&/$None _)]
-            (check* class-loader fixpoints etype actual)
+            (check* class-loader fixpoints invariant?? etype actual)
 
             [(&/$None _) (&/$Some atype)]
-            (check* class-loader fixpoints expected atype)
+            (check* class-loader fixpoints invariant?? expected atype)
 
             [(&/$Some etype) (&/$Some atype)]
-            (check* class-loader fixpoints etype atype))))
+            (check* class-loader fixpoints invariant?? etype atype))))
       
       [(&/$VarT ?id) _]
       (fn [state]
@@ -720,7 +719,7 @@
 
           (&/$Left _)
           ((|do [bound (deref ?id)]
-             (check* class-loader fixpoints bound actual))
+             (check* class-loader fixpoints invariant?? bound actual))
            state)))
       
       [_ (&/$VarT ?id)]
@@ -731,12 +730,12 @@
 
           (&/$Left _)
           ((|do [bound (deref ?id)]
-             (check* class-loader fixpoints expected bound))
+             (check* class-loader fixpoints invariant?? expected bound))
            state)))
 
       [(&/$AppT (&/$ExT eid) eA) (&/$AppT (&/$ExT aid) aA)]
       (if (= eid aid)
-        (check* class-loader fixpoints eA aA)
+        (check* class-loader fixpoints invariant?? eA aA)
         (fail (check-error expected actual)))
 
       ;; [(&/$AppT (&/$VarT ?eid) A1) (&/$AppT (&/$VarT ?aid) A2)]
@@ -744,13 +743,13 @@
       ;;   (|case ((|do [F1 (deref ?eid)]
       ;;             (fn [state]
       ;;               (|case ((|do [F2 (deref ?aid)]
-      ;;                         (check* class-loader fixpoints (App$ F1 A1) (App$ F2 A2)))
+      ;;                         (check* class-loader fixpoints invariant?? (App$ F1 A1) (App$ F2 A2)))
       ;;                       state)
       ;;                 (&/$Right state* output)
       ;;                 (return* state* output)
 
       ;;                 (&/$Left _)
-      ;;                 ((check* class-loader fixpoints (App$ F1 A1) actual)
+      ;;                 ((check* class-loader fixpoints invariant?? (App$ F1 A1) actual)
       ;;                  state))))
       ;;           state)
       ;;     (&/$Right state* output)
@@ -758,70 +757,70 @@
 
       ;;     (&/$Left _)
       ;;     (|case ((|do [F2 (deref ?aid)]
-      ;;               (check* class-loader fixpoints expected (App$ F2 A2)))
+      ;;               (check* class-loader fixpoints invariant?? expected (App$ F2 A2)))
       ;;             state)
       ;;       (&/$Right state* output)
       ;;       (return* state* output)
 
       ;;       (&/$Left _)
-      ;;       ((|do [[fixpoints* _] (check* class-loader fixpoints (Var$ ?eid) (Var$ ?aid))
-      ;;              [fixpoints** _] (check* class-loader fixpoints* A1 A2)]
+      ;;       ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?eid) (Var$ ?aid))
+      ;;              [fixpoints** _] (check* class-loader fixpoints* invariant?? A1 A2)]
       ;;          (return (&/T fixpoints** nil)))
       ;;        state))))
       
-      ;; (|do [_ (check* class-loader fixpoints (Var$ ?eid) (Var$ ?aid))
-      ;;       _ (check* class-loader fixpoints A1 A2)]
+      ;; (|do [_ (check* class-loader fixpoints invariant?? (Var$ ?eid) (Var$ ?aid))
+      ;;       _ (check* class-loader fixpoints invariant?? A1 A2)]
       ;;   (return (&/T fixpoints nil)))
       
       [(&/$AppT (&/$VarT ?id) A1) (&/$AppT F2 A2)]
       (fn [state]
         (|case ((|do [F1 (deref ?id)]
-                  (check* class-loader fixpoints (App$ F1 A1) actual))
+                  (check* class-loader fixpoints invariant?? (App$ F1 A1) actual))
                 state)
           (&/$Right state* output)
           (return* state* output)
 
           (&/$Left _)
-          ((|do [[fixpoints* _] (check* class-loader fixpoints (Var$ ?id) F2)
+          ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?id) F2)
                  e* (apply-type F2 A1)
                  a* (apply-type F2 A2)
-                 [fixpoints** _] (check* class-loader fixpoints* e* a*)]
+                 [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
              (return (&/T fixpoints** nil)))
            state)))
       
       ;; [[&/$AppT [[&/$VarT ?id] A1]] [&/$AppT [F2 A2]]]
-      ;; (|do [[fixpoints* _] (check* class-loader fixpoints (Var$ ?id) F2)
+      ;; (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?id) F2)
       ;;       e* (apply-type F2 A1)
       ;;       a* (apply-type F2 A2)
-      ;;       [fixpoints** _] (check* class-loader fixpoints* e* a*)]
+      ;;       [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
       ;;   (return (&/T fixpoints** nil)))
       
       [(&/$AppT F1 A1) (&/$AppT (&/$VarT ?id) A2)]
       (fn [state]
         (|case ((|do [F2 (deref ?id)]
-                  (check* class-loader fixpoints expected (App$ F2 A2)))
+                  (check* class-loader fixpoints invariant?? expected (App$ F2 A2)))
                 state)
           (&/$Right state* output)
           (return* state* output)
 
           (&/$Left _)
-          ((|do [[fixpoints* _] (check* class-loader fixpoints F1 (Var$ ?id))
+          ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? F1 (Var$ ?id))
                  e* (apply-type F1 A1)
                  a* (apply-type F1 A2)
-                 [fixpoints** _] (check* class-loader fixpoints* e* a*)]
+                 [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
              (return (&/T fixpoints** nil)))
            state)))
       
       ;; [[&/$AppT [F1 A1]] [&/$AppT [[&/$VarT ?id] A2]]]
-      ;; (|do [[fixpoints* _] (check* class-loader fixpoints F1 (Var$ ?id))
+      ;; (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? F1 (Var$ ?id))
       ;;       e* (apply-type F1 A1)
       ;;       a* (apply-type F1 A2)
-      ;;       [fixpoints** _] (check* class-loader fixpoints* e* a*)]
+      ;;       [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
       ;;   (return (&/T fixpoints** nil)))
 
       ;; [(&/$AppT eF eA) (&/$AppT aF aA)]
-      ;; (|do [_ (check* class-loader fixpoints eF aF)]
-      ;;   (check* class-loader fixpoints eA aA))
+      ;; (|do [_ (check* class-loader fixpoints invariant?? eF aF)]
+      ;;   (check* class-loader fixpoints invariant?? eA aA))
       
       [(&/$AppT F A) _]
       (let [fp-pair (&/T expected actual)
@@ -842,44 +841,51 @@
 
           (&/$None)
           (|do [expected* (apply-type F A)]
-            (check* class-loader (fp-put fp-pair true fixpoints) expected* actual))))
+            (check* class-loader (fp-put fp-pair true fixpoints) invariant?? expected* actual))))
 
       [_ (&/$AppT F A)]
       (|do [actual* (apply-type F A)]
-        (check* class-loader fixpoints expected actual*))
+        (check* class-loader fixpoints invariant?? expected actual*))
 
       [(&/$UnivQ _) _]
       (with-var
         (fn [$arg]
           (|do [expected* (apply-type expected $arg)]
-            (check* class-loader fixpoints expected* actual))))
+            (check* class-loader fixpoints invariant?? expected* actual))))
 
       [_ (&/$UnivQ _)]
       (with-var
         (fn [$arg]
           (|do [actual* (apply-type actual $arg)]
-            (check* class-loader fixpoints expected actual*))))
+            (check* class-loader fixpoints invariant?? expected actual*))))
 
-      [(&/$DataT e!name) (&/$DataT "null")]
+      [(&/$DataT e!name e!params) (&/$DataT "null" (&/$Nil))]
       (if (contains? primitive-types e!name)
         (fail (str "[Type Error] Can't use \"null\" with primitive types."))
         (return (&/T fixpoints nil)))
 
-      [(&/$DataT e!name) (&/$DataT a!name)]
+      [(&/$DataT e!name e!params) (&/$DataT a!name a!params)]
       (let [e!name (as-obj e!name)
             a!name (as-obj a!name)]
-        (if (or (.equals ^Object e!name a!name)
-                (.isAssignableFrom (Class/forName e!name true class-loader) (Class/forName a!name true class-loader)))
-          (return (&/T fixpoints nil))
-          (fail (str "[Type Error] Names don't match: " e!name " =/= " 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)))
+
+              (and (not invariant??)
+                   (.isAssignableFrom (Class/forName e!name true class-loader) (Class/forName a!name true class-loader)))
+              (return (&/T fixpoints nil))
+
+              :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 aI eI)]
-        (check* class-loader fixpoints* eO aO))
+      (|do [[fixpoints* _] (check* class-loader fixpoints invariant?? aI eI)]
+        (check* class-loader fixpoints* invariant?? eO aO))
 
       [(&/$TupleT e!members) (&/$TupleT a!members)]
       (|do [fixpoints* (&/fold2% (fn [fp e a]
-                                   (|do [[fp* _] (check* class-loader fp e a)]
+                                   (|do [[fp* _] (check* class-loader fp invariant?? e a)]
                                      (return fp*)))
                                  fixpoints
                                  e!members a!members)]
@@ -887,7 +893,7 @@
       
       [(&/$VariantT e!cases) (&/$VariantT a!cases)]
       (|do [fixpoints* (&/fold2% (fn [fp e a]
-                                   (|do [[fp* _] (check* class-loader fp e a)]
+                                   (|do [[fp* _] (check* class-loader fp invariant?? e a)]
                                      (return fp*)))
                                  fixpoints
                                  e!cases a!cases)]
@@ -899,10 +905,10 @@
         (fail (check-error expected actual)))
 
       [(&/$NamedT ?ename ?etype) _]
-      (check* class-loader fixpoints ?etype actual)
+      (check* class-loader fixpoints invariant?? ?etype actual)
 
       [_ (&/$NamedT ?aname ?atype)]
-      (check* class-loader fixpoints expected ?atype)
+      (check* class-loader fixpoints invariant?? expected ?atype)
 
       [_ _]
       (fail (check-error expected actual))
@@ -910,29 +916,9 @@
 
 (defn check [expected actual]
   (|do [class-loader &/loader
-        _ (check* class-loader init-fixpoints expected actual)]
+        _ (check* class-loader init-fixpoints false expected actual)]
     (return nil)))
 
-(defn apply-lambda [func param]
-  (|case func
-    (&/$LambdaT input output)
-    (|do [_ (check* init-fixpoints input param)]
-      (return output))
-
-    (&/$UnivQ _)
-    (with-var
-      (fn [$var]
-        (|do [func* (apply-type func $var)
-              =return (apply-lambda func* param)]
-          (clean $var =return))))
-
-    (&/$NamedT ?name ?type)
-    (apply-lambda ?type param)
-
-    _
-    (fail (str "[Type System] Not a function type:\n" (show-type func) "\n"))
-    ))
-
 (defn actual-type [type]
   "(-> Type (Lux Type))"
   (|case type