- Fixed a bug when getting a value out of a variant (it was acting improperly when dealing with "composed" variants).

- Revamped the way variants are defined & used in the compiler.

2 files changed, 178 insertions, 202 deletions

diff --git a/src/lux/type.clj b/src/lux/type.clj
index d3a5f1493..9cb854c1e 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -25,143 +25,121 @@
     _
     false))
 
-(def empty-env &/Nil$)
-(defn Data$ [name params]
-  (&/V &/$DataT (&/T [name params])))
-(defn Bound$ [idx]
-  (&/V &/$BoundT idx))
-(defn Var$ [id]
-  (&/V &/$VarT id))
-(defn Lambda$ [in out]
-  (&/V &/$LambdaT (&/T [in out])))
-(defn App$ [fun arg]
-  (&/V &/$AppT (&/T [fun arg])))
-(defn Prod$ [left right]
-  (&/V &/$ProdT (&/T [left right])))
-(defn Sum$ [left right]
-  (&/V &/$SumT (&/T [left right])))
-(defn Univ$ [env body]
-  (&/V &/$UnivQ (&/T [env body])))
-(defn Ex$ [env body]
-  (&/V &/$ExQ (&/T [env body])))
-(defn Named$ [name type]
-  (&/V &/$NamedT (&/T [name type])))
-
-(def $Void (&/V &/$VoidT &/unit-tag))
-(def Unit (&/V &/$UnitT &/unit-tag))
-(def Bool (Named$ (&/T ["lux" "Bool"]) (Data$ "java.lang.Boolean" &/Nil$)))
-(def Int (Named$ (&/T ["lux" "Int"]) (Data$ "java.lang.Long" &/Nil$)))
-(def Real (Named$ (&/T ["lux" "Real"]) (Data$ "java.lang.Double" &/Nil$)))
-(def Char (Named$ (&/T ["lux" "Char"]) (Data$ "java.lang.Character" &/Nil$)))
-(def Text (Named$ (&/T ["lux" "Text"]) (Data$ "java.lang.String" &/Nil$)))
-(def Ident (Named$ (&/T ["lux" "Ident"]) (Prod$ Text Text)))
+(def empty-env &/$Nil)
+
+(def Bool (&/$NamedT (&/T ["lux" "Bool"]) (&/$DataT "java.lang.Boolean" &/$Nil)))
+(def Int (&/$NamedT (&/T ["lux" "Int"]) (&/$DataT "java.lang.Long" &/$Nil)))
+(def Real (&/$NamedT (&/T ["lux" "Real"]) (&/$DataT "java.lang.Double" &/$Nil)))
+(def Char (&/$NamedT (&/T ["lux" "Char"]) (&/$DataT "java.lang.Character" &/$Nil)))
+(def Text (&/$NamedT (&/T ["lux" "Text"]) (&/$DataT "java.lang.String" &/$Nil)))
+(def Ident (&/$NamedT (&/T ["lux" "Ident"]) (&/$ProdT Text Text)))
 
 (def IO
-  (Named$ (&/T ["lux/codata" "IO"])
-          (Univ$ empty-env
-                 (Lambda$ $Void (Bound$ 1)))))
+  (&/$NamedT (&/T ["lux/codata" "IO"])
+             (&/$UnivQ empty-env
+                       (&/$LambdaT &/$VoidT (&/$BoundT 1)))))
 
 (def List
-  (Named$ (&/T ["lux" "List"])
-          (Univ$ empty-env
-                 (Sum$
-                  ;; lux;Nil
-                  Unit
-                  ;; lux;Cons
-                  (Prod$ (Bound$ 1)
-                         (App$ (Bound$ 0)
-                               (Bound$ 1)))))))
+  (&/$NamedT (&/T ["lux" "List"])
+             (&/$UnivQ empty-env
+                       (&/$SumT
+                        ;; lux;Nil
+                        &/$UnitT
+                        ;; lux;Cons
+                        (&/$ProdT (&/$BoundT 1)
+                                  (&/$AppT (&/$BoundT 0)
+                                           (&/$BoundT 1)))))))
 
 (def Maybe
-  (Named$ (&/T ["lux" "Maybe"])
-          (Univ$ empty-env
-                 (Sum$
-                  ;; lux;None
-                  Unit
-                  ;; lux;Some
-                  (Bound$ 1))
-                 )))
+  (&/$NamedT (&/T ["lux" "Maybe"])
+             (&/$UnivQ empty-env
+                       (&/$SumT
+                        ;; lux;None
+                        &/$UnitT
+                        ;; lux;Some
+                        (&/$BoundT 1))
+                       )))
 
 (def Type
-  (Named$ (&/T ["lux" "Type"])
-          (let [Type (App$ (Bound$ 0) (Bound$ 1))
-                TypeList (App$ List Type)
-                TypePair (Prod$ Type Type)]
-            (App$ (Univ$ empty-env
-                         (Sum$
-                          ;; DataT
-                          (Prod$ Text TypeList)
-                          (Sum$
-                           ;; VoidT
-                           Unit
-                           (Sum$
-                            ;; UnitT
-                            Unit
-                            (Sum$
-                             ;; SumT
-                             TypePair
-                             (Sum$
-                              ;; ProdT
-                              TypePair
-                              (Sum$
-                               ;; LambdaT
-                               TypePair
-                               (Sum$
-                                ;; BoundT
-                                Int
-                                (Sum$
-                                 ;; VarT
-                                 Int
-                                 (Sum$
-                                  ;; ExT
-                                  Int
-                                  (Sum$
-                                   ;; UnivQ
-                                   (Prod$ TypeList Type)
-                                   (Sum$
-                                    ;; ExQ
-                                    (Prod$ TypeList Type)
-                                    (Sum$
-                                     ;; AppT
-                                     TypePair
-                                     ;; NamedT
-                                     (Prod$ Ident Type)))))))))))))
-                         )
-                  $Void))))
+  (&/$NamedT (&/T ["lux" "Type"])
+             (let [Type (&/$AppT (&/$BoundT 0) (&/$BoundT 1))
+                   TypeList (&/$AppT List Type)
+                   TypePair (&/$ProdT Type Type)]
+               (&/$AppT (&/$UnivQ empty-env
+                                  (&/$SumT
+                                   ;; DataT
+                                   (&/$ProdT Text TypeList)
+                                   (&/$SumT
+                                    ;; VoidT
+                                    &/$UnitT
+                                    (&/$SumT
+                                     ;; UnitT
+                                     &/$UnitT
+                                     (&/$SumT
+                                      ;; SumT
+                                      TypePair
+                                      (&/$SumT
+                                       ;; ProdT
+                                       TypePair
+                                       (&/$SumT
+                                        ;; LambdaT
+                                        TypePair
+                                        (&/$SumT
+                                         ;; BoundT
+                                         Int
+                                         (&/$SumT
+                                          ;; VarT
+                                          Int
+                                          (&/$SumT
+                                           ;; ExT
+                                           Int
+                                           (&/$SumT
+                                            ;; UnivQ
+                                            (&/$ProdT TypeList Type)
+                                            (&/$SumT
+                                             ;; ExQ
+                                             (&/$ProdT TypeList Type)
+                                             (&/$SumT
+                                              ;; AppT
+                                              TypePair
+                                              ;; NamedT
+                                              (&/$ProdT Ident Type)))))))))))))
+                                  )
+                        &/$VoidT))))
 
 (def DefMetaValue
-  (Named$ (&/T ["lux" "DefMetaValue"])
-          (let [DefMetaValue (App$ (Bound$ 0) (Bound$ 1))]
-            (App$ (Univ$ empty-env
-                         (Sum$
-                          ;; BoolM
-                          Bool
-                          (Sum$
-                           ;; IntM
-                           Int
-                           (Sum$
-                            ;; RealM
-                            Real
-                            (Sum$
-                             ;; CharM
-                             Char
-                             (Sum$
-                              ;; TextM
-                              Text
-                              (Sum$
-                               ;; IdentM
-                               Ident
-                               (Sum$
-                                ;; ListM
-                                (App$ List DefMetaValue)
-                                ;; DictM
-                                (App$ List (Prod$ Text DefMetaValue)))))))))
-                         )
-                  $Void))))
+  (&/$NamedT (&/T ["lux" "DefMetaValue"])
+             (let [DefMetaValue (&/$AppT (&/$BoundT 0) (&/$BoundT 1))]
+               (&/$AppT (&/$UnivQ empty-env
+                                  (&/$SumT
+                                   ;; BoolM
+                                   Bool
+                                   (&/$SumT
+                                    ;; IntM
+                                    Int
+                                    (&/$SumT
+                                     ;; RealM
+                                     Real
+                                     (&/$SumT
+                                      ;; CharM
+                                      Char
+                                      (&/$SumT
+                                       ;; TextM
+                                       Text
+                                       (&/$SumT
+                                        ;; IdentM
+                                        Ident
+                                        (&/$SumT
+                                         ;; ListM
+                                         (&/$AppT List DefMetaValue)
+                                         ;; DictM
+                                         (&/$AppT List (&/$ProdT Text DefMetaValue)))))))))
+                                  )
+                        &/$VoidT))))
 
 (def DefMeta
-  (Named$ (&/T ["lux" "DefMeta"])
-          (App$ List (Prod$ Ident DefMetaValue))))
+  (&/$NamedT (&/T ["lux" "DefMeta"])
+             (&/$AppT List (&/$ProdT Ident DefMetaValue))))
 
 (def Macro)
 
