- Removed Void and Unit as kinds of types.

- Changed the value of "unit" in the old LuxC to match the one in new-luxc.

14 files changed, 225 insertions, 200 deletions

diff --git a/luxc/src/lux/analyser.clj b/luxc/src/lux/analyser.clj
index 1202d4faf..5a50be1fa 100644
--- a/luxc/src/lux/analyser.clj
+++ b/luxc/src/lux/analyser.clj
@@ -201,7 +201,7 @@
 ;; [Resources]
 (defn analyse [optimize eval! compile-module compilers]
   (|do [asts &parser/parse]
-    (&/flat-map% (partial analyse-ast optimize eval! compile-module compilers &/$Void) asts)))
+    (&/flat-map% (partial analyse-ast optimize eval! compile-module compilers &type/Bottom) 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 8c82fe1cf..d0c856ffc 100644
--- a/luxc/src/lux/analyser/base.clj
+++ b/luxc/src/lux/analyser/base.clj
@@ -74,7 +74,7 @@
                   (return ?module))]
     (return (&/T [module* ?name]))))
 
-(let [tag-names #{"Primitive" "Void" "Unit" "Sum" "Product" "Function" "Bound" "Var" "Ex" "UnivQ" "ExQ" "Apply" "Named"}]
+(let [tag-names #{"Primitive" "Sum" "Product" "Function" "Bound" "Var" "Ex" "UnivQ" "ExQ" "Apply" "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 434a0f78a..ff00f1aa8 100644
--- a/luxc/src/lux/analyser/case.clj
+++ b/luxc/src/lux/analyser/case.clj
@@ -38,24 +38,26 @@
   (&/T [(&/T ["" -1 -1]) (&/$Tuple &/$Nil)]))
 
 (defn ^:private resolve-type [type]
-  (|case type
-    (&/$Var ?id)
-    (|do [type* (&/try-all% (&/|list (&type/deref ?id)
-                                     (&/fail-with-loc "##1##")))]
-      (resolve-type type*))
-
-    (&/$UnivQ _)
-    (|do [$var &type/existential
-          =type (&type/apply-type type $var)]
-      (&type/actual-type =type))
-
-    (&/$ExQ _ _)
-    (|do [$var &type/existential
-          =type (&type/apply-type type $var)]
-      (&type/actual-type =type))
+  (if (&type/type= &type/Top type)
+    (return type)
+    (|case type
+      (&/$Var ?id)
+      (|do [type* (&/try-all% (&/|list (&type/deref ?id)
+                                       (&/fail-with-loc "##1##")))]
+        (resolve-type type*))
+
+      (&/$UnivQ _)
+      (|do [$var &type/existential
+            =type (&type/apply-type type $var)]
+        (&type/actual-type =type))
+
+      (&/$ExQ _ _)
+      (|do [$var &type/existential
+            =type (&type/apply-type type $var)]
+        (&type/actual-type =type))
 
-    _
-    (&type/actual-type type)))
+      _
+      (&type/actual-type type))))
 
 (defn update-up-frame [frame]
   (|let [[_env _idx _var] frame]
@@ -239,9 +241,6 @@
     (&/$Named ?name ?type)
     (adjust-type* up ?type)
 
-    (&/$Unit)
-    (return type)
-
     _
     (&/fail-with-loc (str "[Pattern-matching Error] Cannot pattern-match against type: " (&type/show-type type)))
     ))
@@ -302,7 +301,7 @@
       (&/$Tuple ?members)
       (|case ?members
         (&/$Nil)
-        (|do [_ (&type/check value-type &/$Unit)
+        (|do [_ (&type/check value-type &type/Top)
               =kont kont]
           (return (&/T [($TupleTestAC (&/|list)) =kont])))
 
@@ -580,11 +579,8 @@
     (|case ?structs
       (&/$Nil)
       (|do [value-type* (resolve-type value-type)]
-        (|case value-type*
-          (&/$Unit)
+        (if (&type/type= &type/Top value-type*)
           (return true)
-
-          _
           (&/fail-with-loc "[Pattern-maching Error] Unit is not total.")))
       
       _
diff --git a/luxc/src/lux/analyser/lux.clj b/luxc/src/lux/analyser/lux.clj
index df5cfb789..efbf68e54 100644
--- a/luxc/src/lux/analyser/lux.clj
+++ b/luxc/src/lux/analyser/lux.clj
@@ -45,7 +45,7 @@
 ;; [Exports]
 (defn analyse-unit [analyse ?exo-type]
   (|do [_cursor &/cursor
-        _ (&type/check ?exo-type &/$Unit)]
+        _ (&type/check ?exo-type &type/Top)]
     (return (&/|list (&&/|meta ?exo-type _cursor
                                (&&/$tuple (&/|list)))))))
 
@@ -690,7 +690,7 @@
     (return (&/|list (coerce ==type =value)))))
 
 (let [input-type (&/$Apply &type/Text &type/List)
-      output-type (&/$Apply &/$Unit &type/IO)]
+      output-type (&/$Apply &type/Top &type/IO)]
   (defn analyse-program [analyse optimize compile-program ?args ?body]
     (|do [_ &/ensure-statement
           =body (&/with-scope ""
diff --git a/luxc/src/lux/analyser/module.clj b/luxc/src/lux/analyser/module.clj
index 8468249ab..fca407c4b 100644
--- a/luxc/src/lux/analyser/module.clj
+++ b/luxc/src/lux/analyser/module.clj
@@ -48,8 +48,9 @@
        ))
 
 (do-template [<flagger> <asker> <tag>]
-  (do (defn <flagger> [module-name]
-        "(-> Text (Lux Unit))"
+  (do (defn <flagger>
+        "(-> Text (Lux Top))"
+        [module-name]
         (fn [state]
           (let [state* (&/update$ &/$modules
                                   (fn [modules]
@@ -59,8 +60,9 @@
                                                modules))
                                   state)]
             (&/$Right (&/T [state* &/unit-tag])))))
-    (defn <asker> [module-name]
+    (defn <asker>
       "(-> Text (Lux Bool))"
+      [module-name]
       (fn [state]
         (if-let [=module (->> state (&/get$ &/$modules) (&/|get module-name))]
           (&/$Right (&/T [state (|case (&/get$ $module-state =module)
@@ -380,7 +382,7 @@
          state)))))
 
 (defn ensure-can-see-tag
-  "(-> Text Text (Lux Unit))"
+  "(-> Text Text (Lux Top))"
   [module tag-name]
   (|do [current-module &/get-module-name]
     (fn [state]
@@ -463,8 +465,8 @@
     _
     (&/fail-with-loc "[Analyser Error] No import meta-data.")))
 
-(def tag-groups
-  "(Lux (List [Text (List Text)]))"
+(def ^{:doc "(Lux (List [Text (List Text)]))"}
+  tag-groups
   (|do [module &/get-current-module]
     (return (&/|map (fn [pair]
                       (|case pair
@@ -473,5 +475,4 @@
                                              (|let [[t-prefix t-name] tag]
                                                t-name))
                                            tags)])))
-                    (&/get$ $types module)))
-    ))
+                    (&/get$ $types module)))))
diff --git a/luxc/src/lux/analyser/proc/common.clj b/luxc/src/lux/analyser/proc/common.clj
index e3cb5a4c8..94eadb72c 100644
--- a/luxc/src/lux/analyser/proc/common.clj
+++ b/luxc/src/lux/analyser/proc/common.clj
@@ -289,7 +289,7 @@
   ^:private analyse-nat-to-int   &type/Nat  &type/Int    ["nat" "to-int"]
   ^:private analyse-int-to-nat   &type/Int  &type/Nat    ["int" "to-nat"]
   
-  ^:private analyse-nat-char  &type/Nat  &type/Text   ["nat" "char"]
+  ^:private analyse-nat-char     &type/Nat  &type/Text   ["nat" "char"]
   
   ^:private analyse-int-to-frac  &type/Int  &type/Frac   ["int" "to-frac"]
   ^:private analyse-frac-to-int  &type/Frac &type/Int    ["frac" "to-int"]
@@ -297,7 +297,7 @@
   ^:private analyse-deg-to-frac  &type/Deg  &type/Frac   ["deg" "to-frac"]
   ^:private analyse-frac-to-deg  &type/Frac &type/Deg    ["frac" "to-deg"]
   
-  ^:private analyse-io-log       &type/Text &/$Unit     ["io" "log"]
+  ^:private analyse-io-log       &type/Text &type/Top    ["io" "log"]
   ^:private analyse-io-error     &type/Text &type/Bottom ["io" "error"]
   ^:private analyse-io-exit      &type/Int  &type/Bottom ["io" "exit"]
   )
@@ -459,7 +459,7 @@
           (|do [:let [(&/$Cons valueC (&/$Cons boxC (&/$Nil))) ?values]
                 boxA (&&/analyse-1 analyse (&type/Box threadT valueT) boxC)
                 valueA (&&/analyse-1 analyse valueT valueC)
-                _ (&type/check exo-type &/$Unit)
+                _ (&type/check exo-type &type/Top)
                 _cursor &/cursor]
             (return (&/|list (&&/|meta exo-type _cursor
                                        (&&/$proc (&/T ["box" "write"]) (&/|list valueA boxA) (&/|list)))))))))))
