- Small fixes to reader & type-system.

- Test suites for reader, lexer and parser got updated.
- Added unit-tests for type-system.

5 files changed, 546 insertions, 83 deletions

diff --git a/src/lux/type.clj b/src/lux/type.clj
index 70a2f69fa..295d7bfdb 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -756,21 +756,15 @@
         [(&/$ExQ e!env e!def) _]
         (with-var
           (fn [$arg]
-            (|do [:let [expected* (beta-reduce (->> e!env
-                                                    (&/$Cons $arg)
-                                                    (&/$Cons expected))
-                                               e!def)]
+            (|do [expected* (apply-type expected $arg)
                   =output (check* class-loader fixpoints invariant?? expected* actual)
                   _ (clean $arg actual)]
               (return =output))))
 
         [_ (&/$ExQ a!env a!def)]
-        (|do [$arg existential]
-          (|let [actual* (beta-reduce (->> a!env
-                                           (&/$Cons $arg)
-                                           (&/$Cons expected))
-                                      a!def)]
-            (check* class-loader fixpoints invariant?? expected actual*)))
+        (|do [$arg existential
+              actual* (apply-type actual $arg)]
+          (check* class-loader fixpoints invariant?? expected actual*))
 
         [(&/$HostT e!data) (&/$HostT a!data)]
         (&&host/check-host-types (partial check* class-loader fixpoints true)
diff --git a/test/test/lux/lexer.clj b/test/test/lux/lexer.clj
index dc00c1d51..3bd45cb5f 100644
--- a/test/test/lux/lexer.clj
+++ b/test/test/lux/lexer.clj
@@ -5,11 +5,12 @@
 
 (ns test.lux.lexer
   (:use clojure.test)
-  (:require (lux [base :as & :refer [deftags |do return* return fail fail* |let |case]]
+  (:require (lux [base :as & :refer [|do return* return fail fail* |let |case]]
                  [reader :as &reader]
                  [lexer :as &lexer])
             [lux.analyser.module :as &a-module]
-            :reload-all))
+            :reload-all
+            ))
 
 ;; [Utils]
 (def ^:private module-name "test")
@@ -37,7 +38,7 @@
     (|case (&/run-state (|do [[_ single-line] &lexer/lex
                               [_ multi-line] &lexer/lex
                               [_ multi-line-embedded] &lexer/lex]
-                          (return (&/T single-line multi-line multi-line-embedded)))
+                          (return (&/T [single-line multi-line multi-line-embedded])))
                         (make-state (str "##" input1 "\n" "#(" input2 ")#" "\n" "#(" input3 ")#")))
       (&/$Right state [(&lexer/$Comment output1)
                        (&lexer/$Comment output2)
@@ -56,7 +57,7 @@
         input2 "false"]
     (|case (&/run-state (|do [[_ output1] &lexer/lex
                               [_ output2] &lexer/lex]
-                          (return (&/T output1 output2)))
+                          (return (&/T [output1 output2])))
                         (make-state (str input1 "\n" input2)))
       (&/$Right state [(&lexer/$Bool output1)
                        (&lexer/$Bool output2)])
@@ -75,7 +76,7 @@
     (|case (&/run-state (|do [[_ output1] &lexer/lex
                               [_ output2] &lexer/lex
                               [_ output3] &lexer/lex]
-                          (return (&/T output1 output2 output3)))
+                          (return (&/T [output1 output2 output3])))
                         (make-state (str input1 "\n" input2 "\n" input3)))
       (&/$Right state [(&lexer/$Int output1)
                        (&lexer/$Int output2)
@@ -96,7 +97,7 @@
     (|case (&/run-state (|do [[_ output1] &lexer/lex
                               [_ output2] &lexer/lex
                               [_ output3] &lexer/lex]
-                          (return (&/T output1 output2 output3)))
+                          (return (&/T [output1 output2 output3])))
                         (make-state (str input1 "\n" input2 "\n" input3)))
       (&/$Right state [(&lexer/$Real output1)
                        (&lexer/$Real output2)
@@ -129,7 +130,7 @@
                               [_ output7] &lexer/lex
                               [_ output8] &lexer/lex
                               [_ output9] &lexer/lex]
-                          (return (&/T output1 output2 output3 output4 output5 output6 output7 output8 output9)))
+                          (return (&/T [output1 output2 output3 output4 output5 output6 output7 output8 output9])))
                         (make-state (str "#\"" input1 "\"" "\n" "#\"" input2 "\"" "\n" "#\"" input3 "\""
                                          "\n" "#\"" input4 "\"" "\n" "#\"" input5 "\"" "\n" "#\"" input6 "\""
                                          "\n" "#\"" input7 "\"" "\n" "#\"" input8 "\"" "\n" "#\"" input9 "\"")))
@@ -161,16 +162,13 @@
   (let [input1 ""
         input2 "abc"
         input3 "yolo\\nlol\\tmeme"
-        input4 "This is a test \\
-                   \\ of multi-line text. \\
-
-                   \\ I just wanna make sure it works alright..."]
+        input4 "This is a test\\nof multi-line text.\\n\\nI just wanna make sure it works alright..."]
     (|case (&/run-state (|do [[_ output1] &lexer/lex
                               [_ output2] &lexer/lex
                               [_ output3] &lexer/lex
                               [_ output4] &lexer/lex]
-                          (return (&/T output1 output2 output3 output4)))
-                        (make-state (str "\"" input1 "\"" "\n" "\"" input2 "\"" "\n" "\"" input3 "\"")))
+                          (return (&/T [output1 output2 output3 output4])))
+                        (make-state (str "\"" input1 "\"" "\n" "\"" input2 "\"" "\n" "\"" input3 "\"" "\n" "\"" input4 "\"")))
       (&/$Right state [(&lexer/$Text output1)
                        (&lexer/$Text output2)
                        (&lexer/$Text output3)
@@ -197,22 +195,22 @@
                               [_ output3] &lexer/lex
                               [_ output4] &lexer/lex
                               [_ output5] &lexer/lex]
-                          (return (&/T output1 output2 output3 output4 output5)))
-                        (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5)))
+                          (return (&/T [output1 output2 output3 output4 output5])))
+                        (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5 " ")))
       (&/$Right state [(&lexer/$Symbol output1)
                        (&lexer/$Symbol output2)
                        (&lexer/$Symbol output3)
                        (&lexer/$Symbol output4)
                        (&lexer/$Symbol output5)])
       (are [input output] (&/ident= input output)
-           (&/T "" "foo")                     output1
-           (&/T "test" "bar0123456789")       output2
-           (&/T "lux" "b1a2z3")               output3
-           (&/T "test" "quux")                output4
-           (&/T "" "!_@$%^&*-+=.<>?/|\\~`':") output5)
+           (&/T ["" "foo"])                     output1
+           (&/T ["test" "bar0123456789"])       output2
+           (&/T ["lux" "b1a2z3"])               output3
+           (&/T ["test" "quux"])                output4
+           (&/T ["" "!_@$%^&*-+=.<>?/|\\~`':"]) output5)
       
       _