@@ -208,7 +186,7 @@
         (fail* (str "[Type Error] Can't rebind type var: " id " | Current type: " (show-type bound)))
         
         (&/$None)
-        (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/V &/$Some type) %)
+        (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/$Some type) %)
                                                             ts))
                             state)
                  nil))
@@ -221,14 +199,14 @@
     (let [id (->> state (&/get$ &/$type-vars) (&/get$ &/$counter))]
       (return* (&/update$ &/$type-vars #(->> %
                                              (&/update$ &/$counter inc)
-                                             (&/update$ &/$mappings (fn [ms] (&/|put id &/None$ ms))))
+                                             (&/update$ &/$mappings (fn [ms] (&/|put id &/$None ms))))
                           state)
                id))))
 
 (def existential
   ;; (Lux Type)
   (|do [seed &/gen-id]
-    (return (&/V &/$ExT seed))))
+    (return (&/$ExT seed))))
 
 (declare clean*)
 (defn ^:private delete-var [id]
@@ -250,12 +228,12 @@
                                        (|case ?type*
                                          (&/$VarT ?id*)
                                          (if (.equals ^Object id ?id*)
-                                           (return (&/T [?id &/None$]))
+                                           (return (&/T [?id &/$None]))
                                            (return binding))
 
                                          _
                                          (|do [?type** (clean* id ?type*)]
-                                           (return (&/T [?id (&/V &/$Some ?type**)]))))
+                                           (return (&/T [?id (&/$Some ?type**)]))))
                                        ))))
                                (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings)))]
          (fn [state]
@@ -266,7 +244,7 @@
 
 (defn with-var [k]
   (|do [id create-var
-        output (k (Var$ id))
+        output (k (&/$VarT id))
         _ (delete-var id)]
     (return output)))
 
@@ -282,32 +260,32 @@
 
     (&/$DataT ?name ?params)
     (|do [=params (&/map% (partial clean* ?tid) ?params)]
-      (return (Data$ ?name =params)))
+      (return (&/$DataT ?name =params)))
     
     (&/$LambdaT ?arg ?return)
     (|do [=arg (clean* ?tid ?arg)
           =return (clean* ?tid ?return)]
-      (return (Lambda$ =arg =return)))
+      (return (&/$LambdaT =arg =return)))
 
     (&/$AppT ?lambda ?param)
     (|do [=lambda (clean* ?tid ?lambda)
           =param (clean* ?tid ?param)]
-      (return (App$ =lambda =param)))
+      (return (&/$AppT =lambda =param)))
 
     (&/$ProdT ?left ?right)
     (|do [=left (clean* ?tid ?left)
           =right (clean* ?tid ?right)]
-      (return (Prod$ =left =right)))
+      (return (&/$ProdT =left =right)))
     
     (&/$SumT ?left ?right)
     (|do [=left (clean* ?tid ?left)
           =right (clean* ?tid ?right)]
-      (return (Sum$ =left =right)))
+      (return (&/$SumT =left =right)))
 
     (&/$UnivQ ?env ?body)
     (|do [=env (&/map% (partial clean* ?tid) ?env)
           body* (clean* ?tid ?body)]
-      (return (Univ$ =env body*)))
+      (return (&/$UnivQ =env body*)))
 
     _
     (return type)