@@ -474,7 +474,7 @@
 (defn ^:private analyse-process-future [analyse exo-type ?values]
   (|do [:let [(&/$Cons ?procedure (&/$Nil)) ?values]
         =procedure (&&/analyse-1 analyse (&/$Apply &type/Top &type/IO) ?procedure)
-        _ (&type/check exo-type &/$Unit)
+        _ (&type/check exo-type &type/Top)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["process" "future"]) (&/|list =procedure) (&/|list)))))))
@@ -483,7 +483,7 @@
   (|do [:let [(&/$Cons ?milliseconds (&/$Cons ?procedure (&/$Nil))) ?values]
         =milliseconds (&&/analyse-1 analyse &type/Nat ?milliseconds)
         =procedure (&&/analyse-1 analyse (&/$Apply &type/Top &type/IO) ?procedure)
-        _ (&type/check exo-type &/$Unit)
+        _ (&type/check exo-type &type/Top)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
                                (&&/$proc (&/T ["process" "schedule"]) (&/|list =milliseconds =procedure) (&/|list)))))))
diff --git a/luxc/src/lux/analyser/proc/jvm.clj b/luxc/src/lux/analyser/proc/jvm.clj
index 8d926f437..2eef1082c 100644
--- a/luxc/src/lux/analyser/proc/jvm.clj
+++ b/luxc/src/lux/analyser/proc/jvm.clj
@@ -194,7 +194,7 @@
       "float"   (return (&/$Primitive "java.lang.Float" &/$Nil))
       "double"  (return (&/$Primitive "java.lang.Double" &/$Nil))
       "char"    (return (&/$Primitive "java.lang.Character" &/$Nil))