-      (is false "Couldn't read.")
+      (is false "Couldn't read")
       )))
 
 (deftest lex-tag
@@ -227,19 +225,19 @@
                               [_ output3] &lexer/lex
                               [_ output4] &lexer/lex
                               [_ output5] &lexer/lex]
-                          (return (&/T output1 output2 output3 output4 output5)))
-                        (make-state (str "#" input1 "\n" "#" input2 "\n" "#" input3 "\n" "#" input4 "\n" "#" input5)))
+                          (return (&/T [output1 output2 output3 output4 output5])))
+                        (make-state (str "#" input1 "\n" "#" input2 "\n" "#" input3 "\n" "#" input4 "\n" "#" input5 " ")))
       (&/$Right state [(&lexer/$Tag output1)
                        (&lexer/$Tag output2)
                        (&lexer/$Tag output3)
                        (&lexer/$Tag output4)
                        (&lexer/$Tag output5)])
       (are [input output] (&/ident= input output)
-           (&/T "" "foo")                     output1
-           (&/T "test" "bar0123456789")       output2
-           (&/T "lux" "b1a2z3")               output3
-           (&/T "test" "quux")                output4
-           (&/T "" "!_@$%^&*-+=.<>?/|\\~`':") output5)
+           (&/T ["" "foo"])                     output1
+           (&/T ["test" "bar0123456789"])       output2
+           (&/T ["lux" "b1a2z3"])               output3
+           (&/T ["test" "quux"])                output4
+           (&/T ["" "!_@$%^&*-+=.<>?/|\\~`':"]) output5)
       
       _
       (is false "Couldn't read.")