@@ -325,10 +303,10 @@
   (|case type
     (&/$LambdaT ?in ?out)
     (|let [[??out ?args] (unravel-fun ?out)]
-      (&/T [??out (&/Cons$ ?in ?args)]))
+      (&/T [??out (&/$Cons ?in ?args)]))
 
     _
-    (&/T [type &/Nil$])))
+    (&/T [type &/$Nil])))
 
 (defn ^:private unravel-app [fun-type]
   (|case fun-type
@@ -337,14 +315,14 @@
       (&/T [?fun-type (&/|++ ?args (&/|list ?right))]))
 
     _
-    (&/T [fun-type &/Nil$])))
+    (&/T [fun-type &/$Nil])))
 
 (do-template [<tag> <flatten> <at> <desc>]
   (do (defn <flatten> [type]
         "(-> Type (List Type))"
         (|case type
           (<tag> left right)
-          (&/Cons$ left (<flatten> right))
+          (&/$Cons left (<flatten> right))
 
           _
           (&/|list type)))
@@ -380,8 +358,8 @@
       (&/$Nil)
       <unit>))
 
-  Variant$ Sum$  $Void
-  Tuple$   Prod$ Unit
+  Variant$ &/$SumT  &/$VoidT
+  Tuple$   &/$ProdT &/$UnitT
   )
 
 (defn show-type [^objects type]
@@ -495,17 +473,17 @@
   (|let [[e a] k]
     (|case fixpoints
       (&/$Nil)
-      &/None$
+      &/$None
 
       (&/$Cons [[e* a*] v*] fixpoints*)
       (if (and (type= e e*)
                (type= a a*))
-        (&/V &/$Some v*)
+        (&/$Some v*)
         (fp-get k fixpoints*))
       )))
 
 (defn ^:private fp-put [k v fixpoints]
-  (&/Cons$ (&/T [k v]) fixpoints))
+  (&/$Cons (&/T [k v]) fixpoints))
 
 (defn show-type+ [type]
   (|case type
@@ -533,31 +511,31 @@
 (defn beta-reduce [env type]
   (|case type
     (&/$DataT ?name ?params)
-    (Data$ ?name (&/|map (partial beta-reduce env) ?params))
+    (&/$DataT ?name (&/|map (partial beta-reduce env) ?params))
 
     (&/$SumT ?left ?right)
     (let [=left (beta-reduce env ?left)
           =right (beta-reduce env ?right)]
-      (Sum$ =left =right))
+      (&/$SumT =left =right))
 
     (&/$ProdT ?left ?right)
     (let [=left (beta-reduce env ?left)
           =right (beta-reduce env ?right)]
-      (Prod$ =left =right))
+      (&/$ProdT =left =right))
 
     (&/$AppT ?type-fn ?type-arg)
-    (App$ (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
+    (&/$AppT (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
 
     (&/$UnivQ ?local-env ?local-def)
     (|case ?local-env
       (&/$Nil)
-      (Univ$ env ?local-def)
+      (&/$UnivQ env ?local-def)
 
       _
       type)
 
     (&/$LambdaT ?input ?output)
-    (Lambda$ (beta-reduce env ?input) (beta-reduce env ?output))
+    (&/$LambdaT (beta-reduce env ?input) (beta-reduce env ?output))
 
     (&/$BoundT ?idx)
     (|case (&/|at ?idx env)
@@ -575,14 +553,14 @@
   (|case type-fn
     (&/$UnivQ local-env local-def)
     (return (beta-reduce (->> local-env
-                              (&/Cons$ param)
-                              (&/Cons$ type-fn))
+                              (&/$Cons param)
+                              (&/$Cons type-fn))
                          local-def))
 
     (&/$ExQ local-env local-def)
     (return (beta-reduce (->> local-env
-                              (&/Cons$ param)
-                              (&/Cons$ type-fn))
+                              (&/$Cons param)
+                              (&/$Cons type-fn))
                          local-def))
 
     (&/$AppT F A)
@@ -593,12 +571,12 @@
     (apply-type ?type param)
 
     (&/$ExT id)
-    (return (App$ type-fn param))
+    (return (&/$AppT type-fn param))
     
     _
     (fail (str "[Type System] Not a type function:\n" (show-type type-fn) "\n"))))
 
-(def ^:private init-fixpoints &/Nil$)
+(def ^:private init-fixpoints &/$Nil)
 
 (defn ^:private check* [class-loader fixpoints invariant?? expected actual]
   (if (clojure.lang.Util/identical expected actual)
@@ -611,17 +589,17 @@
           (|do [ebound (fn [state]
                          (|case ((deref ?eid) state)
                            (&/$Right state* ebound)
-                           (return* state* (&/V &/$Some ebound))
+                           (return* state* (&/$Some ebound))
 
                            (&/$Left _)
-                           (return* state &/None$)))
+                           (return* state &/$None)))
                 abound (fn [state]
                          (|case ((deref ?aid) state)
                            (&/$Right state* abound)
-                           (return* state* (&/V &/$Some abound))
+                           (return* state* (&/$Some abound))
 
                            (&/$Left _)
-                           (return* state &/None$)))]
+                           (return* state &/$None)))]
             (|case [ebound abound]
               [(&/$None _) (&/$None _)]
               (|do [_ (set-var ?eid actual)]
@@ -666,13 +644,13 @@
         [(&/$AppT (&/$VarT ?id) A1) (&/$AppT F2 A2)]
         (fn [state]
           (|case ((|do [F1 (deref ?id)]
-                    (check* class-loader fixpoints invariant?? (App$ F1 A1) actual))
+                    (check* class-loader fixpoints invariant?? (&/$AppT F1 A1) actual))
                   state)
             (&/$Right state* output)
             (return* state* output)
 
             (&/$Left _)
-            ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (Var$ ?id) F2)
+            ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? (&/$VarT ?id) F2)
                    e* (apply-type F2 A1)
                    a* (apply-type F2 A2)
                    [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
@@ -682,13 +660,13 @@
         [(&/$AppT F1 A1) (&/$AppT (&/$VarT ?id) A2)]
         (fn [state]
           (|case ((|do [F2 (deref ?id)]
-                    (check* class-loader fixpoints invariant?? expected (App$ F2 A2)))
+                    (check* class-loader fixpoints invariant?? expected (&/$AppT F2 A2)))
                   state)
             (&/$Right state* output)
             (return* state* output)
 
             (&/$Left _)
-            ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? F1 (Var$ ?id))
+            ((|do [[fixpoints* _] (check* class-loader fixpoints invariant?? F1 (&/$VarT ?id))
                    e* (apply-type F1 A1)
                    a* (apply-type F1 A2)
                    [fixpoints** _] (check* class-loader fixpoints* invariant?? e* a*)]
@@ -724,7 +702,7 @@
         (|do [$arg existential
               expected* (apply-type expected $arg)]
           (check* class-loader fixpoints invariant?? expected* actual))
-        
+
         [_ (&/$UnivQ _)]
         (with-var
           (fn [$arg]
@@ -735,16 +713,16 @@
         (with-var
           (fn [$arg]
             (|let [expected* (beta-reduce (->> e!env
-                                               (&/Cons$ $arg)
-                                               (&/Cons$ expected))
+                                               (&/$Cons $arg)
+                                               (&/$Cons expected))
                                           e!def)]
               (check* class-loader fixpoints invariant?? expected* actual))))
 
         [_ (&/$ExQ a!env a!def)]
         (|do [$arg existential]
           (|let [actual* (beta-reduce (->> a!env
-                                           (&/Cons$ $arg)
-                                           (&/Cons$ expected))
+                                           (&/$Cons $arg)
+                                           (&/$Cons expected))
                                       a!def)]
             (check* class-loader fixpoints invariant?? expected actual*)))
 
@@ -852,12 +830,12 @@
   (|let [?member-types (flatten-prod type)
          size-types (&/|length ?member-types)]
     (if (not (>= size-types size-members))
-      &/None$
+      &/$None
       (|let [?member-types* (if (= size-types size-members)
                               ?member-types
                               (&/|++ (&/|take (dec size-members) ?member-types)
                                      (&/|list (|case (->> (&/|drop (dec size-members) ?member-types) (&/|reverse))
                                                 (&/$Cons last prevs)
-                                                (&/fold (fn [right left] (Prod$ left right))
+                                                (&/fold (fn [right left] (&/$ProdT left right))
                                                         last prevs)))))]
-        (&/Some$ ?member-types*)))))
+        (&/$Some ?member-types*)))))
diff --git a/src/lux/type/host.clj b/src/lux/type/host.clj
index ae225db1f..531169538 100644
--- a/src/lux/type/host.clj
+++ b/src/lux/type/host.clj
@@ -29,26 +29,26 @@
                  stack (&/|list)]
             (let [super-interface (some valid-sub? (.getInterfaces sub-class))]
               (if (= super-class super-interface)
-                (&/Cons$ super-interface stack)
-                (recur super-interface (&/Cons$ super-interface stack)))))
+                (&/$Cons super-interface stack)
+                (recur super-interface (&/$Cons super-interface stack)))))
 
           (.isInterface super-class)
           (loop [sub-class sub-class
                  stack (&/|list)]
             (if-let [super-interface (some valid-sub? (.getInterfaces sub-class))]
               (if (= super-class super-interface)
-                (&/Cons$ super-interface stack)
-                (recur super-interface (&/Cons$ super-interface stack)))
+                (&/$Cons super-interface stack)
+                (recur super-interface (&/$Cons super-interface stack)))
               (let [super* (.getSuperclass sub-class)]
-                (recur super* (&/Cons$ super* stack)))))
+                (recur super* (&/$Cons super* stack)))))
 
           :else
           (loop [sub-class sub-class
                  stack (&/|list)]
             (let [super* (.getSuperclass sub-class)]
               (if (= super* super-class)
-                (&/Cons$ super* stack)
-                (recur super* (&/Cons$ super* stack))))))))
+                (&/$Cons super* stack)
+                (recur super* (&/$Cons super* stack))))))))
 
 (defn ^:private trace-lineage [^Class sub-class ^Class super-class]
   "(-> Class Class (List Class))"
@@ -56,7 +56,7 @@
     (&/|list)
     (&/|reverse (trace-lineage* super-class sub-class))))
 