-      "void"    (return &/$Unit)
+      "void"    (return &type/Top)
       ;; else
       (|do [=params (&/map% (partial generic-class->type env) params)]
         (return (&/$Primitive name =params))))
@@ -252,7 +252,7 @@
           itype (generic-class->type full-env itype*)]
       (if (double-register-gclass? itype*)
         (&&env/with-local iname itype
-          (&&env/with-local "" &/$Void
+          (&&env/with-local "" &type/Bottom
             body*))
         (&&env/with-local iname itype
           body*)))))
@@ -265,7 +265,7 @@
       (&/$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 &/$Unit]
+            :let [output-type &type/Top]
             =ctor-args (&/map% (fn [ctor-arg]
                                  (|do [:let [[ca-type ca-term] ctor-arg]
                                        =ca-type (generic-class->type full-env ca-type)
@@ -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 &/$Unit]
+        :let [output-type &type/Top]
         _ (&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 &/$Unit]
+        :let [output-type &type/Top]
         _ (&type/check exo-type output-type)
         _cursor &/cursor]
     (return (&/|list (&&/|meta exo-type _cursor
@@ -829,7 +829,7 @@
         _ (compile-interface interface-decl supers =anns =methods)
         :let [_ (println 'INTERFACE (str module "." (&/|first interface-decl)))]
         _cursor &/cursor]
-    (return (&/|list (&&/|meta &/$Unit _cursor
+    (return (&/|list (&&/|meta &type/Top _cursor
                                (&&/$tuple (&/|list)))))))
 
 (defn ^:private analyse-jvm-class [analyse compile-class class-decl super-class interfaces =inheritance-modifier =anns ?fields methods]
@@ -848,7 +848,7 @@
           _ &/pop-dummy-name
           :let [_ (println 'CLASS full-name)]
           _cursor &/cursor]
-      (return (&/|list (&&/|meta &/$Unit _cursor
+      (return (&/|list (&&/|meta &type/Top _cursor
                                  (&&/$tuple (&/|list))))))))
 
 (defn ^:private captured-source [env-entry]
diff --git a/luxc/src/lux/analyser/record.clj b/luxc/src/lux/analyser/record.clj
index ac9a0e64d..595858873 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 &/$Unit]))
+                               (return (&/T [&/$Nil &type/Top]))
                                
                                (&/$Cons [[_ (&/$Tag tag1)] _] _)
                                (|do [[module name] (&&/resolved-ident tag1)
diff --git a/luxc/src/lux/base.clj b/luxc/src/lux/base.clj
index 02942f4e0..25c331b94 100644
--- a/luxc/src/lux/base.clj
+++ b/luxc/src/lux/base.clj
@@ -10,7 +10,7 @@
     (apply prn args)))
 
 ;; [Tags]
-(def unit-tag (.intern (str (char 0) "unit" (char 0))))
+(def unit-tag (.intern ""))
 
 (defn T [elems]
   (case (count elems)
@@ -86,8 +86,6 @@
 ;; Type
 (defvariant
   ("Primitive" 2)
-  ("Void" 0)
-  ("Unit" 0)
   ("Sum" 2)
   ("Product" 2)
   ("Function" 2)
@@ -413,8 +411,9 @@
     _
     (assert false (prn-str '|map f (adt->text xs)))))
 
-(defn |empty? [xs]
+(defn |empty?
   "(All [a] (-> (List a) Bool))"
+  [xs]
   (|case xs
     ($Nil)
     true
@@ -422,8 +421,9 @@
     ($Cons _ _)
     false))
 
-(defn |filter [p xs]
+(defn |filter
   "(All [a] (-> (-> a Bool) (List a) (List a)))"
+  [p xs]
   (|case xs
     ($Nil)
     xs
@@ -433,8 +433,9 @@
       ($Cons x (|filter p xs*))
       (|filter p xs*))))
 
-(defn flat-map [f xs]
+(defn flat-map
   "(All [a b] (-> (-> a (List b)) (List a) (List b)))"
+  [f xs]
   (|case xs
     ($Nil)
     xs
@@ -656,8 +657,9 @@
         (return* state unit-tag)
         (fail* msg)))))
 
-(defn |some [f xs]
+(defn |some
   "(All [a b] (-> (-> a (Maybe b)) (List a) (Maybe b)))"
+  [f xs]
   (|case xs
     ($Nil)
     $None
@@ -782,8 +784,9 @@
 (defn with-writer [writer body]
   (with-jvm-host-slot $writer (fn [_] ($Some writer)) body))
 
-(defn with-type-env [type-env body]
+(defn with-type-env
   "(All [a] (-> TypeEnv (Lux a) (Lux a)))"
+  [type-env body]
   (with-jvm-host-slot $type-env (partial |++ type-env) body))
 
 (defn push-dummy-name [real-name store-name]
@@ -853,17 +856,17 @@
       ($Left msg)
       (fail* msg))))
 
-(defn in-eval? [mode]
-  "(-> CompilerMode Bool)"
-  (|case mode
-    ($Eval) true
-    _       false))
+(do-template [<name> <tag>]
+  (defn <name>
+    "(-> CompilerMode Bool)"
+    [mode]
+    (|case mode
+      (<tag>) true
+      _       false))
 
-(defn in-repl? [mode]
-  "(-> CompilerMode Bool)"
-  (|case mode
-    ($REPL) true
-    _       false))
+  in-eval? $Eval
+  in-repl? $REPL
+  )
 
 (defn with-eval [body]
   (fn [state]
@@ -924,16 +927,17 @@
       ($Some module-name)
       (return* state module-name))))
 
-(defn find-module [name]
+(defn find-module
   "(-> Text (Lux (Module Compiler)))"
+  [name]
   (fn [state]
     (if-let [module (|get name (get$ $modules state))]
       (return* state module)
       ((fail-with-loc (str "[Error] Unknown module: " name))
        state))))
 
-(def get-current-module
-  "(Lux (Module Compiler))"
+(def ^{:doc "(Lux (Module Compiler))"}
+  get-current-module
   (|do [module-name get-module-name]
     (find-module module-name)))
 
@@ -1009,8 +1013,9 @@
           _
           output)))))
 
-(defn with-expected-type [type body]
+(defn with-expected-type
   "(All [a] (-> Type (Lux a)))"
+  [type body]
   (fn [state]
     (let [output (body (set$ $expected ($Some type) state))]
       (|case output
@@ -1021,8 +1026,9 @@
         _
         output))))
 
-(defn with-cursor [^objects cursor body]
+(defn with-cursor
   "(All [a] (-> Cursor (Lux a)))"
+  [^objects cursor body]
   (|let [[_file-name _ _] cursor]
     (if (= "" _file-name)
       body
@@ -1036,8 +1042,9 @@
             _
             output))))))
 
-(defn with-analysis-meta [^objects cursor type body]
+(defn with-analysis-meta
   "(All [a] (-> Cursor Type (Lux a)))"
+  [^objects cursor type body]
   (|let [[_file-name _ _] cursor]
     (if (= "" _file-name)
       (fn [state]
@@ -1065,8 +1072,8 @@
             _
             output))))))
 
-(def ensure-statement
-  "(Lux Unit)"
+(def ^{:doc "(Lux Top)"}
+  ensure-statement
   (fn [state]
     (|case (get$ $expected state)
       ($None)
@@ -1297,8 +1304,9 @@
     ;; (assert false)
     ))
 
-(defn ^:private enumerate* [idx xs]
+(defn ^:private enumerate*
   "(All [a] (-> Int (List a) (List (, Int a))))"
+  [idx xs]
   (|case xs
     ($Cons x xs*)
     ($Cons (T [idx x])
@@ -1308,23 +1316,26 @@
     xs
     ))
 
-(defn enumerate [xs]
+(defn enumerate
   "(All [a] (-> (List a) (List (, Int a))))"
+  [xs]
   (enumerate* 0 xs))
 
-(def modules
-  "(Lux (List Text))"
+(def ^{:doc "(Lux (List Text))"}
+  modules
   (fn [state]
     (return* state (|keys (get$ $modules state)))))
 
-(defn when% [test body]
-  "(-> Bool (Lux Unit) (Lux Unit))"
+(defn when%
+  "(-> Bool (Lux Top) (Lux Top))"
+  [test body]
   (if test
     body
     (return unit-tag)))
 
-(defn |at [idx xs]
+(defn |at
   "(All [a] (-> Int (List a) (Maybe a)))"
+  [idx xs]
   (|case xs
     ($Cons x xs*)
     (cond (< idx 0)
@@ -1337,11 +1348,11 @@
           (|at (dec idx) xs*))
 
     ($Nil)
-    $None
-    ))
+    $None))
 
-(defn normalize [ident]
+(defn normalize
   "(-> Ident (Lux Ident))"
+  [ident]
   (|case ident
     ["" name] (|do [module get-module-name]
                 (return (T [module name])))
@@ -1367,8 +1378,9 @@
       )))
 
 (do-template [<name> <default> <op>]
-  (defn <name> [p xs]
+  (defn <name>
     "(All [a] (-> (-> a Bool) (List a) Bool))"
+    [p xs]
     (|case xs
       ($Nil)
       <default>
@@ -1379,14 +1391,16 @@
   |every? true  and
   |any?   false or)
 
-(defn m-comp [f g]
+(defn m-comp
   "(All [a b c] (-> (-> b (Lux c)) (-> a (Lux b)) (-> a (Lux c))))"
+  [f g]
   (fn [x]
     (|do [y (g x)]
       (f y))))
 
-(defn with-attempt [m-value on-error]
+(defn with-attempt
   "(All [a] (-> (Lux a) (-> Text (Lux a)) (Lux a)))"
+  [m-value on-error]
   (fn [state]
     (|case (m-value state)
       ($Left msg)
diff --git a/luxc/src/lux/compiler/cache/type.clj b/luxc/src/lux/compiler/cache/type.clj
index 76cdbec52..338673807 100644
--- a/luxc/src/lux/compiler/cache/type.clj
+++ b/luxc/src/lux/compiler/cache/type.clj
@@ -26,12 +26,6 @@
       (&/$Primitive name params)
       (str "^" name stop (serialize-list serialize-type params))
 
-      (&/$Void)
-      "0"
-
-      (&/$Unit)
-      "1"
-      
       (&/$Product left right)
       (str "*" (serialize-type left) (serialize-type right))
 
@@ -78,16 +72,9 @@
             [(&/$Cons head tail) input*]))
         ))
 
-(do-template [<name> <signal> <type>]
-  (defn <name> [^String input]
-    (when (.startsWith input <signal>)
-      [<type> (.substring input 1)]
-      ))
-
-  ^:private deserialize-void  "0" &/$Void
-  ^:private deserialize-unit  "1" &/$Unit
-  ^:private deserialize-type* "T" &type/Type
-  )
+(defn ^:private deserialize-type* [^String input]
+  (when (.startsWith input "T")
+    [&type/Type (.substring input 1)]))
 
 (do-template [<name> <signal> <type>]
   (defn <name> [^String input]
@@ -142,8 +129,6 @@
   "(-> Text Type)"
   [input]
   (or (deserialize-type* input)
-      (deserialize-void input)
-      (deserialize-unit input)
       (deserialize-sum input)
       (deserialize-prod input)
       (deserialize-lambda input)
diff --git a/luxc/src/lux/compiler/jvm/proc/host.clj b/luxc/src/lux/compiler/jvm/proc/host.clj
index 041e72819..da2c5ccde 100644
--- a/luxc/src/lux/compiler/jvm/proc/host.clj
+++ b/luxc/src/lux/compiler/jvm/proc/host.clj
@@ -47,45 +47,44 @@
       double-class "java.lang.Double"
       char-class "java.lang.Character"]
   (defn prepare-return! [^MethodVisitor *writer* *type*]
-    (|case *type*
-      (&/$Unit)
+    (if (&type/type= &type/Top *type*)
       (.visitLdcInsn *writer* &/unit-tag)
+      (|case *type*
+        (&/$Primitive "boolean" (&/$Nil))
+        (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name boolean-class) "valueOf" (str "(Z)" (&host-generics/->type-signature boolean-class)))
+        
+        (&/$Primitive "byte" (&/$Nil))
+        (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name byte-class) "valueOf" (str "(B)" (&host-generics/->type-signature byte-class)))
 
-      (&/$Primitive "boolean" (&/$Nil))
-      (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name boolean-class) "valueOf" (str "(Z)" (&host-generics/->type-signature boolean-class)))
-      
-      (&/$Primitive "byte" (&/$Nil))
-      (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name byte-class) "valueOf" (str "(B)" (&host-generics/->type-signature byte-class)))
+        (&/$Primitive "short" (&/$Nil))
+        (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name short-class) "valueOf" (str "(S)" (&host-generics/->type-signature short-class)))
 
-      (&/$Primitive "short" (&/$Nil))
-      (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name short-class) "valueOf" (str "(S)" (&host-generics/->type-signature short-class)))
+        (&/$Primitive "int" (&/$Nil))
+        (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name int-class) "valueOf" (str "(I)" (&host-generics/->type-signature int-class)))
 
-      (&/$Primitive "int" (&/$Nil))
-      (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name int-class) "valueOf" (str "(I)" (&host-generics/->type-signature int-class)))
+        (&/$Primitive "long" (&/$Nil))
+        (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name long-class) "valueOf" (str "(J)" (&host-generics/->type-signature long-class)))
 
-      (&/$Primitive "long" (&/$Nil))
-      (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name long-class) "valueOf" (str "(J)" (&host-generics/->type-signature long-class)))
+        (&/$Primitive "float" (&/$Nil))
+        (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name float-class) "valueOf" (str "(F)" (&host-generics/->type-signature float-class)))
 
-      (&/$Primitive "float" (&/$Nil))
-      (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name float-class) "valueOf" (str "(F)" (&host-generics/->type-signature float-class)))
+        (&/$Primitive "double" (&/$Nil))
+        (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name double-class) "valueOf" (str "(D)" (&host-generics/->type-signature double-class)))
 
-      (&/$Primitive "double" (&/$Nil))
-      (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name double-class) "valueOf" (str "(D)" (&host-generics/->type-signature double-class)))
+        (&/$Primitive "char" (&/$Nil))
+        (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name char-class) "valueOf" (str "(C)" (&host-generics/->type-signature char-class)))
+        
+        (&/$Primitive _ _)
+        nil
 
-      (&/$Primitive "char" (&/$Nil))
-      (.visitMethodInsn *writer* Opcodes/INVOKESTATIC (&host-generics/->bytecode-class-name char-class) "valueOf" (str "(C)" (&host-generics/->type-signature char-class)))
-      
-      (&/$Primitive _ _)
-      nil
+        (&/$Named ?name ?type)
+        (prepare-return! *writer* ?type)
 
-      (&/$Named ?name ?type)
-      (prepare-return! *writer* ?type)
+        (&/$Ex _)
+        nil
 
-      (&/$Ex _)
-      nil
-
-      _
-      (assert false (str 'prepare-return! " " (&type/show-type *type*))))
+        _
+        (assert false (str 'prepare-return! " " (&type/show-type *type*)))))
     *writer*))
 
 ;; [Resources]
diff --git a/luxc/src/lux/host.clj b/luxc/src/lux/host.clj
index 97d2bd69d..3f0181c99 100644
--- a/luxc/src/lux/host.clj
+++ b/luxc/src/lux/host.clj
@@ -58,9 +58,6 @@
       (&/$Function _ _)
       (return (&host-generics/->type-signature function-class))
 
-      (&/$Unit)
-      (return "V")
-
       (&/$Sum _)
       (return object-array)
 
@@ -78,7 +75,9 @@
       (return ex-type-class)
 
       _
-      (assert false (str '->java-sig " " (&type/show-type type)))
+      (if (&type/type= &type/Top type)
+        (return "V")
+        (assert false (str '->java-sig " " (&type/show-type type))))
       )))
 
 (do-template [<name> <static?>]
diff --git a/luxc/src/lux/type.clj b/luxc/src/lux/type.clj
index 76d580cb0..b9c5898a7 100644
--- a/luxc/src/lux/type.clj
+++ b/luxc/src/lux/type.clj
@@ -59,14 +59,14 @@
 (def IO
   (&/$Named (&/T ["lux/codata" "IO"])
             (&/$UnivQ empty-env
-                      (&/$Function &/$Void (&/$Bound 1)))))
+                      (&/$Function Bottom (&/$Bound 1)))))
 
 (def List
   (&/$Named (&/T ["lux" "List"])
             (&/$UnivQ empty-env
                       (&/$Sum
                        ;; lux;Nil
-                       &/$Unit
+                       Top
                        ;; lux;Cons
                        (&/$Product (&/$Bound 1)
                                    (&/$Apply (&/$Bound 1)
@@ -77,7 +77,7 @@
             (&/$UnivQ empty-env
                       (&/$Sum
                        ;; lux;None
-                       &/$Unit
+                       Top
                        ;; lux;Some
                        (&/$Bound 1))
                       )))
@@ -87,46 +87,40 @@
             (let [Type (&/$Apply (&/$Bound 1) (&/$Bound 0))
                   TypeList (&/$Apply Type List)
                   TypePair (&/$Product Type Type)]
-              (&/$Apply &/$Void
+              (&/$Apply Bottom
                         (&/$UnivQ empty-env
                                   (&/$Sum
                                    ;; Primitive
                                    (&/$Product Text TypeList)
                                    (&/$Sum
-                                    ;; Void
-                                    &/$Unit
+                                    ;; Sum
+                                    TypePair
                                     (&/$Sum
-                                     ;; Unit
-                                     &/$Unit
+                                     ;; Product
+                                     TypePair
                                      (&/$Sum
-                                      ;; Sum
+                                      ;; Function
                                       TypePair
                                       (&/$Sum
-                                       ;; Product
-                                       TypePair
+                                       ;; Bound
+                                       Nat
                                        (&/$Sum
-                                        ;; Function
-                                        TypePair
+                                        ;; Var
+                                        Nat
                                         (&/$Sum
-                                         ;; Bound
+                                         ;; Ex
                                          Nat
                                          (&/$Sum
-                                          ;; Var
-                                          Nat
+                                          ;; UnivQ
+                                          (&/$Product TypeList Type)
                                           (&/$Sum
-                                           ;; Ex
-                                           Nat
+                                           ;; ExQ
+                                           (&/$Product TypeList Type)
                                            (&/$Sum
-                                            ;; UnivQ
-                                            (&/$Product TypeList Type)
-                                            (&/$Sum
-                                             ;; ExQ
-                                             (&/$Product TypeList Type)
-                                             (&/$Sum
-                                              ;; App
-                                              TypePair
-                                              ;; Named
-                                              (&/$Product Ident Type)))))))))))))
+                                            ;; App
+                                            TypePair
+                                            ;; Named
+                                            (&/$Product Ident Type)))))))))))
                                   )))))
 
 (def Cursor
@@ -423,8 +417,8 @@
       (&/$Nil)
       <unit>))
 
-  Variant$ &/$Sum  &/$Void
-  Tuple$   &/$Product &/$Unit
+  Variant$ &/$Sum  Bottom
+  Tuple$   &/$Product Top
   )
 
 (defn show-type [^objects type]
@@ -437,12 +431,6 @@
       _
       (str "(primitive " (pr-str name) " " (->> params (&/|map show-type) (&/|interpose " ") (&/fold str "")) ")"))
 
-    (&/$Void)
-    "Void"
-    
-    (&/$Unit)
-    "Unit"
-    
     (&/$Product _)
     (str "[" (->> (flatten-prod type) (&/|map show-type) (&/|interpose " ") (&/fold str "")) "]")
 
@@ -492,12 +480,6 @@
                           (= (&/|length xparams) (&/|length yparams))
                           (&/fold2 #(and %1 (type= %2 %3)) true xparams yparams))
 
-                     [(&/$Void) (&/$Void)]
-                     true
-                     
-                     [(&/$Unit) (&/$Unit)]
-                     true
-
                      [(&/$Product xL xR) (&/$Product yL yR)]
                      (and (type= xL yL)
                           (type= xR yR))
@@ -834,12 +816,6 @@
                   (return fixpoints))
                 (check-error "" expected actual)))))
 