@@ -259,7 +257,7 @@
                               [_ output4] &lexer/lex
                               [_ output5] &lexer/lex
                               [_ output6] &lexer/lex]
-                          (return (&/T output1 output2 output3 output4 output5 output6)))
+                          (return (&/T [output1 output2 output3 output4 output5 output6])))
                         (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5 "\n" input6)))
       (&/$Right state [(&lexer/$Open_Paren)
                        (&lexer/$Close_Paren)
@@ -273,4 +271,6 @@
       (is false "Couldn't read.")
       )))
 
-;; (run-all-tests)
+(comment
+  (run-all-tests)
+  )
diff --git a/test/test/lux/parser.clj b/test/test/lux/parser.clj
index 13bd3500c..29e916b74 100644
--- a/test/test/lux/parser.clj
+++ b/test/test/lux/parser.clj
@@ -6,7 +6,7 @@
 (ns test.lux.parser
   (:use (clojure test
                  template))
-  (:require (lux [base :as & :refer [deftags |do return* return fail fail* |let |case]]
+  (:require (lux [base :as & :refer [|do return* return fail fail* |let |case]]
                  [reader :as &reader]
                  [parser :as &parser])
             [lux.analyser.module :as &a-module]
@@ -147,17 +147,20 @@
 (deftest parse-text
   (let [input1 ""
         input2 "abc"
-        input3 "yolo\\nlol\\tmeme"]
+        input3 "yolo\\nlol\\tmeme"
+        input4 "This is a test\\nof multi-line text.\\n\\nI just wanna make sure it works alright..."]
     (|case (&/run-state (|do [output1 &parser/parse
                               output2 &parser/parse
-                              output3 &parser/parse]
-                          (return (&/|++ output1 (&/|++ output2 output3))))
-                        (make-state (str "\"" input1 "\"" "\n" "\"" input2 "\"" "\n" "\"" input3 "\"")))
-      (&/$Right state (&/$Cons [_ (&/$TextS output1)] (&/$Cons [_ (&/$TextS output2)] (&/$Cons [_ (&/$TextS output3)] (&/$Nil)))))
+                              output3 &parser/parse
+                              output4 &parser/parse]
+                          (return (&/|++ output1 (&/|++ output2 (&/|++ output3 output4)))))
+                        (make-state (str "\"" input1 "\"" "\n" "\"" input2 "\"" "\n" "\"" input3 "\"" "\n" "\"" input4 "\"")))
+      (&/$Right state (&/$Cons [_ (&/$TextS output1)] (&/$Cons [_ (&/$TextS output2)] (&/$Cons [_ (&/$TextS output3)] (&/$Cons [_ (&/$TextS output4)] (&/$Nil))))))
       (are [input output] (= input output)
            input1            output1
            input2            output2
-           "yolo\nlol\tmeme" output3)
+           "yolo\nlol\tmeme" output3
+           "This is a test\nof multi-line text.\n\nI just wanna make sure it works alright..." output4)
       
       _
       (is false "Couldn't read.")
@@ -176,7 +179,7 @@
                               output4 &parser/parse
                               output5 &parser/parse]
                           (return (&/|++ output1 (&/|++ output2 (&/|++ output3 (&/|++ output4 output5))))))
-                        (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5)))
+                        (make-state (str input1 "\n" input2 "\n" input3 "\n" input4 "\n" input5 " ")))
       (&/$Right state (&/$Cons [_ (&/$SymbolS output1)]
                                (&/$Cons [_ (&/$SymbolS output2)]
                                         (&/$Cons [_ (&/$SymbolS output3)]
@@ -184,11 +187,11 @@
                                                           (&/$Cons [_ (&/$SymbolS output5)]
                                                                    (&/$Nil)))))))
       (are [input output] (&/ident= input output)
-           (&/T "" "foo")                     output1
-           (&/T "test" "bar0123456789")       output2
-           (&/T "lux" "b1a2z3")               output3
-           (&/T "test" "quux")                output4
-           (&/T "" "!_@$%^&*-+=.<>?/|\\~`':") output5)
+           (&/T ["" "foo"])                     output1
+           (&/T ["test" "bar0123456789"])       output2
+           (&/T ["lux" "b1a2z3"])               output3
+           (&/T ["test" "quux"])                output4
+           (&/T ["" "!_@$%^&*-+=.<>?/|\\~`':"]) output5)
       
       _
       (is false "Couldn't read.")