-(let [matcher (fn [m ^TypeVariable jt lt] (&/Cons$ (&/T [(.getName jt) lt]) m))]
+(let [matcher (fn [m ^TypeVariable jt lt] (&/$Cons (&/T [(.getName jt) lt]) m))]
   (defn ^:private match-params [sub-type-params params]
     (assert (and (= (&/|length sub-type-params) (&/|length params))
                  (&/|every? (partial instance? TypeVariable) sub-type-params)))
@@ -64,7 +64,6 @@
 
 ;; [Exports]
 (let [class-name-re #"((\[+)L([\.a-zA-Z0-9]+);|([\.a-zA-Z0-9]+)|(\[+)([ZBSIJFDC]))"
-      Unit (&/V &/$UnitT &/unit-tag)
       jprim->lprim (fn [prim]
                      (case prim
                        "Z" "boolean"
@@ -80,9 +79,9 @@
     (if-let [[_ _ arr-obrackets arr-obase simple-base arr-pbrackets arr-pbase] (re-find class-name-re (.getName class))]
       (let [base (or arr-obase simple-base (jprim->lprim arr-pbase))]
         (if (.equals "void" base)
-          Unit
-          (reduce (fn [inner _] (&/V &/$DataT (&/T [array-data-tag (&/|list inner)])))
-                  (&/V &/$DataT (&/T [base &/Nil$]))
+          &/$UnitT
+          (reduce (fn [inner _] (&/$DataT array-data-tag (&/|list inner)))
+                  (&/$DataT base &/$Nil)
                   (range (count (or arr-obrackets arr-pbrackets "")))))
         ))))
 
@@ -93,7 +92,7 @@
 
         (instance? GenericArrayType refl-type)
         (|do [inner-type (instance-param existential matchings (.getGenericComponentType ^GenericArrayType refl-type))]
-          (return (&/V &/$DataT (&/T [array-data-tag (&/|list inner-type)]))))
+          (return (&/$DataT array-data-tag (&/|list inner-type))))
         
         (instance? ParameterizedType refl-type)
         (|do [:let [refl-type* ^ParameterizedType refl-type]
@@ -101,8 +100,8 @@
                            .getActualTypeArguments
                            seq &/->list
                            (&/map% (partial instance-param existential matchings)))]
-          (return (&/V &/$DataT (&/T [(->> refl-type* ^Class (.getRawType) .getName)
-                                      params*]))))
+          (return (&/$DataT (->> refl-type* ^Class (.getRawType) .getName)
+                            params*)))
         
         (instance? TypeVariable refl-type)
         (let [gvar (.getName ^TypeVariable refl-type)]
@@ -123,15 +122,14 @@
   (|case gtype
     (&/$GenericArray component-type)
     (|do [inner-type (instance-gtype existential matchings component-type)]
-      (return (&/V &/$DataT (&/T [array-data-tag (&/|list inner-type)]))))
+      (return (&/$DataT array-data-tag (&/|list inner-type))))
     
     (&/$GenericClass type-name type-params)
     (if-let [m-type (&/|get type-name matchings)]
       (return m-type)
       (|do [params* (&/map% (partial instance-gtype existential matchings)
                             type-params)]
-        (return (&/V &/$DataT (&/T [type-name
-                                    params*])))))
+        (return (&/$DataT type-name params*))))
     
     (&/$GenericTypeVar var-name)
     (if-let [m-type (&/|get var-name matchings)]
@@ -191,7 +189,7 @@
     (if (.isAssignableFrom super-class+ sub-class+)
       (let [lineage (trace-lineage sub-class+ super-class+)]
         (|do [[^Class sub-class* sub-params*] (raise existential lineage sub-class+ sub-params)]
-          (return (&/V &/$DataT (&/T [(.getName sub-class*) sub-params*])))))
+          (return (&/$DataT (.getName sub-class*) sub-params*))))
       (fail (str "[Type Error] Classes don't have a subtyping relationship: " sub-class " </= " super-class)))))
 
 (defn as-obj [class]
@@ -220,16 +218,16 @@
                (= null-data-tag a!name)
                (if (not (primitive-type? e!name))
                  (return (&/T [fixpoints nil]))
-                 (check-error "" (&/V &/$DataT expected) (&/V &/$DataT actual)))
+                 (check-error "" (&/$DataT e!name e!params) (&/$DataT a!name a!params)))
 
                (= null-data-tag e!name)
                (if (= null-data-tag a!name)
                  (return (&/T [fixpoints nil]))
-                 (check-error "" (&/V &/$DataT expected) (&/V &/$DataT actual)))
+                 (check-error "" (&/$DataT e!name e!params) (&/$DataT a!name a!params)))
 
                (and (= array-data-tag e!name)
                     (not= array-data-tag a!name))
