15 files changed, 694 insertions, 694 deletions

diff --git a/luxc/src/lux/analyser.clj b/luxc/src/lux/analyser.clj
index 18bfdcd3e..1c854acb9 100644
--- a/luxc/src/lux/analyser.clj
+++ b/luxc/src/lux/analyser.clj
@@ -26,7 +26,7 @@
       (|do [_cursor &/cursor]
         (analyse exo-type (&/T [_cursor (&/$Tuple values)])))
       (|case exo-type
-        (&/$VarT id)
+        (&/$Var id)
         (|do [? (&type/bound? id)]
           (if (or ? (&&/type-tag? module tag-name))
             (&&lux/analyse-variant analyse (&/$Right exo-type) idx is-last? values)
@@ -46,7 +46,7 @@
     (fn [?var]
       (|do [[[?output-type ?output-cursor] ?output-term] (&&/analyse-1 analyser ?var syntax)]
         (|case [?var ?output-type]
-          [(&/$VarT ?e-id) (&/$VarT ?a-id)]
+          [(&/$Var ?e-id) (&/$Var ?a-id)]
           (if (= ?e-id ?a-id)
             (|do [=output-type (&type/clean ?var ?output-type)]
               (return (&&/|meta =output-type ?output-cursor ?output-term)))
@@ -203,7 +203,7 @@
 ;; [Resources]
 (defn analyse [optimize eval! compile-module compilers]
   (|do [asts &parser/parse]
-    (&/flat-map% (partial analyse-ast optimize eval! compile-module compilers &/$VoidT) asts)))
+    (&/flat-map% (partial analyse-ast optimize eval! compile-module compilers &/$Void) asts)))
 
 (defn clean-output [?var analysis]
   (|do [:let [[[?output-type ?output-cursor] ?output-term] analysis]
diff --git a/luxc/src/lux/analyser/base.clj b/luxc/src/lux/analyser/base.clj
index e1678fb2b..e762c3870 100644
--- a/luxc/src/lux/analyser/base.clj
+++ b/luxc/src/lux/analyser/base.clj
@@ -75,7 +75,7 @@
                   (return ?module))]
     (return (&/T [module* ?name]))))
 
-(let [tag-names #{"HostT" "VoidT" "UnitT" "SumT" "ProdT" "FunctionT" "BoundT" "VarT" "ExT" "UnivQ" "ExQ" "AppT" "NamedT"}]
+(let [tag-names #{"Host" "Void" "Unit" "Sum" "Product" "Function" "Bound" "Var" "Ex" "UnivQ" "ExQ" "App" "Named"}]
   (defn type-tag? [module name]
     (and (= "lux" module)
          (contains? tag-names name))))
diff --git a/luxc/src/lux/analyser/case.clj b/luxc/src/lux/analyser/case.clj
index 1e3214dad..613e415f5 100644
--- a/luxc/src/lux/analyser/case.clj
+++ b/luxc/src/lux/analyser/case.clj
@@ -41,7 +41,7 @@
 
 (defn ^:private resolve-type [type]
   (|case type
-    (&/$VarT ?id)
+    (&/$Var ?id)
     (|do [type* (&/try-all% (&/|list (&type/deref ?id)
                                      (&/fail-with-loc "##1##")))]
       (resolve-type type*))
@@ -65,30 +65,30 @@
 
 (defn clean! [level ?tid bound-idx type]
   (|case type
-    (&/$VarT ?id)
+    (&/$Var ?id)
     (if (= ?tid ?id)
-      (&/$BoundT (+ (* 2 level) bound-idx))
+      (&/$Bound (+ (* 2 level) bound-idx))
       type)
 
-    (&/$HostT ?name ?params)
-    (&/$HostT ?name (&/|map (partial clean! level ?tid bound-idx)
-                            ?params))
+    (&/$Host ?name ?params)
+    (&/$Host ?name (&/|map (partial clean! level ?tid bound-idx)
+                           ?params))
     
-    (&/$FunctionT ?arg ?return)
-    (&/$FunctionT (clean! level ?tid bound-idx ?arg)
-                  (clean! level ?tid bound-idx ?return))
+    (&/$Function ?arg ?return)
+    (&/$Function (clean! level ?tid bound-idx ?arg)
+                 (clean! level ?tid bound-idx ?return))
 
-    (&/$AppT ?lambda ?param)
-    (&/$AppT (clean! level ?tid bound-idx ?lambda)
-             (clean! level ?tid bound-idx ?param))
+    (&/$App ?lambda ?param)
+    (&/$App (clean! level ?tid bound-idx ?lambda)
+            (clean! level ?tid bound-idx ?param))
 
-    (&/$ProdT ?left ?right)
-    (&/$ProdT (clean! level ?tid bound-idx ?left)
-              (clean! level ?tid bound-idx ?right))
+    (&/$Product ?left ?right)
+    (&/$Product (clean! level ?tid bound-idx ?left)
+                (clean! level ?tid bound-idx ?right))
     
-    (&/$SumT ?left ?right)
-    (&/$SumT (clean! level ?tid bound-idx ?left)
-             (clean! level ?tid bound-idx ?right))
+    (&/$Sum ?left ?right)
+    (&/$Sum (clean! level ?tid bound-idx ?left)
+            (clean! level ?tid bound-idx ?right))
 
     (&/$UnivQ ?env ?body)
     (&/$UnivQ (&/|map (partial clean! level ?tid bound-idx) ?env)
@@ -104,20 +104,20 @@
 
 (defn beta-reduce! [level env type]
   (|case type
-    (&/$HostT ?name ?params)
-    (&/$HostT ?name (&/|map (partial beta-reduce! level env) ?params))
+    (&/$Host ?name ?params)
+    (&/$Host ?name (&/|map (partial beta-reduce! level env) ?params))
 
-    (&/$SumT ?left ?right)
-    (&/$SumT (beta-reduce! level env ?left)
-             (beta-reduce! level env ?right))
+    (&/$Sum ?left ?right)
+    (&/$Sum (beta-reduce! level env ?left)
+            (beta-reduce! level env ?right))
 
-    (&/$ProdT ?left ?right)
-    (&/$ProdT (beta-reduce! level env ?left)
-              (beta-reduce! level env ?right))
+    (&/$Product ?left ?right)
+    (&/$Product (beta-reduce! level env ?left)
+                (beta-reduce! level env ?right))
 
-    (&/$AppT ?type-fn ?type-arg)
-    (&/$AppT (beta-reduce! level env ?type-fn)
-             (beta-reduce! level env ?type-arg))
+    (&/$App ?type-fn ?type-arg)
+    (&/$App (beta-reduce! level env ?type-fn)
+            (beta-reduce! level env ?type-arg))
     
     (&/$UnivQ ?local-env ?local-def)
     (|case ?local-env
@@ -135,11 +135,11 @@
       _
       type)
 
-    (&/$FunctionT ?input ?output)
-    (&/$FunctionT (beta-reduce! level env ?input)
-                  (beta-reduce! level env ?output))
+    (&/$Function ?input ?output)
+    (&/$Function (beta-reduce! level env ?input)
+                 (beta-reduce! level env ?output))
 
-    (&/$BoundT ?idx)
+    (&/$Bound ?idx)
     (|case (&/|at (- ?idx (* 2 level)) env)
       (&/$Some bound)
       (beta-reduce! level env bound)
@@ -165,17 +165,17 @@
                                  (&/$Cons type-fn))
                           local-def))
 
-    (&/$AppT F A)
+    (&/$App F A)
     (|do [type-fn* (apply-type! F A)]
       (apply-type! type-fn* param))
 
-    (&/$NamedT ?name ?type)
+    (&/$Named ?name ?type)
     (apply-type! ?type param)
 
-    (&/$ExT id)
-    (return (&/$AppT type-fn param))
+    (&/$Ex id)
+    (return (&/$App type-fn param))
 
-    (&/$VarT id)
+    (&/$Var id)
     (|do [=type-fun (deref id)]
       (apply-type! =type-fun param))
     
@@ -199,9 +199,9 @@
           =type (apply-type! type $var)]
       (adjust-type* up =type))
 
-    (&/$ProdT ?left ?right)
+    (&/$Product ?left ?right)
     (let [=type (&/fold (fn [_abody ena]
-                          (|let [[_aenv _aidx (&/$VarT _avar)] ena]
+                          (|let [[_aenv _aidx (&/$Var _avar)] ena]
                             (clean! 0 _avar _aidx _abody)))
                         type
                         up)
@@ -214,9 +214,9 @@
       (return (&type/Tuple$ (&/|map distributor
                                     (&type/flatten-prod =type)))))
 
-    (&/$SumT ?left ?right)
+    (&/$Sum ?left ?right)
     (let [=type (&/fold (fn [_abody ena]
-                          (|let [[_aenv _aidx (&/$VarT _avar)] ena]
+                          (|let [[_aenv _aidx (&/$Var _avar)] ena]
                             (clean! 0 _avar _aidx _abody)))
                         type
                         up)
@@ -229,19 +229,19 @@
       (return (&type/Variant$ (&/|map distributor
                                       (&type/flatten-sum =type)))))
 
-    (&/$AppT ?tfun ?targ)
+    (&/$App ?tfun ?targ)
     (|do [=type (apply-type! ?tfun ?targ)]
       (adjust-type* up =type))
 
-    (&/$VarT ?id)
+    (&/$Var ?id)
     (|do [type* (&/try-all% (&/|list (&type/deref ?id)
                                      (&/fail-with-loc (str "##2##: " ?id))))]
       (adjust-type* up type*))
 
-    (&/$NamedT ?name ?type)
+    (&/$Named ?name ?type)
     (adjust-type* up ?type)
 
-    (&/$UnitT)
+    (&/$Unit)
     (return type)
 
     _
@@ -309,7 +309,7 @@
       (&/$Tuple ?members)
       (|case ?members
         (&/$Nil)
-        (|do [_ (&type/check value-type &/$UnitT)
+        (|do [_ (&type/check value-type &/$Unit)
               =kont kont]
           (return (&/T [($TupleTestAC (&/|list)) =kont])))
 
@@ -323,7 +323,7 @@
                               (return (&type/fold-prod member-types)))
                             (adjust-type value-type))]
           (|case value-type*
-            (&/$ProdT _)
+            (&/$Product _)
             (|let [num-elems (&/|length ?members)
                    [_shorter _tuple-types] (&type/tuple-types-for (&/|length ?members) value-type*)]
               (if (= num-elems _shorter)
@@ -604,7 +604,7 @@
       (&/$Nil)
       (|do [value-type* (resolve-type value-type)]
         (|case value-type*
-          (&/$UnitT)
+          (&/$Unit)
           (return true)
 
           _
@@ -616,7 +616,7 @@
           (|do [=structs (&/map% (check-totality+ check-totality) ?structs)
                 _ (&type/check value-type (|case (->> (&/|map &/|second =structs) (&/|reverse))
                                             (&/$Cons last prevs)
-                                            (&/fold (fn [right left] (&/$ProdT left right))
+                                            (&/fold (fn [right left] (&/$Product left right))
                                                     last prevs)))]
             (return (or ?total
                         (&/fold #(and %1 %2) true (&/|map &/|first =structs)))))
@@ -624,7 +624,7 @@
             (return true)
             (|do [value-type* (resolve-type value-type)]
               (|case value-type*
-                (&/$ProdT _)
+                (&/$Product _)
                 (|let [num-elems (&/|length ?structs)
                        [_shorter _tuple-types] (&type/tuple-types-for (&/|length ?structs) value-type*)
                        _ (&/assert! (= num-elems _shorter)
@@ -640,7 +640,7 @@
       (return true)
       (|do [value-type* (resolve-type value-type)]
         (|case value-type*
-          (&/$SumT _)
+          (&/$Sum _)
           (|do [totals (&/map2% check-totality
                                 (&type/flatten-sum value-type*)
                                 ?structs)]
diff --git a/luxc/src/lux/analyser/lux.clj b/luxc/src/lux/analyser/lux.clj
index 95dc9af59..2a76ec86a 100644
--- a/luxc/src/lux/analyser/lux.clj
+++ b/luxc/src/lux/analyser/lux.clj
@@ -31,7 +31,7 @@
 ;; nested quantifications that cannot be directly counted.
 (defn ^:private next-bound-type [type]
   "(-> Type Type)"
-  (&/$BoundT (->> (count-univq type) (* 2) (+ 1))))
+  (&/$Bound (->> (count-univq type) (* 2) (+ 1))))
 
 (defn ^:private embed-inferred-input [input output]
   "(-> Type Type Type)"
@@ -40,12 +40,12 @@
     (&/$UnivQ env (embed-inferred-input input output*))
 
     _
-    (&/$FunctionT input output)))
+    (&/$Function input output)))
 
 ;; [Exports]
 (defn analyse-unit [analyse ?exo-type]
   (|do [_cursor &/cursor
-        _ (&type/check ?exo-type &/$UnitT)]
+        _ (&type/check ?exo-type &/$Unit)]
     (return (&/|list (&&/|meta ?exo-type _cursor
                                (&&/$tuple (&/|list)))))))
 
@@ -74,7 +74,7 @@
                     [[tuple-type tuple-cursor] tuple-analysis] (&&/cap-1 (analyse-tuple analyse (&/$Left exo-type**) ?elems))
                     =var (&type/resolve-type $var)
                     inferred-type (|case =var
-                                    (&/$VarT iid)
+                                    (&/$Var iid)
                                     (|do [:let [=var* (next-bound-type tuple-type)]
                                           _ (&type/set-var iid =var*)
                                           tuple-type* (&type/clean $var tuple-type)]
@@ -96,7 +96,7 @@
                                ?elems)
                 _ (&type/check exo-type (|case (->> (&/|map &&/expr-type* =elems) (&/|reverse))
                                           (&/$Cons last prevs)
-                                          (&/fold (fn [right left] (&/$ProdT left right))
+                                          (&/fold (fn [right left] (&/$Product left right))
                                                   last prevs)))
                 _cursor &/cursor]
             (return (&/|list (&&/|meta exo-type _cursor
@@ -105,7 +105,7 @@
           (|do [exo-type* (&type/actual-type exo-type)]
             (&/with-attempt
               (|case exo-type*
-                (&/$ProdT _)
+                (&/$Product _)
                 (|let [num-elems (&/|length ?elems)
                        [_shorter _tuple-types] (&type/tuple-types-for num-elems exo-type*)]
                   (if (= num-elems _shorter)
@@ -139,7 +139,7 @@
 
                 (&/$UnivQ _)
                 (|do [$var &type/existential
-                      :let [(&/$ExT $var-id) $var]
+                      :let [(&/$Ex $var-id) $var]
                       exo-type** (&type/apply-type exo-type* $var)
                       [[tuple-type tuple-cursor] tuple-analysis] (&/with-scope-type-var $var-id
                                                                    (&&/cap-1 (analyse-tuple analyse (&/$Right exo-type**) ?elems)))]
@@ -183,7 +183,7 @@
                   [[variant-type variant-cursor] variant-analysis] (&&/cap-1 (analyse-variant analyse (&/$Left exo-type**) idx is-last? ?values))
                   =var (&type/resolve-type $var)
                   inferred-type (|case =var
-                                  (&/$VarT iid)
+                                  (&/$Var iid)
                                   (|do [:let [=var* (next-bound-type variant-type)]
                                         _ (&type/set-var iid =var*)
                                         variant-type* (&type/clean $var variant-type)]
@@ -199,7 +199,7 @@
 
     (&/$Right exo-type)
     (|do [exo-type* (|case exo-type
-                      (&/$VarT ?id)
+                      (&/$Var ?id)
                       (&/try-all% (&/|list (|do [exo-type* (&type/deref ?id)]
                                              (&type/actual-type exo-type*))
                                            (|do [_ (&type/set-var ?id &type/Type)]
@@ -209,7 +209,7 @@
                       (&type/actual-type exo-type))]
       (&/with-attempt
         (|case exo-type*
-          (&/$SumT _)
+          (&/$Sum _)
           (|do [vtype (&type/sum-at idx exo-type*)
                 :let [num-variant-types (&/|length (&type/flatten-sum exo-type*))
                       is-last?* (if (nil? is-last?)
@@ -238,7 +238,7 @@
           (&/fail-with-loc (str "[Analyser Error] Cannot create variant if the expected type is " (&type/show-type exo-type*) " " idx " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))))
         (fn [err]
           (|case exo-type
-            (&/$VarT ?id)
+            (&/$Var ?id)
             (|do [=exo-type (&type/deref ?id)]
               (&/fail-with-loc (str err "\n" "[Analyser Error] Cannot create variant if the expected type is " (&type/show-type =exo-type) " " idx " " (->> ?values (&/|map &/show-ast) (&/|interpose " ") (&/fold str "")))))
 
@@ -249,7 +249,7 @@
 (defn analyse-record [analyse exo-type ?elems]
   (|do [[rec-members rec-type] (&&record/order-record ?elems)]
     (|case exo-type
-      (&/$VarT id)
+      (&/$Var id)
       (|do [? (&type/bound? id)]
         (if ?
           (analyse-tuple analyse (&/$Right exo-type) rec-members)
@@ -324,7 +324,7 @@
                     [=output-t =args] (analyse-apply* analyse exo-type type* ?args)
                     ==args (&/map% (partial &&/clean-analysis $var) =args)]
                 (|case $var
-                  (&/$VarT ?id)
+                  (&/$Var ?id)
                   (|do [? (&type/bound? ?id)
                         type** (if ?
                                  (&type/clean $var =output-t)
@@ -341,7 +341,7 @@
                 type* (&type/apply-type ?fun-type* $var)]
             (analyse-apply* analyse exo-type type* ?args))
 
-          (&/$FunctionT ?input-t ?output-t)
+          (&/$Function ?input-t ?output-t)
           (|do [[=output-t =args] (analyse-apply* analyse exo-type ?output-t ?args*)
                 =arg (&/with-attempt
                        (&&/analyse-1 analyse ?input-t ?arg)
@@ -411,7 +411,7 @@
 
 (defn ^:private unravel-inf-appt [type]
   (|case type
-    (&/$AppT =input+ (&/$VarT _inf-var))
+    (&/$App =input+ (&/$Var _inf-var))
     (&/$Cons _inf-var (unravel-inf-appt =input+))
 
     _
@@ -419,16 +419,16 @@
 
 (defn ^:private clean-func-inference [$input $output =input =func]
   (|case =input
-    (&/$VarT iid)
+    (&/$Var iid)
     (|do [:let [=input* (next-bound-type =func)]
           _ (&type/set-var iid =input*)
           =func* (&type/clean $input =func)
           =func** (&type/clean $output =func*)]
       (return (&/$UnivQ &/$Nil =func**)))
     
-    (&/$AppT =input+ (&/$VarT _inf-var))
+    (&/$App =input+ (&/$Var _inf-var))
     (&/fold% (fn [_func _inf-var]
-               (|do [:let [$inf-var (&/$VarT _inf-var)]
+               (|do [:let [$inf-var (&/$Var _inf-var)]
                      =inf-var (&type/resolve-type $inf-var)
                      _func* (clean-func-inference $inf-var $output =inf-var _func)
                      _ (&type/delete-var _inf-var)]
@@ -436,9 +436,9 @@
              =func
              (unravel-inf-appt =input))
 
-    (&/$ProdT _ _)
+    (&/$Product _ _)
     (&/fold% (fn [_func _inf-var]
-               (|do [:let [$inf-var (&/$VarT _inf-var)]
+               (|do [:let [$inf-var (&/$Var _inf-var)]
                      =inf-var (&type/resolve-type $inf-var)
                      _func* (clean-func-inference $inf-var $output =inf-var _func)
                      _ (&type/delete-var _inf-var)]
@@ -453,7 +453,7 @@
 
 (defn analyse-function* [analyse exo-type ?self ?arg ?body]
   (|case exo-type
-    (&/$VarT id)
+    (&/$Var id)
     (|do [? (&type/bound? id)]
       (if ?
         (|do [exo-type* (&type/deref id)]
@@ -463,7 +463,7 @@
           (fn [$input]
             (&type/with-var
               (fn [$output]
-                (|do [[[function-type function-cursor] function-analysis] (analyse-function* analyse (&/$FunctionT $input $output) ?self ?arg ?body)
+                (|do [[[function-type function-cursor] function-analysis] (analyse-function* analyse (&/$Function $input $output) ?self ?arg ?body)
                       =input (&type/resolve-type $input)
                       =output (&type/resolve-type $output)
                       inferred-type (clean-func-inference $input $output =input (embed-inferred-input =input =output))
@@ -478,7 +478,7 @@
         (|case exo-type*
           (&/$UnivQ _)
           (|do [$var &type/existential
-                :let [(&/$ExT $var-id) $var]
+                :let [(&/$Ex $var-id) $var]
                 exo-type** (&type/apply-type exo-type* $var)]
             (&/with-scope-type-var $var-id
               (analyse-function* analyse exo-type** ?self ?arg ?body)))
@@ -490,7 +490,7 @@
                     =expr (analyse-function* analyse exo-type** ?self ?arg ?body)]
                 (&&/clean-analysis $var =expr))))
           
-          (&/$FunctionT ?arg-t ?return-t)
+          (&/$Function ?arg-t ?return-t)
           (|do [[=scope =captured =body] (&&function/with-function ?self exo-type*
                                            ?arg ?arg-t
                                            (&&/analyse-1 analyse ?return-t ?body))
@@ -509,14 +509,14 @@
   (|case exo-type
     (&/$UnivQ _)
     (|do [$var &type/existential
-          :let [(&/$ExT $var-id) $var]
+          :let [(&/$Ex $var-id) $var]
           exo-type* (&type/apply-type exo-type $var)
           [_ _expr] (&/with-scope-type-var $var-id
                       (analyse-function** analyse exo-type* ?self ?arg ?body))
           _cursor &/cursor]
       (return (&&/|meta exo-type _cursor _expr)))
     
-    (&/$VarT id)
+    (&/$Var id)
     (|do [? (&type/bound? id)]
       (if ?
         (|do [exo-type* (&type/actual-type exo-type)]
@@ -683,8 +683,8 @@
         =value (&&/analyse-1+ analyse ?value)]
     (return (&/|list (coerce ==type =value)))))
 
-(let [input-type (&/$AppT &type/List &type/Text)
-      output-type (&/$AppT &type/IO &/$UnitT)]
+(let [input-type (&/$App &type/List &type/Text)
+      output-type (&/$App &type/IO &/$Unit)]
   (defn analyse-program [analyse optimize compile-program ?args ?body]
     (|do [_ &/ensure-statement
           =body (&/with-scope ""
diff --git a/luxc/src/lux/analyser/proc/common.clj b/luxc/src/lux/analyser/proc/common.clj
index b6727ff53..29797224f 100644
--- a/luxc/src/lux/analyser/proc/common.clj
+++ b/luxc/src/lux/analyser/proc/common.clj
@@ -21,10 +21,10 @@
   (&type/with-var
     (fn [$var]
       (|do [:let [(&/$Cons op (&/$Nil)) ?values]
-            =op (&&/analyse-1 analyse (&/$AppT &type/IO $var) op)
-            _ (&type/check exo-type (&/$SumT &type/Text ;; lux;Left
-                                             $var ;; lux;Right
-                                             ))
+            =op (&&/analyse-1 analyse (&/$App &type/IO $var) op)
+            _ (&type/check exo-type (&/$Sum &type/Text ;; lux;Left
+                                            $var ;; lux;Right
+                                            ))
             _cursor &/cursor]
         (return (&/|list (&&/|meta exo-type _cursor
                                    (&&/$proc (&/T ["lux" "try"]) (&/|list =op) (&/|list)))))))))
@@ -57,8 +57,8 @@
                                            (&/|list =text =part =start)
                                            (&/|list)))))))
 
-  ^:private analyse-text-index      "index"      (&/$AppT &type/Maybe &type/Nat)
-  ^:private analyse-text-last-index "last-index" (&/$AppT &type/Maybe &type/Nat)
+  ^:private analyse-text-index      "index"      (&/$App &type/Maybe &type/Nat)
+  ^:private analyse-text-last-index "last-index" (&/$App &type/Maybe &type/Nat)
   )
 
 (defn ^:private analyse-text-contains? [analyse exo-type ?values]
@@ -77,7 +77,7 @@
         =text (&&/analyse-1 analyse &type/Text text)
         =from (&&/analyse-1 analyse &type/Nat from)
         =to (&&/analyse-1 analyse &type/Nat to)
-        _ (&type/check exo-type (&/$AppT &type/Maybe &type/Text))
+        _ (&type/check exo-type (&/$App &type/Maybe &type/Text))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["text" "clip"])
@@ -131,7 +131,7 @@
   (|do [:let [(&/$Cons text (&/$Cons idx (&/$Nil))) ?values]
         =text (&&/analyse-1 analyse &type/Text text)
         =idx (&&/analyse-1 analyse &type/Nat idx)
-        _ (&type/check exo-type (&/$AppT &type/Maybe &type/Char))
+        _ (&type/check exo-type (&/$App &type/Maybe &type/Char))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["text" "char"])
@@ -245,7 +245,7 @@
           (return (&/|list (&&/|meta exo-type _cursor
                                      (&&/$proc (&/T <encode-op>) (&/|list =x) (&/|list)))))))
 
-    (let [decode-type (&/$AppT &type/Maybe <type>)]
+    (let [decode-type (&/$App &type/Maybe <type>)]
       (defn <decode> [analyse exo-type ?values]
         (|do [:let [(&/$Cons x (&/$Nil)) ?values]
               =x (&&/analyse-1 analyse &type/Text x)
@@ -306,7 +306,7 @@
   ^:private analyse-deg-to-real  &type/Deg  &type/Real   ["deg" "to-real"]
   ^:private analyse-real-to-deg  &type/Real &type/Deg    ["real" "to-deg"]
   
-  ^:private analyse-io-log       &type/Text &/$UnitT     ["io" "log"]
+  ^:private analyse-io-log       &type/Text &/$Unit     ["io" "log"]
   ^:private analyse-io-error     &type/Text &type/Bottom ["io" "error"]
   ^:private analyse-io-exit      &type/Int  &type/Bottom ["io" "exit"]
   )
@@ -321,7 +321,7 @@
 (defn ^:private analyse-array-new [analyse exo-type ?values]
   (|do [:let [(&/$Cons length (&/$Nil)) ?values]
         =length (&&/analyse-1 analyse &type/Nat length)
-        _ (&type/check exo-type (&/$UnivQ (&/|list) (&type/Array (&/$BoundT 1))))
+        _ (&type/check exo-type (&/$UnivQ (&/|list) (&type/Array (&/$Bound 1))))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["array" "new"]) (&/|list =length) (&/|list)))))))
@@ -332,7 +332,7 @@
       (|do [:let [(&/$Cons array (&/$Cons idx (&/$Nil))) ?values]
             =array (&&/analyse-1 analyse (&type/Array $var) array)
             =idx (&&/analyse-1 analyse &type/Nat idx)
-            _ (&type/check exo-type (&/$AppT &type/Maybe $var))
+            _ (&type/check exo-type (&/$App &type/Maybe $var))
             _cursor &/cursor]
         (return (&/|list (&&/|meta exo-type _cursor
                                    (&&/$proc (&/T ["array" "get"]) (&/|list =array =idx) (&/|list)))))))))
@@ -466,8 +466,8 @@
 
 (defn ^:private analyse-process-future [analyse exo-type ?values]
   (|do [:let [(&/$Cons ?procedure (&/$Nil)) ?values]
-        =procedure (&&/analyse-1 analyse (&/$AppT &type/IO &type/Top) ?procedure)
-        _ (&type/check exo-type &/$UnitT)
+        =procedure (&&/analyse-1 analyse (&/$App &type/IO &type/Top) ?procedure)
+        _ (&type/check exo-type &/$Unit)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["process" "future"]) (&/|list =procedure) (&/|list)))))))
@@ -475,8 +475,8 @@
 (defn ^:private analyse-process-schedule [analyse exo-type ?values]
   (|do [:let [(&/$Cons ?milliseconds (&/$Cons ?procedure (&/$Nil))) ?values]
         =milliseconds (&&/analyse-1 analyse &type/Nat ?milliseconds)
-        =procedure (&&/analyse-1 analyse (&/$AppT &type/IO &type/Top) ?procedure)
-        _ (&type/check exo-type &/$UnitT)
+        =procedure (&&/analyse-1 analyse (&/$App &type/IO &type/Top) ?procedure)
+        _ (&type/check exo-type &/$Unit)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["process" "schedule"]) (&/|list =milliseconds =procedure) (&/|list)))))))
diff --git a/luxc/src/lux/analyser/proc/js.clj b/luxc/src/lux/analyser/proc/js.clj
index 986720108..33fa7816d 100644
--- a/luxc/src/lux/analyser/proc/js.clj
+++ b/luxc/src/lux/analyser/proc/js.clj
@@ -10,9 +10,9 @@
 (do-template [<name> <proc>]
   (defn <name> [analyse exo-type ?values]
     (|do [:let [(&/$Cons ?function ?args) ?values]
-          =function (&&/analyse-1 analyse (&/$HostT "function" &/$Nil) ?function)
+          =function (&&/analyse-1 analyse (&/$Host "function" &/$Nil) ?function)
           =args (&/map% (partial &&/analyse-1+ analyse) ?args)
-          _ (&type/check exo-type (&/$HostT "object" &/$Nil))
+          _ (&type/check exo-type (&/$Host "object" &/$Nil))
           _cursor &/cursor]
       (return (&/|list (&&/|meta exo-type _cursor
                                  (&&/$proc (&/T ["js" <proc>]) (&/$Cons =function =args) (&/|list)))))))
@@ -23,17 +23,17 @@
 
 (defn ^:private analyse-js-object-call [analyse exo-type ?values]
   (|do [:let [(&/$Cons ?object (&/$Cons ?field ?args)) ?values]
-        =object (&&/analyse-1 analyse (&/$HostT "object" &/$Nil) ?object)
+        =object (&&/analyse-1 analyse (&/$Host "object" &/$Nil) ?object)
         =field (&&/analyse-1 analyse &type/Text ?field)
         =args (&/map% (partial &&/analyse-1+ analyse) ?args)
-        _ (&type/check exo-type (&/$HostT "object" &/$Nil))
+        _ (&type/check exo-type (&/$Host "object" &/$Nil))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["js" "object-call"]) (&/$Cons =object (&/$Cons =field =args)) (&/|list)))))))
 
 (defn ^:private analyse-js-ref [analyse exo-type ?values]
   (|do [:let [(&/$Cons [_ (&/$Text ?ref-name)] (&/$Nil)) ?values]
-        _ (&type/check exo-type (&/$HostT "object" &/$Nil))
+        _ (&type/check exo-type (&/$Host "object" &/$Nil))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["js" "ref"]) (&/|list) (&/|list ?ref-name)))))))
@@ -41,9 +41,9 @@
 (do-template [<name> <proc>]
   (defn <name> [analyse exo-type ?values]
     (|do [:let [(&/$Cons ?object (&/$Cons ?field (&/$Nil))) ?values]
-          =object (&&/analyse-1 analyse (&/$HostT "object" &/$Nil) ?object)
+          =object (&&/analyse-1 analyse (&/$Host "object" &/$Nil) ?object)
           =field (&&/analyse-1 analyse &type/Text ?field)
-          _ (&type/check exo-type (&/$HostT "object" &/$Nil))
+          _ (&type/check exo-type (&/$Host "object" &/$Nil))
           _cursor &/cursor]
       (return (&/|list (&&/|meta exo-type _cursor
                                  (&&/$proc (&/T ["js" <proc>]) (&/|list =object =field) (&/|list)))))))
@@ -54,10 +54,10 @@
 
 (defn ^:private analyse-js-set-field [analyse exo-type ?values]
   (|do [:let [(&/$Cons ?object (&/$Cons ?field (&/$Cons ?value (&/$Nil)))) ?values]
-        =object (&&/analyse-1 analyse (&/$HostT "object" &/$Nil) ?object)
+        =object (&&/analyse-1 analyse (&/$Host "object" &/$Nil) ?object)
         =field (&&/analyse-1 analyse &type/Text ?field)
         =value (&&/analyse-1+ analyse ?value)
-        _ (&type/check exo-type (&/$HostT "object" &/$Nil))
+        _ (&type/check exo-type (&/$Host "object" &/$Nil))
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["js" "set-field"]) (&/|list =object =field =value) (&/|list)))))))
@@ -65,7 +65,7 @@
 (do-template [<name> <proc> <type>]
   (defn <name> [analyse exo-type ?values]
     (|do [:let [(&/$Nil) ?values]
-          :let [output-type (&/$HostT <type> &/$Nil)]
+          :let [output-type (&/$Host <type> &/$Nil)]
           _ (&type/check exo-type output-type)
           _cursor &/cursor]
       (return (&/|list (&&/|meta exo-type _cursor
diff --git a/luxc/src/lux/analyser/proc/jvm.clj b/luxc/src/lux/analyser/proc/jvm.clj
index ba9be52b1..977c07787 100644
--- a/luxc/src/lux/analyser/proc/jvm.clj
+++ b/luxc/src/lux/analyser/proc/jvm.clj
@@ -21,16 +21,16 @@
 (defn ^:private ensure-object [type]
   "(-> Type (Lux (, Text (List Type))))"
   (|case type
-    (&/$HostT payload)
+    (&/$Host payload)
     (return payload)
 
-    (&/$VarT id)
+    (&/$Var id)
     (return (&/T ["java.lang.Object" (&/|list)]))
 
-    (&/$ExT id)
+    (&/$Ex id)
     (return (&/T ["java.lang.Object" (&/|list)]))
 
-    (&/$NamedT _ type*)
+    (&/$Named _ type*)
     (ensure-object type*)
 
     (&/$UnivQ _ type*)
@@ -39,7 +39,7 @@
     (&/$ExQ _ type*)
     (ensure-object type*)
 
-    (&/$AppT F A)
+    (&/$App F A)
     (|do [type* (&type/apply-type F A)]
       (ensure-object type*))
 
@@ -49,8 +49,8 @@
 (defn ^:private as-object [type]
   "(-> Type Type)"
   (|case type
-    (&/$HostT class params)
-    (&/$HostT (&host-type/as-obj class) params)
+    (&/$Host class params)
+    (&/$Host (&host-type/as-obj class) params)
 
     _
     type))
@@ -72,19 +72,19 @@
 (defn ^:private as-otype+ [type]
   "(-> Type Type)"
   (|case type
-    (&/$HostT name params)
-    (&/$HostT (as-otype name) params)
+    (&/$Host name params)
+    (&/$Host (as-otype name) params)
 
     _
     type))
 
 (defn ^:private clean-gtype-var [idx gtype-var]
-  (|let [(&/$VarT id) gtype-var]
+  (|let [(&/$Var id) gtype-var]
     (|do [? (&type/bound? id)]
       (if ?
         (|do [real-type (&type/deref id)]
           (return (&/T [idx real-type])))
-        (return (&/T [(+ 2 idx) (&/$BoundT idx)]))))))
+        (return (&/T [(+ 2 idx) (&/$Bound idx)]))))))
 
 (defn ^:private clean-gtype-vars [gtype-vars]
   (|do [[_ clean-types] (&/fold% (fn [idx+types gtype-var]
@@ -99,19 +99,19 @@
   "(-> Text (List Type) Type)"
   (&/fold (fn [base-type type-arg]
             (|case type-arg
-              (&/$BoundT _)
+              (&/$Bound _)
               (&/$UnivQ &type/empty-env base-type)
               
               _
               base-type))
-          (&/$HostT class-name type-args)
+          (&/$Host class-name type-args)
           type-args))
 
 ;; [Resources]
 (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
-    (&/$HostT class targs)
+    (&/$Host class targs)
     (if (= (&/|length targs) (&/|length gvars))
       (|let [gtype-env (&/fold2 (fn [m ^TypeVariable g t] (&/$Cons (&/T [(.getName g) t]) m))
                                 (&/|table)
@@ -186,25 +186,25 @@
     
     (&/$GenericClass name params)
     (case name
-      "boolean" (return (&/$HostT "java.lang.Boolean" &/$Nil))
-      "byte"    (return (&/$HostT "java.lang.Byte" &/$Nil))
-      "short"   (return (&/$HostT "java.lang.Short" &/$Nil))
-      "int"     (return (&/$HostT "java.lang.Integer" &/$Nil))
-      "long"    (return (&/$HostT "java.lang.Long" &/$Nil))
-      "float"   (return (&/$HostT "java.lang.Float" &/$Nil))
-      "double"  (return (&/$HostT "java.lang.Double" &/$Nil))
-      "char"    (return (&/$HostT "java.lang.Character" &/$Nil))
-      "void"    (return &/$UnitT)
+      "boolean" (return (&/$Host "java.lang.Boolean" &/$Nil))
+      "byte"    (return (&/$Host "java.lang.Byte" &/$Nil))
+      "short"   (return (&/$Host "java.lang.Short" &/$Nil))
+      "int"     (return (&/$Host "java.lang.Integer" &/$Nil))
+      "long"    (return (&/$Host "java.lang.Long" &/$Nil))
+      "float"   (return (&/$Host "java.lang.Float" &/$Nil))
+      "double"  (return (&/$Host "java.lang.Double" &/$Nil))
+      "char"    (return (&/$Host "java.lang.Character" &/$Nil))
+      "void"    (return &/$Unit)
       ;; else
       (|do [=params (&/map% (partial generic-class->type env) params)]
-        (return (&/$HostT name =params))))
+        (return (&/$Host name =params))))
 
     (&/$GenericArray param)
     (|do [=param (generic-class->type env param)]
-      (return (&/$HostT &host-type/array-data-tag (&/|list =param))))
+      (return (&/$Host &host-type/array-data-tag (&/|list =param))))
 
     (&/$GenericWildcard _)
-    (return (&/$ExQ &/$Nil (&/$BoundT 1)))
+    (return (&/$ExQ &/$Nil (&/$Bound 1)))
     ))
 
 (defn gen-super-env [class-env supers class-decl]
@@ -252,7 +252,7 @@
           itype (generic-class->type full-env itype*)]
       (if (double-register-gclass? itype*)
         (&&env/with-local iname itype
-          (&&env/with-local "" &/$VoidT
+          (&&env/with-local "" &/$Void
             body*))
         (&&env/with-local iname itype
           body*)))))
@@ -260,12 +260,12 @@
 (defn ^:private analyse-method [analyse class-decl class-env all-supers method]
   "(-> Analyser ClassDecl (List (, TypeVar Type)) (List SuperClassDecl) MethodSyntax (Lux MethodAnalysis))"
   (|let [[?cname ?cparams] class-decl
-         class-type (&/$HostT ?cname (&/|map &/|second class-env))]
+         class-type (&/$Host ?cname (&/|map &/|second class-env))]
     (|case method
       (&/$ConstructorMethodSyntax =privacy-modifier ?strict ?anns ?gvars ?exceptions ?inputs ?ctor-args ?body)
       (|do [method-env (make-type-env ?gvars)
             :let [full-env (&/|++ class-env method-env)]
-            :let [output-type &/$UnitT]
+            :let [output-type &/$Unit]
             =ctor-args (&/map% (fn [ctor-arg]
                                  (|do [:let [[ca-type ca-term] ctor-arg]
                                        =ca-type (generic-class->type full-env ca-type)
@@ -383,10 +383,10 @@
     ))
 
 (do-template [<name> <proc> <from-class> <to-class>]
-  (let [output-type (&/$HostT <to-class> &/$Nil)]
+  (let [output-type (&/$Host <to-class> &/$Nil)]
     (defn <name> [analyse exo-type _?value]
       (|do [:let [(&/$Cons ?value (&/$Nil)) _?value]
-            =value (&&/analyse-1 analyse (&/$HostT <from-class> &/$Nil) ?value)
+            =value (&&/analyse-1 analyse (&/$Host <from-class> &/$Nil) ?value)
             _ (&type/check exo-type output-type)
             _cursor &/cursor]
         (return (&/|list (&&/|meta output-type _cursor (&&/$proc (&/T ["jvm" <proc>]) (&/|list =value) (&/|list))))))))
@@ -423,11 +423,11 @@
   )
 
 (do-template [<name> <proc> <v1-class> <v2-class> <to-class>]
-  (let [output-type (&/$HostT <to-class> &/$Nil)]
+  (let [output-type (&/$Host <to-class> &/$Nil)]
     (defn <name> [analyse exo-type ?values]
       (|do [:let [(&/$Cons ?value1 (&/$Cons ?value2 (&/$Nil))) ?values]
-            =value1 (&&/analyse-1 analyse (&/$HostT <v1-class> &/$Nil) ?value1)
-            =value2 (&&/analyse-1 analyse (&/$HostT <v2-class> &/$Nil) ?value2)
+            =value1 (&&/analyse-1 analyse (&/$Host <v1-class> &/$Nil) ?value1)
+            =value2 (&&/analyse-1 analyse (&/$Host <v2-class> &/$Nil) ?value2)
             _ (&type/check exo-type output-type)
             _cursor &/cursor]
         (return (&/|list (&&/|meta output-type _cursor (&&/$proc (&/T ["jvm" <proc>]) (&/|list =value1 =value2) (&/|list))))))))
@@ -448,8 +448,8 @@
   )
 
 (do-template [<name> <proc> <input-class> <output-class>]
-  (let [input-type (&/$HostT <input-class> &/$Nil)
-        output-type (&/$HostT <output-class> &/$Nil)]
+  (let [input-type (&/$Host <input-class> &/$Nil)
+        output-type (&/$Host <output-class> &/$Nil)]
     (defn <name> [analyse exo-type ?values]
       (|do [:let [(&/$Cons x (&/$Cons y (&/$Nil))) ?values]
             =x (&&/analyse-1 analyse input-type x)
@@ -503,8 +503,8 @@
 (let [length-type &type/Nat
       idx-type &type/Nat]
   (do-template [<elem-class> <array-class> <new-name> <new-tag> <load-name> <load-tag> <store-name> <store-tag>]
-    (let [elem-type (&/$HostT <elem-class> &/$Nil)
-          array-type (&/$HostT <array-class> &/$Nil)]
+    (let [elem-type (&/$Host <elem-class> &/$Nil)
+          array-type (&/$Host <array-class> &/$Nil)]
       (defn <new-name> [analyse exo-type ?values]
         (|do [:let [(&/$Cons length (&/$Nil)) ?values]
               =length (&&/analyse-1 analyse length-type length)
@@ -558,7 +558,7 @@
                    &&a-parser/parse-gclass)
           gtype-env &/get-type-env
           =gclass (&host-type/instance-gtype &type/existential gtype-env gclass)
-          :let [array-type (&/$HostT &host-type/array-data-tag (&/|list =gclass))]
+          :let [array-type (&/$Host &host-type/array-data-tag (&/|list =gclass))]
           =length (&&/analyse-1 analyse length-type length)
           _ (&type/check exo-type array-type)
           _cursor &/cursor]
@@ -614,7 +614,7 @@
 
 (defn ^:private analyse-jvm-null [analyse exo-type ?values]
   (|do [:let [(&/$Nil) ?values]
-        :let [output-type (&/$HostT &host-type/null-data-tag &/$Nil)]
+        :let [output-type (&/$Host &host-type/null-data-tag &/$Nil)]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
@@ -632,7 +632,7 @@
 (defn ^:private analyse-jvm-throw [analyse exo-type ?values]
   (|do [:let [(&/$Cons ?ex (&/$Nil)) ?values]
         =ex (&&/analyse-1+ analyse ?ex)
-        _ (&type/check (&/$HostT "java.lang.Throwable" &/$Nil) (&&/expr-type* =ex))
+        _ (&type/check (&/$Host "java.lang.Throwable" &/$Nil) (&&/expr-type* =ex))
         [throw-class throw-params] (ensure-object (&&/expr-type* =ex))
         _cursor &/cursor
         _ (&type/check exo-type &type/Bottom)]
@@ -673,7 +673,7 @@
         :let [gclass (&host-type/gtype->gclass gtype)]
         =type (&host-type/instance-param &type/existential &/$Nil gtype)
         =value (&&/analyse-1 analyse =type value)
-        :let [output-type &/$UnitT]
+        :let [output-type &/$Unit]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
@@ -690,7 +690,7 @@
         :let [gclass (&host-type/gtype->gclass gtype)]
         =type (analyse-field-access-helper obj-type gvars gtype)
         =value (&&/analyse-1 analyse =type value)
-        :let [output-type &/$UnitT]
+        :let [output-type &/$Unit]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
@@ -709,7 +709,7 @@
     (&/$Cons ^TypeVariable gtv gtype-vars*)
     (&type/with-var
       (fn [$var]
-        (|do [:let [(&/$VarT _id) $var
+        (|do [:let [(&/$Var _id) $var
                     gtype-env* (&/$Cons (&/T [(.getName gtv) $var]) gtype-env)]
               [=gret =args] (analyse-method-call-helper analyse exo-type gret gtype-env* gtype-vars* gtype-args args)
               ==gret (&type/clean $var =gret)
@@ -717,7 +717,7 @@
           (return (&/T [==gret ==args])))))
     ))
 
-(let [dummy-type-param (&/$HostT "java.lang.Object" &/$Nil)]
+(let [dummy-type-param (&/$Host "java.lang.Object" &/$Nil)]
   (do-template [<name> <tag> <only-interface?>]
     (defn <name> [analyse exo-type class method classes ?values]
       (|do [!class! (&/de-alias-class class)
@@ -735,10 +735,10 @@
                                                          (&host/lookup-virtual-method class-loader !class! method classes))
             =object (&&/analyse-1+ analyse object)
             [sub-class sub-params] (ensure-object (&&/expr-type* =object))
-            (&/$HostT super-class* super-params*) (&host-type/->super-type &type/existential class-loader !class! (if (= sub-class class)
-                                                                                                                    !class!
-                                                                                                                    sub-class)
-                                                                           sub-params)
+            (&/$Host super-class* super-params*) (&host-type/->super-type &type/existential class-loader !class! (if (= sub-class class)
+                                                                                                                   !class!
+                                                                                                                   sub-class)
+                                                                          sub-params)
             :let [gtype-env (&/fold2 (fn [m ^TypeVariable g t] (&/$Cons (&/T [(.getName g) t]) m))
                                      (&/|table)
                                      parent-gvars
@@ -811,7 +811,7 @@
                  (return nil))
             (catch Exception e
               (&/fail-with-loc (str "[Analyser Error] Unknown class: " _class-name))))
-        :let [output-type (&/$HostT "java.lang.Class" (&/|list (&/$HostT _class-name (&/|list))))]
+        :let [output-type (&/$Host "java.lang.Class" (&/|list (&/$Host _class-name (&/|list))))]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
     (return (&/|list (&&/|meta output-type _cursor
@@ -822,7 +822,7 @@
         _ (compile-interface interface-decl supers =anns =methods)
         :let [_ (println 'INTERFACE (str module "." (&/|first interface-decl)))]
         _cursor &/cursor]
-    (return (&/|list (&&/|meta &/$UnitT _cursor
+    (return (&/|list (&&/|meta &/$Unit _cursor
                                (&&/$tuple (&/|list)))))))
 
 (defn ^:private analyse-jvm-class [analyse compile-class class-decl super-class interfaces =inheritance-modifier =anns ?fields methods]
@@ -841,7 +841,7 @@
           _ &/pop-dummy-name
           :let [_ (println 'CLASS full-name)]
           _cursor &/cursor]
-      (return (&/|list (&&/|meta &/$UnitT _cursor
+      (return (&/|list (&&/|meta &/$Unit _cursor
                                  (&&/$tuple (&/|list))))))))
 
 (defn ^:private captured-source [env-entry]
@@ -866,7 +866,7 @@
             :let [name (->> scope &/|reverse &/|tail &host/location)
                   class-decl (&/T [name &/$Nil])
                   anon-class (str (string/replace module "/" ".") "." name)
-                  anon-class-type (&/$HostT anon-class &/$Nil)]
+                  anon-class-type (&/$Host anon-class &/$Nil)]
             =ctor-args (&/map% (fn [ctor-arg]
                                  (|let [[arg-type arg-term] ctor-arg]
                                    (|do [=arg-term (&&/analyse-1+ analyse arg-term)]
diff --git a/luxc/src/lux/analyser/record.clj b/luxc/src/lux/analyser/record.clj
index 90be7d330..ac9a0e64d 100644
--- a/luxc/src/lux/analyser/record.clj
+++ b/luxc/src/lux/analyser/record.clj
@@ -11,7 +11,7 @@
   "(-> (List (, Syntax Syntax)) (Lux (List Syntax)))"
   (|do [[tag-group tag-type] (|case pairs
                                (&/$Nil)
-                               (return (&/T [&/$Nil &/$UnitT]))
+                               (return (&/T [&/$Nil &/$Unit]))
                                
                                (&/$Cons [[_ (&/$Tag tag1)] _] _)
                                (|do [[module name] (&&/resolved-ident tag1)
diff --git a/luxc/src/lux/base.clj b/luxc/src/lux/base.clj
index 98b6ce4e8..6ce50c06f 100644
--- a/luxc/src/lux/base.clj
+++ b/luxc/src/lux/base.clj
@@ -86,19 +86,19 @@
 
 ;; Type
 (defvariant
-  ("HostT" 2)
-  ("VoidT" 0)
-  ("UnitT" 0)
-  ("SumT" 2)
-  ("ProdT" 2)
-  ("FunctionT" 2)
-  ("BoundT" 1)
-  ("VarT" 1)
-  ("ExT" 1)
+  ("Host" 2)
+  ("Void" 0)
+  ("Unit" 0)
+  ("Sum" 2)
+  ("Product" 2)
+  ("Function" 2)
+  ("Bound" 1)
+  ("Var" 1)
+  ("Ex" 1)
   ("UnivQ" 2)
   ("ExQ" 2)
-  ("AppT" 2)
-  ("NamedT" 2))
+  ("App" 2)
+  ("Named" 2))
 
 ;; Vars
 (defvariant
diff --git a/luxc/src/lux/compiler/cache/type.clj b/luxc/src/lux/compiler/cache/type.clj
index 5715866f7..f6f06f03c 100644
--- a/luxc/src/lux/compiler/cache/type.clj
+++ b/luxc/src/lux/compiler/cache/type.clj
@@ -24,22 +24,22 @@
   (if (clojure.lang.Util/identical &type/Type type)
     "T"
     (|case type
-      (&/$HostT name params)
+      (&/$Host name params)
       (str "^" name stop (serialize-list serialize-type params))
 
-      (&/$VoidT)
+      (&/$Void)
       "0"
 
-      (&/$UnitT)
+      (&/$Unit)
       "1"
       
-      (&/$ProdT left right)
+      (&/$Product left right)
       (str "*" (serialize-type left) (serialize-type right))
 
-      (&/$SumT left right)
+      (&/$Sum left right)
       (str "+" (serialize-type left) (serialize-type right))
 
-      (&/$FunctionT left right)
+      (&/$Function left right)
       (str ">" (serialize-type left) (serialize-type right))
 
       (&/$UnivQ env body)
@@ -48,19 +48,19 @@
       (&/$ExQ env body)
       (str "E" (serialize-list serialize-type env) (serialize-type body))
 
-      (&/$BoundT idx)
+      (&/$Bound idx)
       (str "$" idx stop)
 
-      (&/$ExT idx)
+      (&/$Ex idx)
       (str "!" idx stop)
 
-      (&/$VarT idx)
+      (&/$Var idx)
       (str "?" idx stop)
 
-      (&/$AppT left right)
+      (&/$App left right)
       (str "%" (serialize-type left) (serialize-type right))
 
-      (&/$NamedT [module name] type*)
+      (&/$Named [module name] type*)
       (str "@" module ident-separator name stop (serialize-type type*))
 
       _
@@ -85,8 +85,8 @@
       [<type> (.substring input 1)]
       ))
 
-  ^:private deserialize-void  "0" &/$VoidT
-  ^:private deserialize-unit  "1" &/$UnitT
+  ^:private deserialize-void  "0" &/$Void
+  ^:private deserialize-unit  "1" &/$Unit
   ^:private deserialize-type* "T" &type/Type
   )
 
@@ -98,10 +98,10 @@
           [(<type> left right) input*]))
       ))
 
-  ^:private deserialize-sum  "+" &/$SumT
-  ^:private deserialize-prod "*" &/$ProdT
-  ^:private deserialize-lambda    ">" &/$FunctionT
-  ^:private deserialize-app  "%" &/$AppT
+  ^:private deserialize-sum  "+" &/$Sum
+  ^:private deserialize-prod "*" &/$Product
+  ^:private deserialize-lambda    ">" &/$Function
+  ^:private deserialize-app  "%" &/$App
   )
 
 (do-template [<name> <signal> <type>]
@@ -110,9 +110,9 @@
       (let [[idx ^String input*] (.split (.substring input 1) stop 2)]
         [(<type> (Long/parseLong idx)) input*])))
 
-  ^:private deserialize-bound "$" &/$BoundT
-  ^:private deserialize-ex    "!" &/$ExT
-  ^:private deserialize-var   "?" &/$VarT
+  ^:private deserialize-bound "$" &/$Bound
+  ^:private deserialize-ex    "!" &/$Ex
+  ^:private deserialize-var   "?" &/$Var
   )
 
 (defn ^:private deserialize-named [^String input]
@@ -120,7 +120,7 @@
     (let [[^String module+name ^String input*] (.split (.substring input 1) stop 2)
           [module name] (.split module+name ident-separator 2)]
       (when-let [[type* ^String input*] (deserialize-type input*)]
-        [(&/$NamedT (&/T [module name]) type*) input*]))))
+        [(&/$Named (&/T [module name]) type*) input*]))))
 
 (do-template [<name> <signal> <type>]
   (defn <name> [^String input]
@@ -137,7 +137,7 @@
   (when (.startsWith input "^")
     (let [[name ^String input*] (.split (.substring input 1) stop 2)]
       (when-let [[params ^String input*] (deserialize-list input*)]
-        [(&/$HostT name params) input*]))))
+        [(&/$Host name params) input*]))))
 
 (defn deserialize-type
   "(-> Text Type)"
diff --git a/luxc/src/lux/compiler/jvm/proc/host.clj b/luxc/src/lux/compiler/jvm/proc/host.clj
index 2c5bbc6cd..94b7ca0d8 100644
--- a/luxc/src/lux/compiler/jvm/proc/host.clj
+++ b/luxc/src/lux/compiler/jvm/proc/host.clj
@@ -48,40 +48,40 @@
       char-class "java.lang.Character"]
   (defn prepare-return! [^MethodVisitor *writer* *type*]
     (|case *type*
-      (&/$UnitT)
+      (&/$Unit)
       (.visitLdcInsn *writer* &/unit-tag)
 
-      (&/$HostT "boolean" (&/$Nil))
+      (&/$Host "boolean" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name boolean-class) "valueOf" (str "(Z)" (&host-generics/->type-signature boolean-class)))
       
-      (&/$HostT "byte" (&/$Nil))
+      (&/$Host "byte" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name byte-class) "valueOf" (str "(B)" (&host-generics/->type-signature byte-class)))
 
-      (&/$HostT "short" (&/$Nil))
+      (&/$Host "short" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name short-class) "valueOf" (str "(S)" (&host-generics/->type-signature short-class)))
 
-      (&/$HostT "int" (&/$Nil))
+      (&/$Host "int" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name int-class) "valueOf" (str "(I)" (&host-generics/->type-signature int-class)))
 
-      (&/$HostT "long" (&/$Nil))
+      (&/$Host "long" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name long-class) "valueOf" (str "(J)" (&host-generics/->type-signature long-class)))
 
-      (&/$HostT "float" (&/$Nil))
+      (&/$Host "float" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name float-class) "valueOf" (str "(F)" (&host-generics/->type-signature float-class)))
 
-      (&/$HostT "double" (&/$Nil))
+      (&/$Host "double" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name double-class) "valueOf" (str "(D)" (&host-generics/->type-signature double-class)))
 
-      (&/$HostT "char" (&/$Nil))
+      (&/$Host "char" (&/$Nil))
       (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name char-class) "valueOf" (str "(C)" (&host-generics/->type-signature char-class)))
       
-      (&/$HostT _ _)
+      (&/$Host _ _)
       nil
 
-      (&/$NamedT ?name ?type)
+      (&/$Named ?name ?type)
       (prepare-return! *writer* ?type)
 
-      (&/$ExT _)
+      (&/$Ex _)
       nil
 
       _
diff --git a/luxc/src/lux/host.clj b/luxc/src/lux/host.clj
index e222baf10..f602376fb 100644
--- a/luxc/src/lux/host.clj
+++ b/luxc/src/lux/host.clj
@@ -30,7 +30,7 @@
 (defn unfold-array [type]
   "(-> Type (, Int Type))"
   (|case type
-    (&/$HostT "#Array" (&/$Cons param (&/$Nil)))
+    (&/$Host "#Array" (&/$Cons param (&/$Nil)))
     (|let [[count inner] (unfold-array param)]
       (&/T [(inc count) inner]))
 
@@ -42,10 +42,10 @@
   (defn ->java-sig [^objects type]
     "(-> Type (Lux Text))"
     (|case type
-      (&/$HostT ?name params)
+      (&/$Host ?name params)
       (cond (= &host-type/array-data-tag ?name) (|do [:let [[level base] (unfold-array type)]
                                                       base-sig (|case base
-                                                                 (&/$HostT base-class _)
+                                                                 (&/$Host base-class _)
                                                                  (return (&host-generics/->type-signature base-class))
 
                                                                  _
@@ -55,26 +55,26 @@
             (= &host-type/null-data-tag ?name)  (return (&host-generics/->type-signature "java.lang.Object"))
             :else                               (return (&host-generics/->type-signature ?name)))
 
-      (&/$FunctionT _ _)
+      (&/$Function _ _)
       (return (&host-generics/->type-signature function-class))
 
-      (&/$UnitT)
+      (&/$Unit)
       (return "V")
 
-      (&/$SumT _)
+      (&/$Sum _)
       (return object-array)
 
-      (&/$ProdT _)
+      (&/$Product _)
       (return object-array)
 
-      (&/$NamedT ?name ?type)
+      (&/$Named ?name ?type)
       (->java-sig ?type)
 
-      (&/$AppT ?F ?A)
+      (&/$App ?F ?A)
       (|do [type* (&type/apply-type ?F ?A)]
         (->java-sig type*))
 
-      (&/$ExT _)
+      (&/$Ex _)
       (return ex-type-class)
 
       _
diff --git a/luxc/src/lux/type.clj b/luxc/src/lux/type.clj
index f69542442..85ce1613b 100644
--- a/luxc/src/lux/type.clj
+++ b/luxc/src/lux/type.clj
@@ -23,145 +23,145 @@
 
 (def empty-env &/$Nil)
 
-(def Bool (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "#Bool" &/$Nil)))
-(def Nat (&/$NamedT (&/T ["lux" "Nat"]) (&/$HostT &&host/nat-data-tag &/$Nil)))
-(def Deg (&/$NamedT (&/T ["lux" "Deg"]) (&/$HostT &&host/deg-data-tag &/$Nil)))
-(def Int (&/$NamedT (&/T ["lux" "Int"]) (&/$HostT "#Int" &/$Nil)))
-(def Real (&/$NamedT (&/T ["lux" "Real"]) (&/$HostT "#Real" &/$Nil)))
-(def Char (&/$NamedT (&/T ["lux" "Char"]) (&/$HostT "#Char" &/$Nil)))
-(def Text (&/$NamedT (&/T ["lux" "Text"]) (&/$HostT "#Text" &/$Nil)))
-(def Ident (&/$NamedT (&/T ["lux" "Ident"]) (&/$ProdT Text Text)))
+(def Bool (&/$Named (&/T ["lux" "Bool"]) (&/$Host "#Bool" &/$Nil)))
+(def Nat (&/$Named (&/T ["lux" "Nat"]) (&/$Host &&host/nat-data-tag &/$Nil)))
+(def Deg (&/$Named (&/T ["lux" "Deg"]) (&/$Host &&host/deg-data-tag &/$Nil)))
+(def Int (&/$Named (&/T ["lux" "Int"]) (&/$Host "#Int" &/$Nil)))
+(def Real (&/$Named (&/T ["lux" "Real"]) (&/$Host "#Real" &/$Nil)))
+(def Char (&/$Named (&/T ["lux" "Char"]) (&/$Host "#Char" &/$Nil)))
+(def Text (&/$Named (&/T ["lux" "Text"]) (&/$Host "#Text" &/$Nil)))
+(def Ident (&/$Named (&/T ["lux" "Ident"]) (&/$Product Text Text)))
 
 (do-template [<name> <tag>]
   (defn <name> [elem-type]
-    (&/$HostT <tag> (&/|list elem-type)))
+    (&/$Host <tag> (&/|list elem-type)))
 
   Array "#Array"
   Atom  "#Atom"
   )
 
 (def Bottom
-  (&/$NamedT (&/T ["lux" "Bottom"])
-             (&/$UnivQ empty-env
-                       (&/$BoundT 1))))
+  (&/$Named (&/T ["lux" "Bottom"])
+            (&/$UnivQ empty-env
+                      (&/$Bound 1))))
 
 (def Top
-  (&/$NamedT (&/T ["lux" "Top"])
-             (&/$ExQ empty-env
-                     (&/$BoundT 1))))
+  (&/$Named (&/T ["lux" "Top"])
+            (&/$ExQ empty-env
+                    (&/$Bound 1))))
 
 (def IO
-  (&/$NamedT (&/T ["lux/codata" "IO"])
-             (&/$UnivQ empty-env
-                       (&/$FunctionT &/$VoidT (&/$BoundT 1)))))
+  (&/$Named (&/T ["lux/codata" "IO"])
+            (&/$UnivQ empty-env
+                      (&/$Function &/$Void (&/$Bound 1)))))
 
 (def List
-  (&/$NamedT (&/T ["lux" "List"])
-             (&/$UnivQ empty-env
-                       (&/$SumT
-                        ;; lux;Nil
-                        &/$UnitT
-                        ;; lux;Cons
-                        (&/$ProdT (&/$BoundT 1)
-                                  (&/$AppT (&/$BoundT 0)
-                                           (&/$BoundT 1)))))))
+  (&/$Named (&/T ["lux" "List"])
+            (&/$UnivQ empty-env
+                      (&/$Sum
+                       ;; lux;Nil
+                       &/$Unit
+                       ;; lux;Cons
+                       (&/$Product (&/$Bound 1)
+                                   (&/$App (&/$Bound 0)
+                                           (&/$Bound 1)))))))
 
 (def Maybe
-  (&/$NamedT (&/T ["lux" "Maybe"])
-             (&/$UnivQ empty-env
-                       (&/$SumT
-                        ;; lux;None
-                        &/$UnitT
-                        ;; lux;Some
-                        (&/$BoundT 1))
-                       )))
+  (&/$Named (&/T ["lux" "Maybe"])
+            (&/$UnivQ empty-env
+                      (&/$Sum
+                       ;; lux;None
+                       &/$Unit
+                       ;; lux;Some
+                       (&/$Bound 1))
+                      )))
 
 (def Type
-  (&/$NamedT (&/T ["lux" "Type"])
-             (let [Type (&/$AppT (&/$BoundT 0) (&/$BoundT 1))
-                   TypeList (&/$AppT List Type)
-                   TypePair (&/$ProdT Type Type)]
-               (&/$AppT (&/$UnivQ empty-env
-                                  (&/$SumT
-                                   ;; HostT
-                                   (&/$ProdT Text TypeList)
-                                   (&/$SumT
-                                    ;; VoidT
-                                    &/$UnitT
-                                    (&/$SumT
-                                     ;; UnitT
-                                     &/$UnitT
-                                     (&/$SumT
-                                      ;; SumT
+  (&/$Named (&/T ["lux" "Type"])
+            (let [Type (&/$App (&/$Bound 0) (&/$Bound 1))
+                  TypeList (&/$App List Type)
+                  TypePair (&/$Product Type Type)]
+              (&/$App (&/$UnivQ empty-env
+                                (&/$Sum
+                                 ;; Host
+                                 (&/$Product Text TypeList)
+                                 (&/$Sum
+                                  ;; Void
+                                  &/$Unit
+                                  (&/$Sum
+                                   ;; Unit
+                                   &/$Unit
+                                   (&/$Sum
+                                    ;; Sum
+                                    TypePair
+                                    (&/$Sum
+                                     ;; Product
+                                     TypePair
+                                     (&/$Sum
+                                      ;; Function
                                       TypePair
-                                      (&/$SumT
-                                       ;; ProdT
-                                       TypePair
-                                       (&/$SumT
-                                        ;; FunctionT
-                                        TypePair
-                                        (&/$SumT
-                                         ;; BoundT
+                                      (&/$Sum
+                                       ;; Bound
+                                       Nat
+                                       (&/$Sum
+                                        ;; Var
+                                        Nat
+                                        (&/$Sum
+                                         ;; Ex
                                          Nat
-                                         (&/$SumT
-                                          ;; VarT
-                                          Nat
-                                          (&/$SumT
-                                           ;; ExT
-                                           Nat
-                                           (&/$SumT
-                                            ;; UnivQ
-                                            (&/$ProdT TypeList Type)
-                                            (&/$SumT
-                                             ;; ExQ
-                                             (&/$ProdT TypeList Type)
-                                             (&/$SumT
-                                              ;; AppT
-                                              TypePair
-                                              ;; NamedT
-                                              (&/$ProdT Ident Type)))))))))))))
-                                  )
-                        &/$VoidT))))
+                                         (&/$Sum
+                                          ;; UnivQ
+                                          (&/$Product TypeList Type)
+                                          (&/$Sum
+                                           ;; ExQ
+                                           (&/$Product TypeList Type)
+                                           (&/$Sum
+                                            ;; App
+                                            TypePair
+                                            ;; Named
+                                            (&/$Product Ident Type)))))))))))))
+                                )
+                      &/$Void))))
 
 (def Ann-Value
-  (&/$NamedT (&/T ["lux" "Ann-Value"])
-             (let [Ann-Value (&/$AppT (&/$BoundT 0) (&/$BoundT 1))]
-               (&/$AppT (&/$UnivQ empty-env
-                                  (&/$SumT
-                                   ;; BoolA
-                                   Bool
-                                   (&/$SumT
-                                    ;; NatA
-                                    Nat
-                                    (&/$SumT
-                                     ;; IntA
-                                     Int
-                                     (&/$SumT
-                                      ;; DegA
-                                      Deg
-                                      (&/$SumT
-                                       ;; RealA
-                                       Real
-                                       (&/$SumT
-                                        ;; CharA
-                                        Char
-                                        (&/$SumT
-                                         ;; TextA
-                                         Text
-                                         (&/$SumT
-                                          ;; IdentA
-                                          Ident
-                                          (&/$SumT
-                                           ;; ListA
-                                           (&/$AppT List Ann-Value)
-                                           ;; DictA
-                                           (&/$AppT List (&/$ProdT Text Ann-Value)))))))))))
-                                  )
-                        &/$VoidT))))
+  (&/$Named (&/T ["lux" "Ann-Value"])
+            (let [Ann-Value (&/$App (&/$Bound 0) (&/$Bound 1))]
+              (&/$App (&/$UnivQ empty-env
+                                (&/$Sum
+                                 ;; BoolA
+                                 Bool
+                                 (&/$Sum
+                                  ;; NatA
+                                  Nat
+                                  (&/$Sum
+                                   ;; IntA
+                                   Int
+                                   (&/$Sum
+                                    ;; DegA
+                                    Deg
+                                    (&/$Sum
+                                     ;; RealA
+                                     Real
+                                     (&/$Sum
+                                      ;; CharA
+                                      Char
+                                      (&/$Sum
+                                       ;; TextA
+                                       Text
+                                       (&/$Sum
+                                        ;; IdentA
+                                        Ident
+                                        (&/$Sum
+                                         ;; ListA
+                                         (&/$App List Ann-Value)
+                                         ;; DictA
+                                         (&/$App List (&/$Product Text Ann-Value)))))))))))
+                                )
+                      &/$Void))))
 
 (def Anns
-  (&/$NamedT (&/T ["lux" "Anns"])
-             (&/$AppT List (&/$ProdT Ident Ann-Value))))
+  (&/$Named (&/T ["lux" "Anns"])
+            (&/$App List (&/$Product Ident Ann-Value))))
 
 (def Macro)
 
@@ -196,7 +196,7 @@
 
 (defn deref+ [type]
   (|case type
-    (&/$VarT id)
+    (&/$Var id)
     (deref id)
 
     _
@@ -270,7 +270,7 @@
              (->> compiler
                   (&/get$ &/$type-context)
                   (&/get$ &/$ex-counter)
-                  &/$ExT))))
+                  &/$Ex))))
 
 (declare clean*)
 (defn delete-var [id]
@@ -290,7 +290,7 @@
 
                                        (&/$Some ?type*)
                                        (|case ?type*
-                                         (&/$VarT ?id*)
+                                         (&/$Var ?id*)
                                          (if (= id ?id*)
                                            (return (&/T [?id &/$None]))
                                            (return binding))
@@ -308,13 +308,13 @@
 
 (defn with-var [k]
   (|do [id create-var
-        output (k (&/$VarT id))
+        output (k (&/$Var id))
         _ (delete-var id)]
     (return output)))
 
 (defn clean* [?tid type]
   (|case type
-    (&/$VarT ?id)
+    (&/$Var ?id)
     (if (= ?tid ?id)
       (|do [? (bound? ?id)]
         (if ?
@@ -325,7 +325,7 @@
           (|do [=type (deref ?id)
                 ==type (clean* ?tid =type)]
             (|case ==type
-              (&/$VarT =id)
+              (&/$Var =id)
               (if (= ?tid =id)
                 (|do [_ (unset-var ?id)]
                   (return type))
@@ -338,38 +338,38 @@
           (return type)))
       )
 
-    (&/$HostT ?name ?params)
+    (&/$Host ?name ?params)
     (|do [=params (&/map% (partial clean* ?tid) ?params)]
-      (return (&/$HostT ?name =params)))
+      (return (&/$Host ?name =params)))
     
-    (&/$FunctionT ?arg ?return)
+    (&/$Function ?arg ?return)
     (|do [=arg (clean* ?tid ?arg)
           =return (clean* ?tid ?return)]
-      (return (&/$FunctionT =arg =return)))
+      (return (&/$Function =arg =return)))
 
-    (&/$AppT ?lambda ?param)
+    (&/$App ?lambda ?param)
     (|do [=lambda (clean* ?tid ?lambda)
           =param (clean* ?tid ?param)]
-      (return (&/$AppT =lambda =param)))
+      (return (&/$App =lambda =param)))
 
-    (&/$ProdT ?left ?right)
+    (&/$Product ?left ?right)
     (|do [=left (clean* ?tid ?left)
           =right (clean* ?tid ?right)]
-      (return (&/$ProdT =left =right)))
+      (return (&/$Product =left =right)))
     
-    (&/$SumT ?left ?right)
+    (&/$Sum ?left ?right)
     (|do [=left (clean* ?tid ?left)
           =right (clean* ?tid ?right)]
-      (return (&/$SumT =left =right)))
+      (return (&/$Sum =left =right)))
 
     (&/$UnivQ ?env ?body)
     (|do [=env (&/map% (partial clean* ?tid) ?env)
-          body* (clean* ?tid ?body)] ;; TODO: DON'T CLEAN THE BODY
+          body* (clean* ?tid ?body)] ;; TODO: DO NOT CLEAN THE BODY
       (return (&/$UnivQ =env body*)))
 
     (&/$ExQ ?env ?body)
     (|do [=env (&/map% (partial clean* ?tid) ?env)
-          body* (clean* ?tid ?body)] ;; TODO: DON'T CLEAN THE BODY
+          body* (clean* ?tid ?body)] ;; TODO: DO NOT CLEAN THE BODY
       (return (&/$ExQ =env body*)))
 
     _
@@ -378,7 +378,7 @@
 
 (defn clean [tvar type]
   (|case tvar
-    (&/$VarT ?id)
+    (&/$Var ?id)
     (clean* ?id type)
     
     _
@@ -386,7 +386,7 @@
 
 (defn ^:private unravel-fun [type]
   (|case type
-    (&/$FunctionT ?in ?out)
+    (&/$Function ?in ?out)
     (|let [[??out ?args] (unravel-fun ?out)]
       (&/T [??out (&/$Cons ?in ?args)]))
 
@@ -395,7 +395,7 @@
 
 (defn ^:private unravel-app [fun-type]
   (|case fun-type
-    (&/$AppT ?left ?right)
+    (&/$App ?left ?right)
     (|let [[?fun-type ?args] (unravel-app ?left)]
       (&/T [?fun-type (&/|++ ?args (&/|list ?right))]))
 
@@ -415,7 +415,7 @@
     (defn <at> [tag type]
       "(-> Int Type (Lux Type))"
       (|case type
-        (&/$NamedT ?name ?type)
+        (&/$Named ?name ?type)
         (<at> tag ?type)
         
         (<tag> ?left ?right)
@@ -429,8 +429,8 @@
         _
         (&/fail-with-loc (str "[Type Error] Type is not a " <desc> ": " (show-type type))))))
 
-  &/$SumT  flatten-sum  sum-at  "Sum"
-  &/$ProdT flatten-prod prod-at "Product"
+  &/$Sum  flatten-sum  sum-at  "Sum"
+  &/$Product flatten-prod prod-at "Product"
   )
 
 (do-template [<name> <ctor> <unit>]
@@ -443,13 +443,13 @@
       (&/$Nil)
       <unit>))
 
-  Variant$ &/$SumT  &/$VoidT
-  Tuple$   &/$ProdT &/$UnitT
+  Variant$ &/$Sum  &/$Void
+  Tuple$   &/$Product &/$Unit
   )
 
 (defn show-type [^objects type]
   (|case type
-    (&/$HostT name params)
+    (&/$Host name params)
     (|case params
       (&/$Nil)
       (str "(host " name ")")
@@ -457,32 +457,32 @@
       _
       (str "(host " name " " (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
 
-    (&/$VoidT)
+    (&/$Void)
     "Void"
     
-    (&/$UnitT)
+    (&/$Unit)
     "Unit"
     
-    (&/$ProdT _)
+    (&/$Product _)
     (str "[" (->> (flatten-prod type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) "]")
 
-    (&/$SumT _)
+    (&/$Sum _)
     (str "(| " (->> (flatten-sum type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")")
     
-    (&/$FunctionT input output)
+    (&/$Function input output)
     (|let [[?out ?ins] (unravel-fun type)]
       (str "(-> " (->> ?ins (&/|map show-type) (&/|interpose " ") (&/fold str "")) " " (show-type ?out) ")"))
 
-    (&/$VarT id)
+    (&/$Var id)
     (str "⌈v:" id "⌋")
 
-    (&/$ExT ?id)
+    (&/$Ex ?id)
     (str "⟨e:" ?id "⟩")
 
-    (&/$BoundT idx)
+    (&/$Bound idx)
     (str idx)
 
-    (&/$AppT _ _)
+    (&/$App _ _)
     (|let [[?call-fun ?call-args] (unravel-app type)]
       (str "(" (show-type ?call-fun) " " (->> ?call-args (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
     
@@ -494,7 +494,7 @@
     (str "(Ex " "{" (->> ?env (&/|map show-type) (&/|interpose " ") (&/fold str "")) "} "
          (show-type ?body) ")")
     
-    (&/$NamedT ?name ?type)
+    (&/$Named ?name ?type)
     (&/ident->text ?name)
 
     _
@@ -503,52 +503,52 @@
 (defn type= [x y]
   (or (clojure.lang.Util/identical x y)
       (let [output (|case [x y]
-                     [(&/$NamedT [?xmodule ?xname] ?xtype) (&/$NamedT [?ymodule ?yname] ?ytype)]
+                     [(&/$Named [?xmodule ?xname] ?xtype) (&/$Named [?ymodule ?yname] ?ytype)]
                      (and (= ?xmodule ?ymodule)
                           (= ?xname ?yname))
 
-                     [(&/$HostT xname xparams) (&/$HostT yname yparams)]
+                     [(&/$Host xname xparams) (&/$Host yname yparams)]
                      (and (.equals ^Object xname yname)
                           (= (&/|length xparams) (&/|length yparams))
                           (&/fold2 #(and %1 (type= %2 %3)) true xparams yparams))
 
-                     [(&/$VoidT) (&/$VoidT)]
+                     [(&/$Void) (&/$Void)]
                      true
                      
-                     [(&/$UnitT) (&/$UnitT)]
+                     [(&/$Unit) (&/$Unit)]
                      true
 
-                     [(&/$ProdT xL xR) (&/$ProdT yL yR)]
+                     [(&/$Product xL xR) (&/$Product yL yR)]
                      (and (type= xL yL)
                           (type= xR yR))
 
-                     [(&/$SumT xL xR) (&/$SumT yL yR)]
+                     [(&/$Sum xL xR) (&/$Sum yL yR)]
                      (and (type= xL yL)
                           (type= xR yR))
 
-                     [(&/$FunctionT xinput xoutput) (&/$FunctionT yinput youtput)]
+                     [(&/$Function xinput xoutput) (&/$Function yinput youtput)]
                      (and (type= xinput yinput)
                           (type= xoutput youtput))
 
-                     [(&/$VarT xid) (&/$VarT yid)]
+                     [(&/$Var xid) (&/$Var yid)]
                      (= xid yid)
 
-                     [(&/$BoundT xidx) (&/$BoundT yidx)]
+                     [(&/$Bound xidx) (&/$Bound yidx)]
                      (= xidx yidx)
 
-                     [(&/$ExT xid) (&/$ExT yid)]
+                     [(&/$Ex xid) (&/$Ex yid)]
                      (= xid yid)
 
-                     [(&/$AppT xlambda xparam) (&/$AppT ylambda yparam)]
+                     [(&/$App xlambda xparam) (&/$App ylambda yparam)]
                      (and (type= xlambda ylambda) (type= xparam yparam))
                      
                      [(&/$UnivQ xenv xbody) (&/$UnivQ yenv ybody)]
                      (type= xbody ybody)
 
-                     [(&/$NamedT ?xname ?xtype) _]
+                     [(&/$Named ?xname ?xtype) _]
                      (type= ?xtype y)
 
-                     [_ (&/$NamedT ?yname ?ytype)]
+                     [_ (&/$Named ?yname ?ytype)]
                      (type= x ?ytype)
                      
                      [_ _]
@@ -574,7 +574,7 @@
 
 (defn show-type+ [type]
   (|case type
-    (&/$VarT ?id)
+    (&/$Var ?id)
     (fn [state]
       (|case ((deref ?id) state)
         (&/$Right state* bound)
@@ -597,17 +597,17 @@
 
 (defn beta-reduce [env type]
   (|case type
-    (&/$HostT ?name ?params)
-    (&/$HostT ?name (&/|map (partial beta-reduce env) ?params))
+    (&/$Host ?name ?params)
+    (&/$Host ?name (&/|map (partial beta-reduce env) ?params))
 
-    (&/$SumT ?left ?right)
-    (&/$SumT (beta-reduce env ?left) (beta-reduce env ?right))
+    (&/$Sum ?left ?right)
+    (&/$Sum (beta-reduce env ?left) (beta-reduce env ?right))
 
-    (&/$ProdT ?left ?right)
-    (&/$ProdT (beta-reduce env ?left) (beta-reduce env ?right))
+    (&/$Product ?left ?right)
+    (&/$Product (beta-reduce env ?left) (beta-reduce env ?right))
 
-    (&/$AppT ?type-fn ?type-arg)
-    (&/$AppT (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
+    (&/$App ?type-fn ?type-arg)
+    (&/$App (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
     
     (&/$UnivQ ?local-env ?local-def)
     (|case ?local-env
@@ -625,10 +625,10 @@
       _
       type)
 
-    (&/$FunctionT ?input ?output)
-    (&/$FunctionT (beta-reduce env ?input) (beta-reduce env ?output))
+    (&/$Function ?input ?output)
+    (&/$Function (beta-reduce env ?input) (beta-reduce env ?output))
 
-    (&/$BoundT ?idx)
+    (&/$Bound ?idx)
     (|case (&/|at ?idx env)
       (&/$Some bound)
       (beta-reduce env bound)
@@ -654,18 +654,18 @@
                               (&/$Cons type-fn))
                          local-def))
 
-    (&/$AppT F A)
+    (&/$App F A)
     (|do [type-fn* (apply-type F A)]
       (apply-type type-fn* param))
 
-    (&/$NamedT ?name ?type)
+    (&/$Named ?name ?type)
     (apply-type ?type param)
 
     ;; TODO: This one must go...
-    (&/$ExT id)
-    (return (&/$AppT type-fn param))
+    (&/$Ex id)
+    (return (&/$App type-fn param))
 
-    (&/$VarT id)
+    (&/$Var id)
     (|do [=type-fun (deref id)]
       (apply-type =type-fun param))
     
@@ -679,7 +679,7 @@
     (return fixpoints)
     (&/with-attempt
       (|case [expected actual]
-        [(&/$VarT ?eid) (&/$VarT ?aid)]
+        [(&/$Var ?eid) (&/$Var ?aid)]
         (if (= ?eid ?aid)
           (return fixpoints)
           (|do [ebound (fn [state]
@@ -710,7 +710,7 @@
               [(&/$Some etype) (&/$Some atype)]
               (check* fixpoints invariant?? etype atype))))
         
-        [(&/$VarT ?id) _]
+        [(&/$Var ?id) _]
         (fn [state]
           (|case ((set-var ?id actual) state)
             (&/$Right state* _)
@@ -721,7 +721,7 @@
                (check* fixpoints invariant?? bound actual))
              state)))
         
-        [_ (&/$VarT ?id)]
+        [_ (&/$Var ?id)]
         (fn [state]
           (|case ((set-var ?id expected) state)
             (&/$Right state* _)
@@ -732,15 +732,15 @@
                (check* fixpoints invariant?? expected bound))
              state)))
 
-        [(&/$AppT (&/$ExT eid) eA) (&/$AppT (&/$ExT aid) aA)]
+        [(&/$App (&/$Ex eid) eA) (&/$App (&/$Ex aid) aA)]
         (if (= eid aid)
           (check* fixpoints invariant?? eA aA)
           (check-error "" expected actual))
 
-        [(&/$AppT (&/$VarT ?id) A1) (&/$AppT F2 A2)]
+        [(&/$App (&/$Var ?id) A1) (&/$App F2 A2)]
         (fn [state]
           (|case ((|do [F1 (deref ?id)]
-                    (check* fixpoints invariant?? (&/$AppT F1 A1) actual))
+                    (check* fixpoints invariant?? (&/$App F1 A1) actual))
                   state)
             (&/$Right state* output)
             (return* state* output)
@@ -752,34 +752,34 @@
                  (check* fixpoints invariant?? expected actual*))
                state)
 
-              (&/$ExT _)
-              ((|do [fixpoints* (check* fixpoints invariant?? (&/$VarT ?id) F2)]
+              (&/$Ex _)
+              ((|do [fixpoints* (check* fixpoints invariant?? (&/$Var ?id) F2)]
                  (check* fixpoints* invariant?? A1 A2))
                state)
 
               _
-              ((|do [fixpoints* (check* fixpoints invariant?? (&/$VarT ?id) F2)
+              ((|do [fixpoints* (check* fixpoints invariant?? (&/$Var ?id) F2)
                      e* (apply-type F2 A1)
                      a* (apply-type F2 A2)]
                  (check* fixpoints* invariant?? e* a*))
                state))))
         
-        [(&/$AppT F1 A1) (&/$AppT (&/$VarT ?id) A2)]
+        [(&/$App F1 A1) (&/$App (&/$Var ?id) A2)]
         (fn [state]
           (|case ((|do [F2 (deref ?id)]
-                    (check* fixpoints invariant?? expected (&/$AppT F2 A2)))
+                    (check* fixpoints invariant?? expected (&/$App F2 A2)))
                   state)
             (&/$Right state* output)
             (return* state* output)
 
             (&/$Left _)
-            ((|do [fixpoints* (check* fixpoints invariant?? F1 (&/$VarT ?id))
+            ((|do [fixpoints* (check* fixpoints invariant?? F1 (&/$Var ?id))
                    e* (apply-type F1 A1)
                    a* (apply-type F1 A2)]
                (check* fixpoints* invariant?? e* a*))
              state)))
         
-        [(&/$AppT F A) _]
+        [(&/$App F A) _]
         (let [fp-pair (&/T [expected actual])
               _ (when (> (&/|length fixpoints) 64)
                   (&/|log! (println-str 'FIXPOINTS (->> (&/|keys fixpoints)
@@ -789,7 +789,7 @@
                                                                          (show-type a)))))
                                                         (&/|interpose "\n\n")
                                                         (&/fold str ""))))
-                  (assert false (prn-str 'check* '[(&/$AppT F A) _] (&/|length fixpoints) (show-type expected) (show-type actual))))]
+                  (assert false (prn-str 'check* '[(&/$App F A) _] (&/|length fixpoints) (show-type expected) (show-type actual))))]
           (|case (fp-get fp-pair fixpoints)
             (&/$Some ?)
             (if ?
@@ -800,10 +800,10 @@
             (|do [expected* (apply-type F A)]
               (check* (fp-put fp-pair true fixpoints) invariant?? expected* actual))))
 
-        [_ (&/$AppT (&/$ExT aid) A)]
+        [_ (&/$App (&/$Ex aid) A)]
         (check-error "" expected actual)
 
-        [_ (&/$AppT F A)]
+        [_ (&/$App F A)]
         (|do [actual* (apply-type F A)]
           (check* fixpoints invariant?? expected actual*))
 
@@ -833,7 +833,7 @@
               actual* (apply-type actual $arg)]
           (check* fixpoints invariant?? expected actual*))
 
-        [(&/$HostT e!data) (&/$HostT a!data)]
+        [(&/$Host e!data) (&/$Host a!data)]
         (|do [? &/jvm?]
           (if ?
             (|do [class-loader &/loader]
@@ -853,33 +853,33 @@
                   (return fixpoints))
                 (check-error "" expected actual)))))
 
-        [(&/$VoidT) (&/$VoidT)]
+        [(&/$Void) (&/$Void)]
         (return fixpoints)
         
-        [(&/$UnitT) (&/$UnitT)]
+        [(&/$Unit) (&/$Unit)]
         (return fixpoints)
 
-        [(&/$FunctionT eI eO) (&/$FunctionT aI aO)]
+        [(&/$Function eI eO) (&/$Function aI aO)]
         (|do [fixpoints* (check* fixpoints invariant?? aI eI)]
           (check* fixpoints* invariant?? eO aO))
 
-        [(&/$ProdT eL eR) (&/$ProdT aL aR)]
+        [(&/$Product eL eR) (&/$Product aL aR)]
         (|do [fixpoints* (check* fixpoints invariant?? eL aL)]
           (check* fixpoints* invariant?? eR aR))
 
-        [(&/$SumT eL eR) (&/$SumT aL aR)]
+        [(&/$Sum eL eR) (&/$Sum aL aR)]
         (|do [fixpoints* (check* fixpoints invariant?? eL aL)]
           (check* fixpoints* invariant?? eR aR))
 
-        [(&/$ExT e!id) (&/$ExT a!id)]
+        [(&/$Ex e!id) (&/$Ex a!id)]
         (if (= e!id a!id)
           (return fixpoints)
           (check-error "" expected actual))
 
-        [(&/$NamedT _ ?etype) _]
+        [(&/$Named _ ?etype) _]
         (check* fixpoints invariant?? ?etype actual)
 
-        [_ (&/$NamedT _ ?atype)]
+        [_ (&/$Named _ ?atype)]
         (check* fixpoints invariant?? expected ?atype)
 
         [_ _]
@@ -894,15 +894,15 @@
 (defn actual-type [type]
   "(-> Type (Lux Type))"
   (|case type
-    (&/$AppT ?all ?param)
+    (&/$App ?all ?param)
     (|do [type* (apply-type ?all ?param)]
       (actual-type type*))
 
-    (&/$VarT id)
+    (&/$Var id)
     (|do [=type (deref id)]
       (actual-type =type))
 
-    (&/$NamedT ?name ?type)
+    (&/$Named ?name ?type)
     (actual-type ?type)
     
     _
@@ -912,7 +912,7 @@
 (defn type-name [type]
   "(-> Type (Lux Ident))"
   (|case type
-    (&/$NamedT name _)
+    (&/$Named name _)
     (return name)
     
     _
@@ -922,7 +922,7 @@
 (defn unknown? [type]
   "(-> Type (Lux Bool))"
   (|case type
-    (&/$VarT id)
+    (&/$Var id)
     (|do [? (bound? id)]
       (return (not ?)))
 
@@ -932,7 +932,7 @@
 (defn resolve-type [type]
   "(-> Type (Lux Type))"
   (|case type
-    (&/$VarT id)
+    (&/$Var id)
     (|do [? (bound? id)]
       (if ?
         (deref id)
@@ -949,7 +949,7 @@
       (&/T [size-members (&/|++ (&/|take (dec size-members) ?member-types)
                                 (&/|list (|case (->> ?member-types (&/|drop (dec size-members)) (&/|reverse))
                                            (&/$Cons last prevs)
-                                           (&/fold (fn [right left] (&/$ProdT left right))
+                                           (&/fold (fn [right left] (&/$Product left right))
                                                    last prevs))))])
       (&/T [size-types ?member-types])
       )))
@@ -966,48 +966,48 @@
       (&/$Cons last prevs)
       (&/fold (fn [r l] (<plus> l r)) last prevs)))
 
-  fold-prod &/$UnitT &/$ProdT
-  fold-sum  &/$VoidT &/$SumT
+  fold-prod &/$Unit &/$Product
+  fold-sum  &/$Void &/$Sum
   )
 
 (def create-var+
   (|do [id create-var]
-    (return (&/$VarT id))))
+    (return (&/$Var id))))
 
 (defn ^:private push-app [inf-type inf-var]
   (|case inf-type
-    (&/$AppT inf-type* inf-var*)
-    (&/$AppT (push-app inf-type* inf-var) inf-var*)
+    (&/$App inf-type* inf-var*)
+    (&/$App (push-app inf-type* inf-var) inf-var*)
 
     _
-    (&/$AppT inf-type inf-var)))
+    (&/$App inf-type inf-var)))
 
 (defn ^:private push-name [name inf-type]
   (|case inf-type
-    (&/$AppT inf-type* inf-var*)
-    (&/$AppT (push-name name inf-type*) inf-var*)
+    (&/$App inf-type* inf-var*)
+    (&/$App (push-name name inf-type*) inf-var*)
 
     _
-    (&/$NamedT name inf-type)))
+    (&/$Named name inf-type)))
 
 (defn ^:private push-univq [env inf-type]
   (|case inf-type
-    (&/$AppT inf-type* inf-var*)
-    (&/$AppT (push-univq env inf-type*) inf-var*)
+    (&/$App inf-type* inf-var*)
+    (&/$App (push-univq env inf-type*) inf-var*)
 
     _
     (&/$UnivQ env inf-type)))
 
 (defn instantiate-inference [type]
   (|case type
-    (&/$NamedT ?name ?type)
+    (&/$Named ?name ?type)
     (|do [output (instantiate-inference ?type)]
       (return (push-name ?name output)))
 
     (&/$UnivQ _aenv _abody)
     (|do [inf-var create-var
           output (instantiate-inference _abody)]
-      (return (push-univq _aenv (push-app output (&/$VarT inf-var)))))
+      (return (push-univq _aenv (push-app output (&/$Var inf-var)))))
 
     _
     (return type)))
diff --git a/luxc/src/lux/type/host.clj b/luxc/src/lux/type/host.clj
index e2f7c1c1f..7d894b4df 100644
--- a/luxc/src/lux/type/host.clj
+++ b/luxc/src/lux/type/host.clj
@@ -77,18 +77,18 @@
     (let [gclass-name (.getName class)]
       (case gclass-name
         ("[Z" "[B" "[S" "[I" "[J" "[F" "[D" "[C")
-        (&/$HostT gclass-name (&/|list))
+        (&/$Host gclass-name (&/|list))
         ;; else
         (if-let [[_ _ arr-obrackets arr-obase simple-base arr-pbrackets arr-pbase] (re-find class-name-re gclass-name)]
           (let [base (or arr-obase simple-base (jprim->lprim arr-pbase))]
             (if (.equals "void" base)
-              &/$UnitT
-              (reduce (fn [inner _] (&/$HostT array-data-tag (&/|list inner)))
-                      (&/$HostT base (try (-> (Class/forName base) .getTypeParameters
-                                              seq count (repeat (&/$HostT "java.lang.Object" &/$Nil))
-                                              &/->list)
-                                       (catch Exception e
-                                         (&/|list))))
+              &/$Unit
+              (reduce (fn [inner _] (&/$Host array-data-tag (&/|list inner)))
+                      (&/$Host base (try (-> (Class/forName base) .getTypeParameters
+                                             seq count (repeat (&/$Host "java.lang.Object" &/$Nil))
+                                             &/->list)
+                                      (catch Exception e
+                                        (&/|list))))
                       (range (count (or arr-obrackets arr-pbrackets "")))))
             ))))))
 
@@ -99,7 +99,7 @@
 
         (instance? GenericArrayType refl-type)
         (|do [inner-type (instance-param existential matchings (.getGenericComponentType ^GenericArrayType refl-type))]
-          (return (&/$HostT array-data-tag (&/|list inner-type))))
+          (return (&/$Host array-data-tag (&/|list inner-type))))
         
         (instance? ParameterizedType refl-type)
         (|do [:let [refl-type* ^ParameterizedType refl-type]
@@ -107,8 +107,8 @@
                            .getActualTypeArguments
                            seq &/->list
                            (&/map% (partial instance-param existential matchings)))]
-          (return (&/$HostT (->> refl-type* ^Class (.getRawType) .getName)
-                            params*)))
+          (return (&/$Host (->> refl-type* ^Class (.getRawType) .getName)
+                           params*)))
         
         (instance? TypeVariable refl-type)
         (let [gvar (.getName ^TypeVariable refl-type)]
@@ -127,13 +127,13 @@
 (defn principal-class [refl-type]
   (cond (instance? Class refl-type)
         (|case (class->type refl-type)
-          (&/$HostT "#Array" (&/$Cons (&/$HostT class-name _) (&/$Nil)))
+          (&/$Host "#Array" (&/$Cons (&/$Host class-name _) (&/$Nil)))
           (str "[" (&host-generics/->type-signature class-name))
 
-          (&/$HostT class-name _)
+          (&/$Host class-name _)
           (&host-generics/->type-signature class-name)
 
-          (&/$UnitT)
+          (&/$Unit)
           "V")
 
         (instance? GenericArrayType refl-type)
@@ -157,7 +157,7 @@
   (|case gtype
     (&/$GenericArray component-type)
     (|do [inner-type (instance-gtype existential matchings component-type)]
-      (return (&/$HostT array-data-tag (&/|list inner-type))))
+      (return (&/$Host array-data-tag (&/|list inner-type))))
     
     (&/$GenericClass type-name type-params)
     ;; When referring to type-parameters during class or method
@@ -171,7 +171,7 @@
       (return m-type)
       (|do [params* (&/map% (partial instance-gtype existential matchings)
                             type-params)]
-        (return (&/$HostT type-name params*))))
+        (return (&/$Host type-name params*))))
     
     (&/$GenericTypeVar var-name)
     (if-let [m-type (&/|get var-name matchings)]
@@ -232,7 +232,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 (&/$HostT (.getName sub-class*) sub-params*))))
+          (return (&/$Host (.getName sub-class*) sub-params*))))
       (&/fail-with-loc (str "[Host Error] Classes do not have a subtyping relationship: " sub-class " </= " super-class)))))
 
 (defn as-obj [class]
@@ -271,7 +271,7 @@
                  (if (= (&/|length e!params) (&/|length a!params))
                    (|do [_ (&/map2% check e!params a!params)]
                      (return fixpoints))
-                   (check-error "" (&/$HostT e!name e!params) (&/$HostT a!name a!params)))
+                   (check-error "" (&/$Host e!name e!params) (&/$Host a!name a!params)))
 
                  (or (lux-type? e!name)
                      (lux-type? a!name))
@@ -280,14 +280,14 @@
                          (and (not (primitive-type? e!name))
                               (= null-data-tag a!name)))
                    (return fixpoints)
-                   (check-error "" (&/$HostT e!name e!params) (&/$HostT a!name a!params)))
+                   (check-error "" (&/$Host e!name e!params) (&/$Host a!name a!params)))
 
                  (not invariant??)
                  (|do [actual* (->super-type existential class-loader e!name a!name a!params)]
-                   (check (&/$HostT e!name e!params) actual*))
+                   (check (&/$Host e!name e!params) actual*))
 
                  :else
-                 (check-error "" (&/$HostT e!name e!params) (&/$HostT a!name a!params))))
+                 (check-error "" (&/$Host e!name e!params) (&/$Host a!name a!params))))
       (catch Exception e
         (throw e)))))
 
diff --git a/luxc/test/test/lux/type.clj b/luxc/test/test/lux/type.clj
index a12e5c89b..5a9a7ff1b 100644
--- a/luxc/test/test/lux/type.clj
+++ b/luxc/test/test/lux/type.clj
@@ -7,9 +7,9 @@
 
 ;; [Tests]
 (deftest check-base-types
-  (|case (&/run-state (|do [_ (&type/check &/$UnitT &/$UnitT)
+  (|case (&/run-state (|do [_ (&type/check &/$Unit &/$Unit)
 
-                            _ (&type/check &/$VoidT &/$VoidT)]
+                            _ (&type/check &/$Void &/$Void)]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -20,11 +20,11 @@
     ))
 
 (deftest check-simple-host-types
-  (|case (&/run-state (|do [_ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil)
-                                           (&/$HostT "java.lang.Boolean" &/$Nil))
+  (|case (&/run-state (|do [_ (&type/check (&/$Host "java.lang.Boolean" &/$Nil)
+                                           (&/$Host "java.lang.Boolean" &/$Nil))
                             
-                            _ (&type/check (&/$HostT "java.lang.Object" &/$Nil)
-                                           (&/$HostT "java.lang.Boolean" &/$Nil))]
+                            _ (&type/check (&/$Host "java.lang.Object" &/$Nil)
+                                           (&/$Host "java.lang.Boolean" &/$Nil))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -35,14 +35,14 @@
     ))
 
 (deftest check-complex-host-types
-  (|case (&/run-state (|do [_ (&type/check (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                           (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil))))
+  (|case (&/run-state (|do [_ (&type/check (&/$Host "java.util.List" (&/|list (&/$Host "java.lang.Boolean" &/$Nil)))
+                                           (&/$Host "java.util.List" (&/|list (&/$Host "java.lang.Boolean" &/$Nil))))
                             
-                            _ (&type/check (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Object" &/$Nil)))
-                                           (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil))))
+                            _ (&type/check (&/$Host "java.util.List" (&/|list (&/$Host "java.lang.Object" &/$Nil)))
+                                           (&/$Host "java.util.List" (&/|list (&/$Host "java.lang.Boolean" &/$Nil))))
 
-                            _ (&type/check (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                           (&/$HostT "java.util.ArrayList" (&/|list (&/$HostT "java.lang.Boolean" &/$Nil))))]
+                            _ (&type/check (&/$Host "java.util.List" (&/|list (&/$Host "java.lang.Boolean" &/$Nil)))
+                                           (&/$Host "java.util.ArrayList" (&/|list (&/$Host "java.lang.Boolean" &/$Nil))))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -53,14 +53,14 @@
     ))
 
 (deftest check-named-types
-  (|case (&/run-state (|do [_ (&type/check (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$HostT "java.lang.Boolean" &/$Nil))
+  (|case (&/run-state (|do [_ (&type/check (&/$Named (&/T ["lux" "Bool"]) (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$Host "java.lang.Boolean" &/$Nil))
                             
-                            _ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil)
-                                           (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil)))
+                            _ (&type/check (&/$Host "java.lang.Boolean" &/$Nil)
+                                           (&/$Named (&/T ["lux" "Bool"]) (&/$Host "java.lang.Boolean" &/$Nil)))
                             
-                            _ (&type/check (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil)))]
+                            _ (&type/check (&/$Named (&/T ["lux" "Bool"]) (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$Named (&/T ["lux" "Bool"]) (&/$Host "java.lang.Boolean" &/$Nil)))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -71,41 +71,41 @@
     ))
 
 (deftest check-sum-types
-  (|case (&/run-state (|do [_ (&type/check (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$SumT (&/$HostT "java.lang.Object" &/$Nil)
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$SumT (&/$HostT "java.lang.Object" &/$Nil)
-                                                    (&/$HostT "java.lang.Object" &/$Nil))
-                                           (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                    (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                             (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                           (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                    (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                             (&/$HostT "java.lang.Boolean" &/$Nil))))
-
-                            _ (&type/check (&/$SumT (&/$HostT "java.lang.Object" &/$Nil)
-                                                    (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                             (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                           (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                    (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                             (&/$HostT "java.lang.Boolean" &/$Nil))))
-
-                            _ (&type/check (&/$SumT (&/$HostT "java.lang.Object" &/$Nil)
-                                                    (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                             (&/$HostT "java.lang.Object" &/$Nil)))
-                                           (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                    (&/$SumT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                             (&/$HostT "java.lang.Boolean" &/$Nil))))]
+  (|case (&/run-state (|do [_ (&type/check (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                   (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                   (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$Sum (&/$Host "java.lang.Object" &/$Nil)
+                                                   (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                   (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$Sum (&/$Host "java.lang.Object" &/$Nil)
+                                                   (&/$Host "java.lang.Object" &/$Nil))
+                                           (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                   (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                   (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                           (&/$Host "java.lang.Boolean" &/$Nil)))
+                                           (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                   (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                           (&/$Host "java.lang.Boolean" &/$Nil))))
+
+                            _ (&type/check (&/$Sum (&/$Host "java.lang.Object" &/$Nil)
+                                                   (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                           (&/$Host "java.lang.Boolean" &/$Nil)))
+                                           (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                   (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                           (&/$Host "java.lang.Boolean" &/$Nil))))
+
+                            _ (&type/check (&/$Sum (&/$Host "java.lang.Object" &/$Nil)
+                                                   (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                           (&/$Host "java.lang.Object" &/$Nil)))
+                                           (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                   (&/$Sum (&/$Host "java.lang.Boolean" &/$Nil)
+                                                           (&/$Host "java.lang.Boolean" &/$Nil))))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -116,41 +116,41 @@
     ))
 
 (deftest check-prod-types
-  (|case (&/run-state (|do [_ (&type/check (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                     (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                     (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$ProdT (&/$HostT "java.lang.Object" &/$Nil)
-                                                     (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                     (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$ProdT (&/$HostT "java.lang.Object" &/$Nil)
-                                                     (&/$HostT "java.lang.Object" &/$Nil))
-                                           (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                     (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                     (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                               (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                           (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                     (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                               (&/$HostT "java.lang.Boolean" &/$Nil))))
-
-                            _ (&type/check (&/$ProdT (&/$HostT "java.lang.Object" &/$Nil)
-                                                     (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                               (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                           (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                     (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                               (&/$HostT "java.lang.Boolean" &/$Nil))))
-
-                            _ (&type/check (&/$ProdT (&/$HostT "java.lang.Object" &/$Nil)
-                                                     (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                               (&/$HostT "java.lang.Object" &/$Nil)))
-                                           (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                     (&/$ProdT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                               (&/$HostT "java.lang.Boolean" &/$Nil))))]
+  (|case (&/run-state (|do [_ (&type/check (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                       (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                       (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$Product (&/$Host "java.lang.Object" &/$Nil)
+                                                       (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                       (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$Product (&/$Host "java.lang.Object" &/$Nil)
+                                                       (&/$Host "java.lang.Object" &/$Nil))
+                                           (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                       (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                       (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                   (&/$Host "java.lang.Boolean" &/$Nil)))
+                                           (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                       (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                   (&/$Host "java.lang.Boolean" &/$Nil))))
+
+                            _ (&type/check (&/$Product (&/$Host "java.lang.Object" &/$Nil)
+                                                       (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                   (&/$Host "java.lang.Boolean" &/$Nil)))
+                                           (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                       (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                   (&/$Host "java.lang.Boolean" &/$Nil))))
+
+                            _ (&type/check (&/$Product (&/$Host "java.lang.Object" &/$Nil)
+                                                       (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                   (&/$Host "java.lang.Object" &/$Nil)))
+                                           (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                       (&/$Product (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                   (&/$Host "java.lang.Boolean" &/$Nil))))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -161,41 +161,41 @@
     ))
 
 (deftest check-lambda-types
-  (|case (&/run-state (|do [_ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                       (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                       (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                       (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$LambdaT (&/$HostT "java.lang.Object" &/$Nil)
-                                                       (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                       (&/$HostT "java.lang.Object" &/$Nil))
-                                           (&/$LambdaT (&/$HostT "java.lang.Object" &/$Nil)
-                                                       (&/$HostT "java.lang.Boolean" &/$Nil)))
+  (|case (&/run-state (|do [_ (&type/check (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                      (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                      (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                      (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$Lambda (&/$Host "java.lang.Object" &/$Nil)
+                                                      (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                      (&/$Host "java.lang.Object" &/$Nil))
+                                           (&/$Lambda (&/$Host "java.lang.Object" &/$Nil)
+                                                      (&/$Host "java.lang.Boolean" &/$Nil)))
                             
-                            _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                       (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                                   (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                           (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                       (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                                   (&/$HostT "java.lang.Boolean" &/$Nil))))
-
-                            _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                       (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                                   (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                           (&/$LambdaT (&/$HostT "java.lang.Object" &/$Nil)
-                                                       (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                                   (&/$HostT "java.lang.Boolean" &/$Nil))))
-
-                            _ (&type/check (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                       (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                                   (&/$HostT "java.lang.Object" &/$Nil)))
-                                           (&/$LambdaT (&/$HostT "java.lang.Object" &/$Nil)
-                                                       (&/$LambdaT (&/$HostT "java.lang.Boolean" &/$Nil)
-                                                                   (&/$HostT "java.lang.Boolean" &/$Nil))))
+                            _ (&type/check (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                      (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                 (&/$Host "java.lang.Boolean" &/$Nil)))
+                                           (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                      (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                 (&/$Host "java.lang.Boolean" &/$Nil))))
+
+                            _ (&type/check (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                      (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                 (&/$Host "java.lang.Boolean" &/$Nil)))
+                                           (&/$Lambda (&/$Host "java.lang.Object" &/$Nil)
+                                                      (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                 (&/$Host "java.lang.Boolean" &/$Nil))))
+
+                            _ (&type/check (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                      (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                 (&/$Host "java.lang.Object" &/$Nil)))
+                                           (&/$Lambda (&/$Host "java.lang.Object" &/$Nil)
+                                                      (&/$Lambda (&/$Host "java.lang.Boolean" &/$Nil)
+                                                                 (&/$Host "java.lang.Boolean" &/$Nil))))
                             ]
                         (return nil))
                       (&/init-state nil))
@@ -207,7 +207,7 @@
     ))
 
 (deftest check-ex-types
-  (|case (&/run-state (|do [_ (&type/check (&/$ExT 0) (&/$ExT 0))]
+  (|case (&/run-state (|do [_ (&type/check (&/$Ex 0) (&/$Ex 0))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -219,39 +219,39 @@
 
 (deftest check-univ-quantification
   (|case (&/run-state (|do [_ (&type/check (&/$UnivQ (&/|list)
-                                                     (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+                                                     (&/$Lambda &/$Void (&/$Bound 1)))
                                            (&/$UnivQ (&/|list)
-                                                     (&/$LambdaT &/$VoidT (&/$BoundT 1))))
+                                                     (&/$Lambda &/$Void (&/$Bound 1))))
 
                             _ (&type/check (&/$UnivQ (&/|list)
-                                                     (&/$SumT
+                                                     (&/$Sum
                                                       ;; lux;None
-                                                      &/$UnitT
+                                                      &/$Unit
                                                       ;; lux;Some
-                                                      (&/$BoundT 1)))
+                                                      (&/$Bound 1)))
                                            (&/$UnivQ (&/|list)
-                                                     (&/$SumT
+                                                     (&/$Sum
                                                       ;; lux;None
-                                                      &/$UnitT
+                                                      &/$Unit
                                                       ;; lux;Some
-                                                      (&/$BoundT 1))))
+                                                      (&/$Bound 1))))
 
                             _ (&type/check (&/$UnivQ (&/|list)
-                                                     (&/$SumT
+                                                     (&/$Sum
                                                       ;; lux;Nil
-                                                      &/$UnitT
+                                                      &/$Unit
                                                       ;; lux;Cons
-                                                      (&/$ProdT (&/$BoundT 1)
-                                                                (&/$AppT (&/$BoundT 0)
-                                                                         (&/$BoundT 1)))))
+                                                      (&/$Product (&/$Bound 1)
+                                                                  (&/$App (&/$Bound 0)
+                                                                          (&/$Bound 1)))))
                                            (&/$UnivQ (&/|list)
-                                                     (&/$SumT
+                                                     (&/$Sum
                                                       ;; lux;Nil
-                                                      &/$UnitT
+                                                      &/$Unit
                                                       ;; lux;Cons
-                                                      (&/$ProdT (&/$BoundT 1)
-                                                                (&/$AppT (&/$BoundT 0)
-                                                                         (&/$BoundT 1))))))]
+                                                      (&/$Product (&/$Bound 1)
+                                                                  (&/$App (&/$Bound 0)
+                                                                          (&/$Bound 1))))))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -263,39 +263,39 @@
 
 (deftest check-ex-quantification
   (|case (&/run-state (|do [_ (&type/check (&/$ExQ (&/|list)
-                                                   (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+                                                   (&/$Lambda &/$Void (&/$Bound 1)))
                                            (&/$ExQ (&/|list)
-                                                   (&/$LambdaT &/$VoidT (&/$BoundT 1))))
+                                                   (&/$Lambda &/$Void (&/$Bound 1))))
 
                             _ (&type/check (&/$ExQ (&/|list)
-                                                   (&/$SumT
+                                                   (&/$Sum
                                                     ;; lux;None
-                                                    &/$UnitT
+                                                    &/$Unit
                                                     ;; lux;Some
-                                                    (&/$BoundT 1)))
+                                                    (&/$Bound 1)))
                                            (&/$ExQ (&/|list)
-                                                   (&/$SumT
+                                                   (&/$Sum
                                                     ;; lux;None
-                                                    &/$UnitT
+                                                    &/$Unit
                                                     ;; lux;Some
-                                                    (&/$BoundT 1))))
+                                                    (&/$Bound 1))))
 
                             _ (&type/check (&/$ExQ (&/|list)
-                                                   (&/$SumT
+                                                   (&/$Sum
                                                     ;; lux;Nil
-                                                    &/$UnitT
+                                                    &/$Unit
                                                     ;; lux;Cons
-                                                    (&/$ProdT (&/$BoundT 1)
-                                                              (&/$AppT (&/$BoundT 0)
-                                                                       (&/$BoundT 1)))))
+                                                    (&/$Product (&/$Bound 1)
+                                                                (&/$App (&/$Bound 0)
+                                                                        (&/$Bound 1)))))
                                            (&/$ExQ (&/|list)
-                                                   (&/$SumT
+                                                   (&/$Sum
                                                     ;; lux;Nil
-                                                    &/$UnitT
+                                                    &/$Unit
                                                     ;; lux;Cons
-                                                    (&/$ProdT (&/$BoundT 1)
-                                                              (&/$AppT (&/$BoundT 0)
-                                                                       (&/$BoundT 1))))))]
+                                                    (&/$Product (&/$Bound 1)
+                                                                (&/$App (&/$Bound 0)
+                                                                        (&/$Bound 1))))))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -306,49 +306,49 @@
     ))
 
 (deftest check-app-type
-  (|case (&/run-state (|do [_ (&type/check (&/$AppT (&/$UnivQ (&/|list)
-                                                              (&/$LambdaT &/$VoidT (&/$BoundT 1)))
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$AppT (&/$UnivQ (&/|list)
-                                                              (&/$LambdaT &/$VoidT (&/$BoundT 1)))
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$AppT (&/$UnivQ (&/|list)
-                                                              (&/$SumT
-                                                               ;; lux;None
-                                                               &/$UnitT
-                                                               ;; lux;Some
-                                                               (&/$BoundT 1)))
-                                                    (&/$HostT "java.lang.Object" &/$Nil))
-                                           (&/$AppT (&/$UnivQ (&/|list)
-                                                              (&/$SumT
-                                                               ;; lux;None
-                                                               &/$UnitT
-                                                               ;; lux;Some
-                                                               (&/$BoundT 1)))
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$AppT (&/$ExQ (&/|list)
-                                                            (&/$LambdaT &/$VoidT (&/$BoundT 1)))
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil))
-                                           (&/$AppT (&/$ExQ (&/|list)
-                                                            (&/$LambdaT &/$VoidT (&/$BoundT 1)))
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil)))
-
-                            _ (&type/check (&/$AppT (&/$ExQ (&/|list)
-                                                            (&/$SumT
-                                                             ;; lux;None
-                                                             &/$UnitT
-                                                             ;; lux;Some
-                                                             (&/$BoundT 1)))
-                                                    (&/$HostT "java.lang.Object" &/$Nil))
-                                           (&/$AppT (&/$ExQ (&/|list)
-                                                            (&/$SumT
-                                                             ;; lux;None
-                                                             &/$UnitT
-                                                             ;; lux;Some
-                                                             (&/$BoundT 1)))
-                                                    (&/$HostT "java.lang.Boolean" &/$Nil)))]
+  (|case (&/run-state (|do [_ (&type/check (&/$App (&/$UnivQ (&/|list)
+                                                             (&/$Lambda &/$Void (&/$Bound 1)))
+                                                   (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$App (&/$UnivQ (&/|list)
+                                                             (&/$Lambda &/$Void (&/$Bound 1)))
+                                                   (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$App (&/$UnivQ (&/|list)
+                                                             (&/$Sum
+                                                              ;; lux;None
+                                                              &/$Unit
+                                                              ;; lux;Some
+                                                              (&/$Bound 1)))
+                                                   (&/$Host "java.lang.Object" &/$Nil))
+                                           (&/$App (&/$UnivQ (&/|list)
+                                                             (&/$Sum
+                                                              ;; lux;None
+                                                              &/$Unit
+                                                              ;; lux;Some
+                                                              (&/$Bound 1)))
+                                                   (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$App (&/$ExQ (&/|list)
+                                                           (&/$Lambda &/$Void (&/$Bound 1)))
+                                                   (&/$Host "java.lang.Boolean" &/$Nil))
+                                           (&/$App (&/$ExQ (&/|list)
+                                                           (&/$Lambda &/$Void (&/$Bound 1)))
+                                                   (&/$Host "java.lang.Boolean" &/$Nil)))
+
+                            _ (&type/check (&/$App (&/$ExQ (&/|list)
+                                                           (&/$Sum
+                                                            ;; lux;None
+                                                            &/$Unit
+                                                            ;; lux;Some
+                                                            (&/$Bound 1)))
+                                                   (&/$Host "java.lang.Object" &/$Nil))
+                                           (&/$App (&/$ExQ (&/|list)
+                                                           (&/$Sum
+                                                            ;; lux;None
+                                                            &/$Unit
+                                                            ;; lux;Some
+                                                            (&/$Bound 1)))
+                                                   (&/$Host "java.lang.Boolean" &/$Nil)))]
                         (return nil))
                       (&/init-state nil))
     (&/$Right state nil)
@@ -361,36 +361,36 @@
 (deftest check-var-type
   (|case (&/run-state (|do [_ (&type/with-var
                                 (fn [$var]
-                                  (|do [_ (&type/check $var (&/$HostT "java.lang.Boolean" &/$Nil))
-                                        (&/$HostT "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
+                                  (|do [_ (&type/check $var (&/$Host "java.lang.Boolean" &/$Nil))
+                                        (&/$Host "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
                                     (return nil))))
 
                             _ (&type/with-var
                                 (fn [$var]
-                                  (|do [_ (&type/check (&/$AppT (&/$UnivQ (&/|list)
-                                                                          (&/$LambdaT &/$VoidT (&/$BoundT 1)))
-                                                                $var)
-                                                       (&/$AppT (&/$UnivQ (&/|list)
-                                                                          (&/$LambdaT &/$VoidT (&/$BoundT 1)))
-                                                                (&/$HostT "java.lang.Boolean" &/$Nil)))
-                                        (&/$HostT "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
+                                  (|do [_ (&type/check (&/$App (&/$UnivQ (&/|list)
+                                                                         (&/$Lambda &/$Void (&/$Bound 1)))
+                                                               $var)
+                                                       (&/$App (&/$UnivQ (&/|list)
+                                                                         (&/$Lambda &/$Void (&/$Bound 1)))
+                                                               (&/$Host "java.lang.Boolean" &/$Nil)))
+                                        (&/$Host "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
                                     (return nil))))
 
                             _ (&type/with-var
                                 (fn [$var]
-                                  (|do [_ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil) $var)
-                                        (&/$HostT "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
+                                  (|do [_ (&type/check (&/$Host "java.lang.Boolean" &/$Nil) $var)
+                                        (&/$Host "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
                                     (return nil))))
 
                             _ (&type/with-var
                                 (fn [$var]
-                                  (|do [_ (&type/check (&/$AppT (&/$UnivQ (&/|list)
-                                                                          (&/$LambdaT &/$VoidT (&/$BoundT 1)))
-                                                                (&/$HostT "java.lang.Boolean" &/$Nil))
-                                                       (&/$AppT (&/$UnivQ (&/|list)
-                                                                          (&/$LambdaT &/$VoidT (&/$BoundT 1)))
-                                                                $var))
-                                        (&/$HostT "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
+                                  (|do [_ (&type/check (&/$App (&/$UnivQ (&/|list)
+                                                                         (&/$Lambda &/$Void (&/$Bound 1)))
+                                                               (&/$Host "java.lang.Boolean" &/$Nil))
+                                                       (&/$App (&/$UnivQ (&/|list)
+                                                                         (&/$Lambda &/$Void (&/$Bound 1)))
+                                                               $var))
+                                        (&/$Host "java.lang.Boolean" (&/$Nil)) (&type/deref+ $var)]
                                     (return nil))))
 
                             _ (&type/with-var
@@ -412,11 +412,11 @@
                                   (&type/with-var
                                     (fn [$var2]
                                       (|do [_ (&type/check $var1 $var2)
-                                            _ (&type/check $var1 (&/$HostT "java.lang.Boolean" (&/|list)))
+                                            _ (&type/check $var1 (&/$Host "java.lang.Boolean" (&/|list)))
                                             =var1 (&type/deref+ $var1)
                                             _ (&/assert! (&type/type= =var1 $var2) "")
                                             =var2 (&type/deref+ $var2)
-                                            _ (&/assert! (&type/type= =var2 (&/$HostT "java.lang.Boolean" (&/|list))) "")]
+                                            _ (&/assert! (&type/type= =var2 (&/$Host "java.lang.Boolean" (&/|list))) "")]
                                         (return nil))))))
 
                             _ (&type/with-var
@@ -424,11 +424,11 @@
                                   (&type/with-var
                                     (fn [$var2]
                                       (|do [_ (&type/check $var2 $var1)
-                                            _ (&type/check $var1 (&/$HostT "java.lang.Boolean" (&/|list)))
+                                            _ (&type/check $var1 (&/$Host "java.lang.Boolean" (&/|list)))
                                             =var2 (&type/deref+ $var2)
                                             _ (&/assert! (&type/type= =var2 $var1) "")
                                             =var1 (&type/deref+ $var1)
-                                            _ (&/assert! (&type/type= =var1 (&/$HostT "java.lang.Boolean" (&/|list))) "")]
+                                            _ (&/assert! (&type/type= =var1 (&/$Host "java.lang.Boolean" (&/|list))) "")]
                                         (return nil))))))
                             
                             _ (&type/with-var
@@ -436,11 +436,11 @@
                                   (&type/with-var
                                     (fn [$var2]
                                       (|do [_ (&type/check $var1 $var2)
-                                            _ (&type/check $var2 (&/$HostT "java.lang.Boolean" (&/|list)))
+                                            _ (&type/check $var2 (&/$Host "java.lang.Boolean" (&/|list)))
                                             =var1 (&type/deref+ $var1)
                                             _ (&/assert! (&type/type= =var1 $var2) "")
                                             =var2 (&type/deref+ $var2)
-                                            _ (&/assert! (&type/type= =var2 (&/$HostT "java.lang.Boolean" (&/|list))) "")]
+                                            _ (&/assert! (&type/type= =var2 (&/$Host "java.lang.Boolean" (&/|list))) "")]
                                         (return nil))))))
 
                             _ (&type/with-var
@@ -448,11 +448,11 @@
                                   (&type/with-var
                                     (fn [$var2]
                                       (|do [_ (&type/check $var2 $var1)
-                                            _ (&type/check $var2 (&/$HostT "java.lang.Boolean" (&/|list)))
+                                            _ (&type/check $var2 (&/$Host "java.lang.Boolean" (&/|list)))
                                             =var2 (&type/deref+ $var2)
                                             _ (&/assert! (&type/type= =var2 $var1) "")
                                             =var1 (&type/deref+ $var1)
-                                            _ (&/assert! (&type/type= =var1 (&/$HostT "java.lang.Boolean" (&/|list))) "")]
+                                            _ (&/assert! (&type/type= =var1 (&/$Host "java.lang.Boolean" (&/|list))) "")]
                                         (return nil))))))]
                         (return nil))
                       (&/init-state nil))