@@ -207,7 +210,7 @@
                               output4 &parser/parse
                               output5 &parser/parse]
                           (return (&/|++ output1 (&/|++ output2 (&/|++ output3 (&/|++ output4 output5))))))
-                        (make-state (str "#" input1 "\n" "#" input2 "\n" "#" input3 "\n" "#" input4 "\n" "#" input5)))
+                        (make-state (str "#" input1 "\n" "#" input2 "\n" "#" input3 "\n" "#" input4 "\n" "#" input5 " ")))
       (&/$Right state (&/$Cons [_ (&/$TagS output1)]
                                (&/$Cons [_ (&/$TagS output2)]
                                         (&/$Cons [_ (&/$TagS output3)]
@@ -215,11 +218,11 @@
                                                           (&/$Cons [_ (&/$TagS output5)]
                                                                    (&/$Nil)))))))
       (are [input output] (&/ident= input output)
-           (&/T "" "foo")                     output1
-           (&/T "test" "bar0123456789")       output2
-           (&/T "lux" "b1a2z3")               output3
-           (&/T "test" "quux")                output4
-           (&/T "" "!_@$%^&*-+=.<>?/|\\~`':") output5)
+           (&/T ["" "foo"])                     output1
+           (&/T ["test" "bar0123456789"])       output2
+           (&/T ["lux" "b1a2z3"])               output3
+           (&/T ["test" "quux"])                output4
+           (&/T ["" "!_@$%^&*-+=.<>?/|\\~`':"]) output5)
       
       _
       (is false "Couldn't read.")
@@ -236,10 +239,10 @@
                                                                       (&/$Cons [_ (&/$TagS tagv)]
                                                                                (&/$Nil))))))]
                                  (&/$Nil)))
-        (do (is (&/ident= (&/T "" "yolo") symv))
+        (do (is (&/ident= (&/T ["" "yolo"]) symv))
           (is (= 123 intv))
           (is (= "lol" textv))
-          (is (&/ident= (&/T "" "meme") tagv)))
+          (is (&/ident= (&/T ["" "meme"]) tagv)))
         
         _
         (is false "Couldn't read.")
@@ -257,13 +260,15 @@
                                                        (&/$Cons [[_ (&/$TextS textv)] [_ (&/$TagS tagv)]]
                                                                 (&/$Nil))))]
                                (&/$Nil)))
-      (do (is (&/ident= (&/T "" "yolo") symv))
+      (do (is (&/ident= (&/T ["" "yolo"]) symv))
         (is (= 123 intv))
         (is (= "lol" textv))
-        (is (&/ident= (&/T "" "meme") tagv)))
+        (is (&/ident= (&/T ["" "meme"]) tagv)))
       
       _
       (is false "Couldn't read.")
       )))
 