-               (check-error "" (&/V &/$DataT expected) (&/V &/$DataT actual))
+               (check-error "" (&/$DataT e!name e!params) (&/$DataT a!name a!params))
                
                :else
                (let [e!name (as-obj e!name)
@@ -242,7 +240,7 @@
 
                        (not invariant??)
                        (|do [actual* (->super-type existential class-loader e!name a!name a!params)]
-                         (check (&/V &/$DataT expected) actual*))
+                         (check (&/$DataT e!name e!params) actual*))
 
                        :else
                        (fail (str "[Type Error] Names don't match: " e!name " =/= " a!name)))))
@@ -253,10 +251,10 @@
 (defn gtype->gclass [gtype]
   "(-> GenericType GenericClass)"
   (cond (instance? Class gtype)
-        (&/V &/$GenericClass (&/T [(.getName ^Class gtype) &/Nil$]))
+        (&/$GenericClass (.getName ^Class gtype) &/$Nil)
 
         (instance? GenericArrayType gtype)
-        (&/V &/$GenericArray (gtype->gclass (.getGenericComponentType ^GenericArrayType gtype)))
+        (&/$GenericArray (gtype->gclass (.getGenericComponentType ^GenericArrayType gtype)))
 
         (instance? ParameterizedType gtype)
         (let [type-name (->> ^ParameterizedType gtype ^Class (.getRawType) .getName)
@@ -264,12 +262,12 @@
                                .getActualTypeArguments
                                seq &/->list
                                (&/|map gtype->gclass))]
-          (&/V &/$GenericClass (&/T [type-name type-params])))
+          (&/$GenericClass type-name type-params))
 
         (instance? TypeVariable gtype)
-        (&/V &/$GenericTypeVar (.getName ^TypeVariable gtype))
+        (&/$GenericTypeVar (.getName ^TypeVariable gtype))
 
         (instance? WildcardType gtype)
         (if-let [bound (->> ^WildcardType gtype .getUpperBounds seq first)]
           (gtype->gclass bound)
-          (&/V &/$GenericWildcard &/unit-tag))))
+          &/$GenericWildcard)))