-        [(&/$Void) (&/$Void)]
-        (return fixpoints)
-        
-        [(&/$Unit) (&/$Unit)]
-        (return fixpoints)
-
         [(&/$Function eI eO) (&/$Function aI aO)]
         (|do [fixpoints* (check* fixpoints invariant?? aI eI)]
           (check* fixpoints* invariant?? eO aO))
@@ -947,8 +923,8 @@
       (&/$Cons last prevs)
       (&/fold (fn [r l] (<plus> l r)) last prevs)))
 
-  fold-prod &/$Unit &/$Product
-  fold-sum  &/$Void &/$Sum
+  fold-prod Top &/$Product
+  fold-sum  Bottom &/$Sum
   )
 
 (def create-var+
diff --git a/luxc/src/lux/type/host.clj b/luxc/src/lux/type/host.clj
index c4d4ef243..2e2db3bf6 100644
--- a/luxc/src/lux/type/host.clj
+++ b/luxc/src/lux/type/host.clj
@@ -8,6 +8,61 @@
                               TypeVariable
                               WildcardType)))
 
+(defn ^:private type= [x y]
+  (or (clojure.lang.Util/identical x y)
+      (let [output (|case [x y]
+                     [(&/$Named [?xmodule ?xname] ?xtype) (&/$Named [?ymodule ?yname] ?ytype)]
+                     (and (= ?xmodule ?ymodule)
+                          (= ?xname ?yname))
+
+                     [(&/$Primitive xname xparams) (&/$Primitive yname yparams)]
+                     (and (.equals ^Object xname yname)
+                          (= (&/|length xparams) (&/|length yparams))
+                          (&/fold2 #(and %1 (type= %2 %3)) true xparams yparams))
+
+                     [(&/$Product xL xR) (&/$Product yL yR)]
+                     (and (type= xL yL)
+                          (type= xR yR))
+
+                     [(&/$Sum xL xR) (&/$Sum yL yR)]
+                     (and (type= xL yL)
+                          (type= xR yR))
+
+                     [(&/$Function xinput xoutput) (&/$Function yinput youtput)]
+                     (and (type= xinput yinput)
+                          (type= xoutput youtput))
+
+                     [(&/$Var xid) (&/$Var yid)]
+                     (= xid yid)
+
+                     [(&/$Bound xidx) (&/$Bound yidx)]
+                     (= xidx yidx)
+
+                     [(&/$Ex xid) (&/$Ex yid)]
+                     (= xid yid)
+
+                     [(&/$Apply xparam xlambda) (&/$Apply yparam ylambda)]
+                     (and (type= xparam yparam) (type= xlambda ylambda))
+                     
+                     [(&/$UnivQ xenv xbody) (&/$UnivQ yenv ybody)]
+                     (type= xbody ybody)
+
+                     [(&/$Named ?xname ?xtype) _]
+                     (type= ?xtype y)
+
+                     [_ (&/$Named ?yname ?ytype)]
+                     (type= x ?ytype)
+                     
+                     [_ _]
+                     false
+                     )]
+        output)))
+
+(def ^:private Top
+  (&/$Named (&/T ["lux" "Top"])
+            (&/$ExQ (&/|list)
+                    (&/$Bound 1))))
+
 ;; [Exports]
 (def array-data-tag "#Array")
 (def null-data-tag "#Null")
@@ -82,7 +137,7 @@
         (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)
-              &/$Unit
+              Top
               (reduce (fn [inner _] (&/$Primitive array-data-tag (&/|list inner)))
                       (&/$Primitive base (try (-> (Class/forName base) .getTypeParameters
                                                   seq count (repeat (&/$Primitive "java.lang.Object" &/$Nil))
@@ -126,15 +181,15 @@
 
 (defn principal-class [refl-type]
   (cond (instance? Class refl-type)
-        (|case (class->type refl-type)
-          (&/$Primitive "#Array" (&/$Cons (&/$Primitive class-name _) (&/$Nil)))
-          (str "[" (&host-generics/->type-signature class-name))
-
-          (&/$Primitive class-name _)
-          (&host-generics/->type-signature class-name)
-
-          (&/$Unit)
-          "V")
+        (let [class-type (class->type refl-type)]
+          (if (type= Top class-type)
+            "V"
+            (|case class-type
+              (&/$Primitive "#Array" (&/$Cons (&/$Primitive class-name _) (&/$Nil)))
+              (str "[" (&host-generics/->type-signature class-name))
+
+              (&/$Primitive class-name _)
+              (&host-generics/->type-signature class-name))))
 
         (instance? GenericArrayType refl-type)
         (str "[" (principal-class (.getGenericComponentType ^GenericArrayType refl-type)))