-(run-all-tests)
+(comment
+  (run-all-tests)
+  )
diff --git a/test/test/lux/reader.clj b/test/test/lux/reader.clj
index ca4797f10..ee9cb4c35 100644
--- a/test/test/lux/reader.clj
+++ b/test/test/lux/reader.clj
@@ -5,7 +5,7 @@
 
 (ns test.lux.reader
   (:use clojure.test)
-  (:require (lux [base :as & :refer [deftags |do return* return fail fail* |let |case]]
+  (:require (lux [base :as & :refer [|do return* return fail fail* |let |case]]
                  [reader :as &reader])
             :reload-all))
 
@@ -15,13 +15,13 @@
 
 ;; [Tests]
 (deftest test-source-code-reading
-  (is (= 4 (&/|length source))))
+  (is (= 5 (&/|length source))))
 
 (deftest test-text-reading
   ;; Should be capable of recognizing literal texts.
   (let [input "lo"]
     (|case (&/run-state (&reader/read-text input) init-state)
-      (&/$Right state [cursor output])
+      (&/$Right state [cursor end-line? output])
       (is (= input output))
 
       _
@@ -31,19 +31,8 @@
 (deftest test-regex-reading
   ;; Should be capable of matching simple, grouping regex-patterns.
   (|case (&/run-state (&reader/read-regex #"l(.)l") init-state)
-    (&/$Right state [cursor output])
-    (is (= "lol" "lol"))
-
-    _
-    (is false "Couldn't read.")
-    ))
-
-(deftest test-regex2-reading
-  ;; Should be capable of matching double, grouping regex-patterns.
-  (|case (&/run-state (&reader/read-regex2 #"(.)(..)") init-state)
-    (&/$Right state [cursor [left right]])
-    (is (and (= "l" left)
-             (= "ol" right)))
+    (&/$Right state [cursor end-line? output])
+    (is (= "lol" output))
 
     _
     (is false "Couldn't read.")
@@ -51,12 +40,14 @@
 
 (deftest test-regex+-reading
   ;; Should be capable of matching multi-line regex-patterns.
-  (|case (&/run-state (&reader/read-regex+ #"(?is)^(.*?)(cat|$)") init-state)
+  (|case (&/run-state (&reader/read-regex+ #"(?is)^((?!cat).)*") init-state)
     (&/$Right state [cursor output])
-    (is (= "lol\nmeme\nnyan " output))
+    (is (= "\nlol\nmeme\nnyan " output))
 
     _
     (is false "Couldn't read.")
     ))
 
-;; (run-all-tests)
+(comment
+  (run-all-tests)
+  )
diff --git a/test/test/lux/type.clj b/test/test/lux/type.clj
new file mode 100644
index 000000000..1a43f7cc4
--- /dev/null
+++ b/test/test/lux/type.clj
@@ -0,0 +1,473 @@
+;;  Copyright (c) Eduardo Julian. All rights reserved.
+;;  This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0.
+;;  If a copy of the MPL was not distributed with this file,
+;;  You can obtain one at http://mozilla.org/MPL/2.0/.
+
+(ns test.lux.type
+  (:use clojure.test)
+  (:require (lux [base :as & :refer [|do return* return fail fail* |let |case]]
+                 [type :as &type])
+            :reload-all
+            ))
+
+;; [Tests]
+(deftest check-base-types
+  (|case (&/run-state (|do [_ (&type/check &/$UnitT &/$UnitT)
+
+                            _ (&type/check &/$VoidT &/$VoidT)]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(deftest check-simple-host-types
+  (|case (&/run-state (|do [_ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil)
+                                           (&/$HostT "java.lang.Boolean" &/$Nil))
+                            
+                            _ (&type/check (&/$HostT "java.lang.Object" &/$Nil)
+                                           (&/$HostT "java.lang.Boolean" &/$Nil))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(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))))
+                            
+                            _ (&type/check (&/$HostT "java.util.List" (&/|list (&/$HostT "java.lang.Object" &/$Nil)))
+                                           (&/$HostT "java.util.List" (&/|list (&/$HostT "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))))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(deftest check-named-types
+  (|case (&/run-state (|do [_ (&type/check (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil))
+                                           (&/$HostT "java.lang.Boolean" &/$Nil))
+                            
+                            _ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil)
+                                           (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil)))
+                            
+                            _ (&type/check (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil))
+                                           (&/$NamedT (&/T ["lux" "Bool"]) (&/$HostT "java.lang.Boolean" &/$Nil)))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(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))))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(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))))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(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)))
+                            
+                            _ (&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))))
+                            ]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(deftest check-ex-types
+  (|case (&/run-state (|do [_ (&type/check (&/$ExT 0) (&/$ExT 0))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(deftest check-univ-quantification
+  (|case (&/run-state (|do [_ (&type/check (&/$UnivQ (&/|list)
+                                                     (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+                                           (&/$UnivQ (&/|list)
+                                                     (&/$LambdaT &/$VoidT (&/$BoundT 1))))
+
+                            _ (&type/check (&/$UnivQ (&/|list)
+                                                     (&/$SumT
+                                                      ;; lux;None
+                                                      &/$UnitT
+                                                      ;; lux;Some
+                                                      (&/$BoundT 1)))
+                                           (&/$UnivQ (&/|list)
+                                                     (&/$SumT
+                                                      ;; lux;None
+                                                      &/$UnitT
+                                                      ;; lux;Some
+                                                      (&/$BoundT 1))))
+
+                            _ (&type/check (&/$UnivQ (&/|list)
+                                                     (&/$SumT
+                                                      ;; lux;Nil
+                                                      &/$UnitT
+                                                      ;; lux;Cons
+                                                      (&/$ProdT (&/$BoundT 1)
+                                                                (&/$AppT (&/$BoundT 0)
+                                                                         (&/$BoundT 1)))))
+                                           (&/$UnivQ (&/|list)
+                                                     (&/$SumT
+                                                      ;; lux;Nil
+                                                      &/$UnitT
+                                                      ;; lux;Cons
+                                                      (&/$ProdT (&/$BoundT 1)
+                                                                (&/$AppT (&/$BoundT 0)
+                                                                         (&/$BoundT 1))))))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(deftest check-ex-quantification
+  (|case (&/run-state (|do [_ (&type/check (&/$ExQ (&/|list)
+                                                   (&/$LambdaT &/$VoidT (&/$BoundT 1)))
+                                           (&/$ExQ (&/|list)
+                                                   (&/$LambdaT &/$VoidT (&/$BoundT 1))))
+
+                            _ (&type/check (&/$ExQ (&/|list)
+                                                   (&/$SumT
+                                                    ;; lux;None
+                                                    &/$UnitT
+                                                    ;; lux;Some
+                                                    (&/$BoundT 1)))
+                                           (&/$ExQ (&/|list)
+                                                   (&/$SumT
+                                                    ;; lux;None
+                                                    &/$UnitT
+                                                    ;; lux;Some
+                                                    (&/$BoundT 1))))
+
+                            _ (&type/check (&/$ExQ (&/|list)
+                                                   (&/$SumT
+                                                    ;; lux;Nil
+                                                    &/$UnitT
+                                                    ;; lux;Cons
+                                                    (&/$ProdT (&/$BoundT 1)
+                                                              (&/$AppT (&/$BoundT 0)
+                                                                       (&/$BoundT 1)))))
+                                           (&/$ExQ (&/|list)
+                                                   (&/$SumT
+                                                    ;; lux;Nil
+                                                    &/$UnitT
+                                                    ;; lux;Cons
+                                                    (&/$ProdT (&/$BoundT 1)
+                                                              (&/$AppT (&/$BoundT 0)
+                                                                       (&/$BoundT 1))))))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(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)))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(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)]
+                                    (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)]
+                                    (return nil))))
+
+                            _ (&type/with-var
+                                (fn [$var]
+                                  (|do [_ (&type/check (&/$HostT "java.lang.Boolean" &/$Nil) $var)
+                                        (&/$HostT "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)]
+                                    (return nil))))
+
+                            _ (&type/with-var
+                                (fn [$var1]
+                                  (&type/with-var
+                                    (fn [$var2]
+                                      (|do [_ (&type/check $var1 $var2)]
+                                        (return nil))))))
+
+                            _ (&type/with-var
+                                (fn [$var1]
+                                  (&type/with-var
+                                    (fn [$var2]
+                                      (|do [_ (&type/check $var2 $var1)]
+                                        (return nil))))))
+
+                            _ (&type/with-var
+                                (fn [$var1]
+                                  (&type/with-var
+                                    (fn [$var2]
+                                      (|do [_ (&type/check $var1 $var2)
+                                            _ (&type/check $var1 (&/$HostT "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))) "")]
+                                        (return nil))))))
+
+                            _ (&type/with-var
+                                (fn [$var1]
+                                  (&type/with-var
+                                    (fn [$var2]
+                                      (|do [_ (&type/check $var2 $var1)
+                                            _ (&type/check $var1 (&/$HostT "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))) "")]
+                                        (return nil))))))
+                            
+                            _ (&type/with-var
+                                (fn [$var1]
+                                  (&type/with-var
+                                    (fn [$var2]
+                                      (|do [_ (&type/check $var1 $var2)
+                                            _ (&type/check $var2 (&/$HostT "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))) "")]
+                                        (return nil))))))
+
+                            _ (&type/with-var
+                                (fn [$var1]
+                                  (&type/with-var
+                                    (fn [$var2]
+                                      (|do [_ (&type/check $var2 $var1)
+                                            _ (&type/check $var2 (&/$HostT "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))) "")]
+                                        (return nil))))))]
+                        (return nil))
+                      (&/init-state nil))
+    (&/$Right state nil)
+    (is true)
+    
+    (&/$Left error)
+    (is false error)
+    ))
+
+(comment
+  (run-all-tests)
+  )