- Removed analyse-2, as it was redundant.

- Fixed several bugs within lux.lux.
- Renamed "check'" to ":'" and "coerce" to ":!".

1 files changed, 412 insertions, 444 deletions

diff --git a/source/lux.lux b/source/lux.lux
index b03de7473..dee780e98 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -79,25 +79,25 @@
 ##   (| #None
 ##      (#Some a)))
 (def' Maybe
-  (check' Type
-          (#AllT [#Nil "Maybe" "a"
-                  (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
-                                     (#Cons [["lux;Some" (#BoundT "a")]
-                                             #Nil])]))])))
+  (: Type
+     (#AllT [#Nil "Maybe" "a"
+             (#VariantT (#Cons [["lux;None" (#TupleT #Nil)]
+                                (#Cons [["lux;Some" (#BoundT "a")]
+                                        #Nil])]))])))
 
 ## (deftype (Bindings k v)
 ##   (& #counter Int
 ##      #mappings (List (, k v))))
 (def' Bindings
-  (check' Type
-          (#AllT [#Nil "Bindings" "k"
-                  (#AllT [#Nil "" "v"
-                          (#RecordT (#Cons [["lux;counter" Int]
-                                            (#Cons [["lux;mappings" (#AppT [List
-                                                                            (#TupleT (#Cons [(#BoundT "k")
-                                                                                             (#Cons [(#BoundT "v")
-                                                                                                     #Nil])]))])]
-                                                    #Nil])]))])])))
+  (: Type
+     (#AllT [#Nil "Bindings" "k"
+             (#AllT [#Nil "" "v"
+                     (#RecordT (#Cons [["lux;counter" Int]
+                                       (#Cons [["lux;mappings" (#AppT [List
+                                                                       (#TupleT (#Cons [(#BoundT "k")
+                                                                                        (#Cons [(#BoundT "v")
+                                                                                                #Nil])]))])]
+                                               #Nil])]))])])))
 
 ## (deftype (Env k v)
 ##   (& #name Text
@@ -105,41 +105,41 @@
 ##      #locals  (Bindings k v)
 ##      #closure (Bindings k v)))
 (def' Env
-  (check' Type
-          (#AllT [#Nil "Env" "k"
-                  (#AllT [#Nil "" "v"
-                          (#RecordT (#Cons [["lux;name" Text]
-                                            (#Cons [["lux;inner-closures" Int]
-                                                    (#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")])
-                                                                                  (#BoundT "v")])]
-                                                            (#Cons [["lux;closure" (#AppT [(#AppT [Bindings (#BoundT "k")])
-                                                                                           (#BoundT "v")])]
-                                                                    #Nil])])])]))])])))
+  (: Type
+     (#AllT [#Nil "Env" "k"
+             (#AllT [#Nil "" "v"
+                     (#RecordT (#Cons [["lux;name" Text]
+                                       (#Cons [["lux;inner-closures" Int]
+                                               (#Cons [["lux;locals" (#AppT [(#AppT [Bindings (#BoundT "k")])
+                                                                             (#BoundT "v")])]
+                                                       (#Cons [["lux;closure" (#AppT [(#AppT [Bindings (#BoundT "k")])
+                                                                                      (#BoundT "v")])]
+                                                               #Nil])])])]))])])))
 
 ## (deftype Cursor
 ##   (, Text Int Int))
 (def' Cursor
-  (check' Type
-          (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])]))))
+  (: Type
+     (#TupleT (#Cons [Text (#Cons [Int (#Cons [Int #Nil])])]))))
 
 ## (deftype (Meta m v)
 ##   (| (#Meta (, m v))))
 (def' Meta
-  (check' Type
-          (#AllT [#Nil "Meta" "m"
-                  (#AllT [#Nil "" "v"
-                          (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
-                                                                          (#Cons [(#BoundT "v")
-                                                                                  #Nil])]))]
-                                             #Nil]))])])))
+  (: Type
+     (#AllT [#Nil "Meta" "m"
+             (#AllT [#Nil "" "v"
+                     (#VariantT (#Cons [["lux;Meta" (#TupleT (#Cons [(#BoundT "m")
+                                                                     (#Cons [(#BoundT "v")
+                                                                             #Nil])]))]
+                                        #Nil]))])])))
 
 ## (def' Reader
 ##   (List (Meta Cursor Text)))
 (def' Reader
-  (check' Type
-          (#AppT [List
-                  (#AppT [(#AppT [Meta Cursor])
-                          Text])])))
+  (: Type
+     (#AppT [List
+             (#AppT [(#AppT [Meta Cursor])
+                     Text])])))
 
 ## (deftype CompilerState
 ##   (& #source         (Maybe Reader)
@@ -152,36 +152,18 @@
 ##      #loader         (^ java.net.URLClassLoader)
 ##      #eval-ctor      Int))
 (def' CompilerState
-  (check' Type
-          (#RecordT (#Cons [["lux;source" (#AppT [Maybe Reader])]
-                            (#Cons [["lux;modules" (#AppT [List Any])]
-                                    (#Cons [["lux;module-aliases" (#AppT [List Any])]
-                                            (#Cons [["lux;global-env" (#AppT [Maybe (#AppT [(#AppT [Env Text]) Any])])]
-                                                    (#Cons [["lux;local-envs" (#AppT [List (#AppT [(#AppT [Env Text]) Any])])]
-                                                            (#Cons [["lux;types" (#AppT [(#AppT [Bindings Int]) Type])]
-                                                                    (#Cons [["lux;writer" (#DataT "org.objectweb.asm.ClassWriter")]
-                                                                            (#Cons [["lux;loader" (#DataT "java.lang.ClassLoader")]
-                                                                                    (#Cons [["lux;eval-ctor" Int]
-                                                                                            #Nil])])])])])])])])]))))
-
-## (deftype (Syntax' f)
-##   (f (| (#Bool Bool)
-##         (#Int Int)
-##         (#Real Real)
-##         (#Char Char)
-##         (#Text Text)
-##         (#Form (List (Syntax' f)))
-##         (#Tuple (List (Syntax' f)))
-##         (#Record (List (, Text (Syntax' f)))))))
-## (deftype #rec Syntax
-##   (Meta Cursor (| (#Bool Bool)
-##                   (#Int Int)
-##                   (#Real Real)
-##                   (#Char Char)
-##                   (#Text Text)
-##                   (#Form (List Syntax))
-##                   (#Tuple (List Syntax))
-##                   (#Record (List (, Text Syntax))))))
+  (: Type
+     (#RecordT (#Cons [["lux;source" (#AppT [Maybe Reader])]
+                       (#Cons [["lux;modules" (#AppT [List Any])]
+                               (#Cons [["lux;module-aliases" (#AppT [List Any])]
+                                       (#Cons [["lux;global-env" (#AppT [Maybe (#AppT [(#AppT [Env Text]) Any])])]
+                                               (#Cons [["lux;local-envs" (#AppT [List (#AppT [(#AppT [Env Text]) Any])])]
+                                                       (#Cons [["lux;types" (#AppT [(#AppT [Bindings Int]) Type])]
+                                                               (#Cons [["lux;writer" (#DataT "org.objectweb.asm.ClassWriter")]
+                                                                       (#Cons [["lux;loader" (#DataT "java.lang.ClassLoader")]
+                                                                               (#Cons [["lux;eval-ctor" Int]
+                                                                                       #Nil])])])])])])])])]))))
+
 ## (deftype (Syntax' w)
 ##   (| (#Bool Bool)
 ##      (#Int Int)
@@ -194,246 +176,217 @@
 ##      (#Tuple (List (w (Syntax' w))))
 ##      (#Record (List (, Text (w (Syntax' w)))))))
 (def' Syntax'
-  (check' Type
-          (case' (#AppT [(#BoundT "w")
-                         (#AppT [(#BoundT "Syntax'")
-                                 (#BoundT "w")])])
-                 Syntax'
-                 (case' (#AppT [List Syntax'])
-                        Syntax'List
-                        (case' (#TupleT (#Cons [Text (#Cons [Text #Nil])]))
-                               Ident
-                               (#AllT [#Nil "Syntax'" "w"
-                                       (#VariantT (#Cons [["lux;Bool" Bool]
-                                                          (#Cons [["lux;Int" Int]
-                                                                  (#Cons [["lux;Real" Real]
-                                                                          (#Cons [["lux;Char" Char]
-                                                                                  (#Cons [["lux;Text" Text]
-                                                                                          (#Cons [["lux;Symbol" Ident]
-                                                                                                  (#Cons [["lux;Tag" Ident]
-                                                                                                          (#Cons [["lux;Form" Syntax'List]
-                                                                                                                  (#Cons [["lux;Tuple" Syntax'List]
-                                                                                                                          (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax' #Nil])]))])]
-                                                                                                                                  #Nil])
-                                                                                                                          ])])])])])])])])])
-                                                  )])
-                               )))))
+  (: Type
+     (case' (#AppT [(#BoundT "w")
+                    (#AppT [(#BoundT "Syntax'")
+                            (#BoundT "w")])])
+            Syntax'
+            (case' (#AppT [List Syntax'])
+                   Syntax'List
+                   (case' (#TupleT (#Cons [Text (#Cons [Text #Nil])]))
+                          Ident
+                          (#AllT [#Nil "Syntax'" "w"
+                                  (#VariantT (#Cons [["lux;Bool" Bool]
+                                                     (#Cons [["lux;Int" Int]
+                                                             (#Cons [["lux;Real" Real]
+                                                                     (#Cons [["lux;Char" Char]
+                                                                             (#Cons [["lux;Text" Text]
+                                                                                     (#Cons [["lux;Symbol" Ident]
+                                                                                             (#Cons [["lux;Tag" Ident]
+                                                                                                     (#Cons [["lux;Form" Syntax'List]
+                                                                                                             (#Cons [["lux;Tuple" Syntax'List]
+                                                                                                                     (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax' #Nil])]))])]
+                                                                                                                             #Nil])
+                                                                                                                     ])])])])])])])])])
+                                             )])
+                          )))))
 
 ## (deftype Syntax
 ##   (Meta Cursor (Syntax' (Meta Cursor))))
 (def' Syntax
-  (check' Type
-          (case' (#AppT [Meta Cursor])
-                 w
-                 (#AppT [w (#AppT [Syntax' w])]))))
-
-## (def' Syntax
-##   (check' Type
-##           (case' (#AppT [(#BoundT "Syntax") (#BoundT "")])
-##                  Syntax
-##                  (case' (#AppT [List Syntax])
-##                         SyntaxList
-##                         (#AppT [(#AllT [#Nil "Syntax" ""
-##                                         (#AppT [(#AppT [Meta Cursor])
-##                                                 (#VariantT (#Cons [["lux;Bool" Bool]
-##                                                                    (#Cons [["lux;Int" Int]
-##                                                                            (#Cons [["lux;Real" Real]
-##                                                                                    (#Cons [["lux;Char" Char]
-##                                                                                            (#Cons [["lux;Text" Text]
-##                                                                                                    (#Cons [["lux;Form" SyntaxList]
-##                                                                                                            (#Cons [["lux;Tuple" SyntaxList]
-##                                                                                                                    (#Cons [["lux;Record" (#AppT [List (#TupleT (#Cons [Text (#Cons [Syntax #Nil])]))])]
-##                                                                                                                            #Nil])])])])])])])]))])])
-##                                 #NothingT])))))
+  (: Type
+     (case' (#AppT [Meta Cursor])
+            w
+            (#AppT [w (#AppT [Syntax' w])]))))
 
 ## (deftype (Either l r)
 ##   (| (#Left l)
 ##      (#Right r)))
 (def' Either
-  (check' Type
-          (#AllT [#Nil "_" "l"
-                  (#AllT [#Nil "" "r"
-                          (#VariantT (#Cons [["lux;Left" (#BoundT "l")]
-                                             (#Cons [["lux;Right" (#BoundT "r")]
-                                                     #Nil])]))])])))
-
-## (deftype MacroOutput
-##   (Either Text [CompilerState (List Syntax)]))
-## (def' MacroOutput
-##   (check' Type
-##           (case' (#AppT [List Syntax])
-##                  SyntaxList
-##                  (#AppT [(#AppT [Either Text])
-##                          (#TupleT (#Cons [CompilerState
-##                                           (#Cons [SyntaxList #Nil])]))]))))
+  (: Type
+     (#AllT [#Nil "_" "l"
+             (#AllT [#Nil "" "r"
+                     (#VariantT (#Cons [["lux;Left" (#BoundT "l")]
+                                        (#Cons [["lux;Right" (#BoundT "r")]
+                                                #Nil])]))])])))
 
 ## (deftype Macro
 ##   (-> (List Syntax) CompilerState
 ##       (Either Text [CompilerState (List Syntax)])))
 (def' Macro
-  (check' Type
-          (case' (#AppT [List Syntax])
-                 SyntaxList
-                 (#LambdaT [SyntaxList
-                            (#LambdaT [CompilerState
-                                       (#AppT [(#AppT [Either Text])
-                                               (#TupleT (#Cons [CompilerState
-                                                                (#Cons [SyntaxList
-                                                                        #Nil])]))])])]))))
+  (: Type
+     (case' (#AppT [List Syntax])
+            SyntaxList
+            (#LambdaT [SyntaxList
+                       (#LambdaT [CompilerState
+                                  (#AppT [(#AppT [Either Text])
+                                          (#TupleT (#Cons [CompilerState
+                                                           (#Cons [SyntaxList
+                                                                   #Nil])]))])])]))))
 
 ## Base functions & macros
 ## (def (_meta data)
 ##   (-> (Syntax' (Meta Cursor)) Syntax)
 ##   (#Meta [["" -1 -1] data]))
 (def' _meta
-  (check' (#LambdaT [(#AppT [Syntax'
-                             (#AppT [Meta Cursor])])
-                     Syntax])
-          (lambda' _ data
-                   (#Meta [["" -1 -1] data]))))
+  (: (#LambdaT [(#AppT [Syntax'
+                        (#AppT [Meta Cursor])])
+                Syntax])
+     (lambda' _ data
+              (#Meta [["" -1 -1] data]))))
 
 ## (def (return' x)
 ##   (-> SyntaxList CompilerState
 ##       (Either Text (, CompilerState SyntaxList)))
 ##   ...)
 (def' return'
-  (check' (case' (#AppT [List Syntax])
-                 SyntaxList
-                 (#LambdaT [SyntaxList
-                            (#LambdaT [CompilerState
-                                       (#AppT [(#AppT [Either Text])
-                                               (#TupleT (#Cons [CompilerState
-                                                                (#Cons [SyntaxList
-                                                                        #Nil])]))])])]))
-          (lambda' _ val
-                   (lambda' _ state
-                            (#Right [state val])))))
+  (: (case' (#AppT [List Syntax])
+            SyntaxList
+            (#LambdaT [SyntaxList
+                       (#LambdaT [CompilerState
+                                  (#AppT [(#AppT [Either Text])
+                                          (#TupleT (#Cons [CompilerState
+                                                           (#Cons [SyntaxList
+                                                                   #Nil])]))])])]))
+     (lambda' _ val
+              (lambda' _ state
+                       (#Right [state val])))))
 
 ## (def (fail' msg)
 ##   (-> Text CompilerState
 ##       (Either Text (, CompilerState SyntaxList)))
 ##   ...)
 (def' fail'
-  (check' (case' (#AppT [List Syntax])
-                 SyntaxList
-                 (#LambdaT [Text
-                            (#LambdaT [CompilerState
-                                       (#AppT [(#AppT [Either Text])
-                                               (#TupleT (#Cons [CompilerState
-                                                                (#Cons [SyntaxList
-                                                                        #Nil])]))])])]))
-          (lambda' _ msg
-                   (lambda' _ state
-                            (#Left msg)))))
+  (: (case' (#AppT [List Syntax])
+            SyntaxList
+            (#LambdaT [Text
+                       (#LambdaT [CompilerState
+                                  (#AppT [(#AppT [Either Text])
+                                          (#TupleT (#Cons [CompilerState
+                                                           (#Cons [SyntaxList
+                                                                   #Nil])]))])])]))
+     (lambda' _ msg
+              (lambda' _ state
+                       (#Left msg)))))
 
 ## (def' let'
-##   (check' Macro
+##   (: Macro
 ##           (lambda' _ tokens
 ##                    (case' tokens
 ##                           (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
 ##                           (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
 ##                                                                  (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
 ##                                            #Nil]))
-                          
+
 ##                           _
 ##                           (#Left "Wrong syntax for let'")))))
 (def' let'
-  (check' Macro
-          (lambda' _ tokens
-                   (case' tokens
-                          (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
-                          (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
-                                                                 (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
-                                           #Nil]))
-
-                          _
-                          (fail' "Wrong syntax for let'")))))
+  (: Macro
+     (lambda' _ tokens
+              (case' tokens
+                     (#Cons [lhs (#Cons [rhs (#Cons [body #Nil])])])
+                     (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "case'"]))
+                                                            (#Cons [rhs (#Cons [lhs (#Cons [body #Nil])])])])))
+                                      #Nil]))
+
+                     _
+                     (fail' "Wrong syntax for let'")))))
 (declare-macro' let')
 
 (def' lambda
-  (check' Macro
-          (lambda' _ tokens
-                   (case' tokens
-                          (#Cons [(#Meta [_ (#Tuple (#Cons [arg args']))]) (#Cons [body #Nil])])
-                          (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "lambda'"]))
-                                                                 (#Cons [(_meta (#Symbol ["" ""]))
-                                                                         (#Cons [arg
-                                                                                 (#Cons [(case' args'
-                                                                                                #Nil
-                                                                                                body
-
-                                                                                                _
-                                                                                                (_meta (#Form (#Cons [(_meta (#Symbol ["lux" "lambda"]))
-                                                                                                                      (#Cons [(_meta (#Tuple args'))
-                                                                                                                              (#Cons [body #Nil])])]))))
-                                                                                         #Nil])])])])))
-                                           #Nil]))
-
-                          (#Cons [(#Meta [_ (#Symbol self)]) (#Cons [(#Meta [_ (#Tuple (#Cons [arg args']))]) (#Cons [body #Nil])])])
-                          (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "lambda'"]))
-                                                                 (#Cons [(_meta (#Symbol self))
-                                                                         (#Cons [arg
-                                                                                 (#Cons [(case' args'
-                                                                                                #Nil
-                                                                                                body
-
-                                                                                                _
-                                                                                                (_meta (#Form (#Cons [(_meta (#Symbol ["lux" "lambda"]))
-                                                                                                                      (#Cons [(_meta (#Tuple args'))
-                                                                                                                              (#Cons [body #Nil])])]))))
-                                                                                         #Nil])])])])))
-                                           #Nil]))
-                          
-                          _
-                          (fail' "Wrong syntax for lambda")))))
+  (: Macro
+     (lambda' _ tokens
+              (case' tokens
+                     (#Cons [(#Meta [_ (#Tuple (#Cons [arg args']))]) (#Cons [body #Nil])])
+                     (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "lambda'"]))
+                                                            (#Cons [(_meta (#Symbol ["" ""]))
+                                                                    (#Cons [arg
+                                                                            (#Cons [(case' args'
+                                                                                           #Nil
+                                                                                           body
+
+                                                                                           _
+                                                                                           (_meta (#Form (#Cons [(_meta (#Symbol ["lux" "lambda"]))
+                                                                                                                 (#Cons [(_meta (#Tuple args'))
+                                                                                                                         (#Cons [body #Nil])])]))))
+                                                                                    #Nil])])])])))
+                                      #Nil]))
+
+                     (#Cons [(#Meta [_ (#Symbol self)]) (#Cons [(#Meta [_ (#Tuple (#Cons [arg args']))]) (#Cons [body #Nil])])])
+                     (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "lambda'"]))
+                                                            (#Cons [(_meta (#Symbol self))
+                                                                    (#Cons [arg
+                                                                            (#Cons [(case' args'
+                                                                                           #Nil
+                                                                                           body
+
+                                                                                           _
+                                                                                           (_meta (#Form (#Cons [(_meta (#Symbol ["lux" "lambda"]))
+                                                                                                                 (#Cons [(_meta (#Tuple args'))
+                                                                                                                         (#Cons [body #Nil])])]))))
+                                                                                    #Nil])])])])))
+                                      #Nil]))
+                     
+                     _
+                     (fail' "Wrong syntax for lambda")))))
 (declare-macro' lambda)
 
 (def' def
-  (check' Macro
-          (lambda [tokens]
-            (case' tokens
-                   (#Cons [(#Meta [_ (#Symbol name)]) (#Cons [body #Nil])])
-                   (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "def'"])) tokens])))
-                                    #Nil]))
-
-                   (#Cons [(#Meta [_ (#Form (#Cons [(#Meta [_ (#Symbol name)]) args]))])
-                           (#Cons [body #Nil])])
-                   (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "def'"]))
-                                                          (#Cons [(_meta (#Symbol name))
-                                                                  (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["lux" "lambda"]))
-                                                                                                (#Cons [(_meta (#Symbol name))
-                                                                                                        (#Cons [(_meta (#Tuple args))
-                                                                                                                (#Cons [body #Nil])])])])))
-                                                                          #Nil])])])))
-                                    #Nil]))
-
-                   (#Cons [(#Meta [_ (#Symbol name)]) (#Cons [type (#Cons [body #Nil])])])
-                   (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "def'"]))
-                                                          (#Cons [(_meta (#Symbol name))
-                                                                  (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "check'"]))
-                                                                                                (#Cons [type
-                                                                                                        (#Cons [body
-                                                                                                                #Nil])])])))
-                                                                          #Nil])])])))
-                                    #Nil]))
-
-                   (#Cons [(#Meta [_ (#Form (#Cons [(#Meta [_ (#Symbol name)]) args]))])
-                           (#Cons [type (#Cons [body #Nil])])])
-                   (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "def'"]))
-                                                          (#Cons [(_meta (#Symbol name))
-                                                                  (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "check'"]))
-                                                                                                (#Cons [type
-                                                                                                        (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["lux" "lambda"]))
-                                                                                                                                      (#Cons [(_meta (#Symbol name))
-                                                                                                                                              (#Cons [(_meta (#Tuple args))
-                                                                                                                                                      (#Cons [body #Nil])])])])))
-                                                                                                                #Nil])])])))
-                                                                          #Nil])])])))
-                                    #Nil]))
-
-                   _
-                   (fail' "Wrong syntax for def")
-                   ))))
+  (: Macro
+     (lambda [tokens]
+       (case' tokens
+              (#Cons [(#Meta [_ (#Symbol name)]) (#Cons [body #Nil])])
+              (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "def'"])) tokens])))
+                               #Nil]))
+
+              (#Cons [(#Meta [_ (#Form (#Cons [(#Meta [_ (#Symbol name)]) args]))])
+                      (#Cons [body #Nil])])
+              (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "def'"]))
+                                                     (#Cons [(_meta (#Symbol name))
+                                                             (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["lux" "lambda"]))
+                                                                                           (#Cons [(_meta (#Symbol name))
+                                                                                                   (#Cons [(_meta (#Tuple args))
+                                                                                                           (#Cons [body #Nil])])])])))
+                                                                     #Nil])])])))
+                               #Nil]))
+
+              (#Cons [(#Meta [_ (#Symbol name)]) (#Cons [type (#Cons [body #Nil])])])
+              (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "def'"]))
+                                                     (#Cons [(_meta (#Symbol name))
+                                                             (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" ":"]))
+                                                                                           (#Cons [type
+                                                                                                   (#Cons [body
+                                                                                                           #Nil])])])))
+                                                                     #Nil])])])))
+                               #Nil]))
+
+              (#Cons [(#Meta [_ (#Form (#Cons [(#Meta [_ (#Symbol name)]) args]))])
+                      (#Cons [type (#Cons [body #Nil])])])
+              (return' (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" "def'"]))
+                                                     (#Cons [(_meta (#Symbol name))
+                                                             (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["" ":"]))
+                                                                                           (#Cons [type
+                                                                                                   (#Cons [(_meta (#Form (#Cons [(_meta (#Symbol ["lux" "lambda"]))
+                                                                                                                                 (#Cons [(_meta (#Symbol name))
+                                                                                                                                         (#Cons [(_meta (#Tuple args))
+                                                                                                                                                 (#Cons [body #Nil])])])])))
+                                                                                                           #Nil])])])))
+                                                                     #Nil])])])))
+                               #Nil]))
+
+              _
+              (fail' "Wrong syntax for def")
+              ))))
 (declare-macro' def)
 
 (def (defmacro tokens)
@@ -552,19 +505,19 @@
 
 (def (reverse' list)
   (->' ($' List Syntax) ($' List Syntax))
-  (fold' (check' (->' ($' List Syntax) Syntax
-                      ($' List Syntax))
-                 (lambda [tail head]
-                   (#Cons [head tail])))
+  (fold' (: (->' ($' List Syntax) Syntax
+                 ($' List Syntax))
+            (lambda [tail head]
+              (#Cons [head tail])))
          #Nil
          list))
 
 (defmacro (list xs)
-  (return' (#Cons [(fold' (check' (->' Syntax Syntax Syntax)
-                                  (lambda [tail head]
-                                    (_meta (#Form (#Cons [(_meta (#Tag ["lux" "Cons"]))
-                                                          (#Cons [(_meta (#Tuple (#Cons [head (#Cons [tail #Nil])])))
-                                                                  #Nil])])))))
+  (return' (#Cons [(fold' (: (->' Syntax Syntax Syntax)
+                             (lambda [tail head]
+                               (_meta (#Form (#Cons [(_meta (#Tag ["lux" "Cons"]))
+                                                     (#Cons [(_meta (#Tuple (#Cons [head (#Cons [tail #Nil])])))
+                                                             #Nil])])))))
                           (_meta (#Tag ["lux" "Nil"]))
                           (reverse' xs))
                    #Nil])))
@@ -572,36 +525,130 @@
 (defmacro (list& xs)
   (case' (reverse' xs)
          (#Cons [last init])
-         (return' (list (fold' (check' (->' Syntax Syntax Syntax)
-                                       (lambda [tail head]
-                                         (_meta (#Form (list (_meta (#Tag ["lux" "Cons"]))
-                                                             (_meta (#Tuple (list head tail))))))))
+         (return' (list (fold' (: (->' Syntax Syntax Syntax)
+                                  (lambda [tail head]
+                                    (_meta (#Form (list (_meta (#Tag ["lux" "Cons"]))
+                                                        (_meta (#Tuple (list head tail))))))))
                                last
                                init)))
 
          _
          (fail' "Wrong syntax for list&")))
 
-## (def (as-pairs xs)
-##   (All [a]
-##        (-> (List a) (List [a a])))
-##   (case' xs
-##          (#Cons [x (#Cons [y xs'])])
-##          (#Cons [[x y] (as-pairs xs')])
+(def (as-pairs' xs)
+  (All' [a]
+        (->' ($' List (B' a)) ($' List (#TupleT (list (B' a) (B' a))))))
+  (case' xs
+         (#Cons [x (#Cons [y xs'])])
+         (list& [x y] (as-pairs' xs'))
 
-##          _
-##          #Nil))
+         _
+         #Nil))
 
-## (defmacro (let tokens state)
-##   (case' tokens
-##          (#Cons [(#Meta [_ (#Tuple bindings)]) (#Cons [body #Nil])])
-##          (let' output (fold (lambda [body binding]
-##                               (case' binding
-##                                      [label value]
-##                                      (_meta (#Form (list (_meta (#Symbol ["lux" "let'"])) label value body)))))
-##                             body
-##                             (reverse (as-pairs bindings)))
-##                (#Right [state (list output)]))))
+(defmacro (let tokens)
+  (case' tokens
+         (#Cons [(#Meta [_ (#Tuple bindings)]) (#Cons [body #Nil])])
+         (return' (list (fold' (: (->' Syntax (#TupleT (list Syntax Syntax))
+                                       Syntax)
+                                  (lambda [body binding]
+                                    (case' binding
+                                           [label value]
+                                           (_meta (#Form (list (_meta (#Symbol ["lux" "let'"])) label value body))))))
+                               body
+                               (fold' (: (->' ($' List (#TupleT (list Syntax Syntax))) (#TupleT (list Syntax Syntax))
+                                              ($' List (#TupleT (list Syntax Syntax))))
+                                         (lambda [tail head]
+                                           (#Cons [head tail])))
+                                      #Nil
+                                      (as-pairs' bindings)))))
+
+         _
+         (fail' "Wrong syntax for let")))
+
+(def (map' f xs)
+  (All' [a b]
+        (->' (->' (B' a) (B' b)) ($' List (B' a)) ($' List (B' b))))
+  (case' xs
+         #Nil
+         #Nil
+
+         (#Cons [x xs'])
+         (#Cons [(f x) (map' f xs')])))
+
+(def (wrap-meta content)
+  (->' ($' Syntax' ($' Meta Cursor)) Syntax)
+  (_meta (#Form (list (_meta (#Tag ["lux" "Meta"]))
+                      (_meta (#Tuple (list (_meta (#Tuple (list (_meta (#Text "")) (_meta (#Int -1)) (_meta (#Int -1)))))
+                                           (_meta content))))))))
+
+(def (untemplate-list tokens)
+  (->' ($' List Syntax) Syntax)
+  (case' tokens
+         #Nil
+         (_meta (#Tag ["lux" "Nil"]))
+
+         (#Cons [token tokens'])
+         (_meta (#Form (list (_meta (#Tag ["lux" "Cons"]))
+                             (_meta (#Tuple (list token (untemplate-list tokens')))))))))
+
+(def (untemplate token)
+  (->' Syntax Syntax)
+  (case' token
+         (#Meta [_ (#Bool value)])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Bool"])) (_meta (#Bool value)))))
+
+         (#Meta [_ (#Int value)])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Int"])) (_meta (#Int value)))))
+
+         (#Meta [_ (#Real value)])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Real"])) (_meta (#Real value)))))
+
+         (#Meta [_ (#Char value)])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Char"])) (_meta (#Char value)))))
+
+         (#Meta [_ (#Text value)])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Text"])) (_meta (#Text value)))))
+
+         (#Meta [_ (#Tag [module name])])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Tag"])) (_meta (#Tuple (list (_meta (#Text module)) (_meta (#Text name))))))))
+
+         (#Meta [_ (#Symbol [module name])])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Symbol"])) (_meta (#Tuple (list (_meta (#Text module)) (_meta (#Text name))))))))
+
+         (#Meta [_ (#Tuple elems)])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Tuple"])) (untemplate-list (map' untemplate elems)))))
+
+         (#Meta [_ (#Form (#Cons [(#Meta [_ (#Symbol ["" "~"])]) (#Cons [(#Meta [_ unquoted]) #Nil])]))])
+         (_meta unquoted)
+
+         (#Meta [_ (#Form elems)])
+         (wrap-meta (#Form (list (_meta (#Tag ["lux" "Form"])) (untemplate-list (map' untemplate elems)))))
+
+         (#Meta [_ (#Record fields)])
+         (wrap-meta (#Record (map' (: (->' (#TupleT (list Text Syntax)) (#TupleT (list Text Syntax)))
+                                      (lambda [kv]
+                                        (let [[k v] kv]
+                                          [k (untemplate v)])))
+                                   fields)))
+         ))
+
+(defmacro (` tokens)
+  (case' tokens
+         (#Cons [template #Nil])
+         (return' (list (untemplate template)))
+
+         _
+         (fail' "Wrong syntax for `")))
+
+(defmacro (if tokens)
+  (case' tokens
+         (#Cons [test (#Cons [then (#Cons [else #Nil])])])
+         (return' (list (` (case' (~ test)
+                                  true  (~ then)
+                                  false (~ else)))))
+
+         _
+         (fail' "Wrong syntax for if")))
 
 ## (def (print x)
 ##   (-> (^ java.lang.Object) [])
@@ -641,85 +688,11 @@
 ##        (-> (List (List a)) (List a)))
 ##   (fold ++ #Nil))
 
-## (def (map f xs)
-##   (All [a b]
-##        (-> (-> a b) (List a) (List b)))
-##   (case' xs
-##          #Nil
-##          #Nil
-
-##          (#Cons [x xs'])
-##          (#Cons [(f x) (map f xs')])))
-
 ## (def flat-map
 ##   (All [a b]
 ##        (-> (-> a (List b)) (List a) (List b)))
 ##   (. concat map))
 
-## (def (wrap-meta content)
-##   ...
-##   (_meta (#Form (list (_meta (#Tag ["lux" "Meta"]))
-##                       (_meta (#Tuple (list (_meta (#Tuple (list (_meta (#Form (list (_meta (#Tag ["lux" "Text"])) (_meta (#Text "")))))
-##                                                                 (_meta (#Form (list (_meta (#Tag ["lux" "Int"]))  (_meta (#Int -1)))))
-##                                                                 (_meta (#Form (list (_meta (#Tag ["lux" "Int"]))  (_meta (#Int -1))))))))
-##                                            (_meta content))))))))
-
-## (def (untemplate-list tokens)
-##   (-> (List Syntax) Syntax)
-##   (case' tokens
-##          #Nil
-##          (_meta (#Tag ["lux" "Nil"]))
-
-##          (#Cons [token tokens'])
-##          (_meta (#Form (list (_meta (#Tag ["lux" "Cons"]))
-##                              (_meta (#Tuple (list token (untemplate-list tokens')))))))))
-
-## (def (untemplate token)
-##   ...
-##   (case' token
-##          (#Meta [_ (#Bool value)])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Bool"])) (_meta (#Bool value)))))
-
-##          (#Meta [_ (#Int value)])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Int"])) (_meta (#Int value)))))
-
-##          (#Meta [_ (#Real value)])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Real"])) (_meta (#Real value)))))
-
-##          (#Meta [_ (#Char value)])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Char"])) (_meta (#Char value)))))
-
-##          (#Meta [_ (#Text value)])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Text"])) (_meta (#Text value)))))
-
-##          (#Meta [_ (#Tag [module name])])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Tag"])) (_meta (#Tuple (list (_meta (#Text module)) (_meta (#Text name))))))))
-
-##          (#Meta [_ (#Symbol [module name])])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Symbol"])) (_meta (#Tuple (list (_meta (#Text module)) (_meta (#Text name))))))))
-
-##          (#Meta [_ (#Tuple elems)])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Tuple"])) (untemplate-list (map untemplate elems)))))
-
-##          (#Meta [_ (#Form (#Cons [(#Meta [_ (#Symbol [_ "~"])]) (#Cons [(#Meta [_ unquoted]) #Nil])]))])
-##          (_meta unquoted)
-
-##          (#Meta [_ (#Form elems)])
-##          (wrap-meta (#Form (list (_meta (#Tag ["lux" "Form"])) (untemplate-list (map untemplate elems)))))
-##          ))
-
-(defmacro (` tokens)
-  (case' tokens
-         (#Cons [template #Nil])
-         (return' (list (untemplate template)))))
-
-(defmacro (if tokens)
-  (case' tokens
-         (#Cons [test (#Cons [then (#Cons [else #Nil])])])
-         (return' (list (` (case' (~ test)
-                                  true  (~ then)
-                                  false (~ else)))))))
-
 ## (def (filter p xs)
 ##   (All [a]
 ##        (-> (-> a Bool) (List a) (List a)))
@@ -927,14 +900,14 @@
 ##          #Nil true
 ##          _    false))
 
-## ## ## ## (do-template [<name> <op>]
-## ## ## ##              (def (<name> p xs)
-## ## ## ##                (case xs
-## ## ## ##                  #Nil true
-## ## ## ##                  (#Cons [x xs']) (<op> (p x) (<name> p xs'))))
+## ## (do-template [<name> <op>]
+## ##              (def (<name> p xs)
+## ##                (case xs
+## ##                  #Nil true
+## ##                  (#Cons [x xs']) (<op> (p x) (<name> p xs'))))
 
-## ## ## ##              [every? and]
-## ## ## ##              [any?   or])
+## ##              [every? and]
+## ##              [any?   or])
 
 ## (def (range from to)
 ##   (-> Int Int (List Int))
@@ -1022,11 +995,11 @@
 ##                (map (. apply (zip2 bindings-list)))
 ##                return))))
 
-## ## ## ## (do-template [<name> <offset>]
-## ## ## ##              (def <name> (int+ <offset>))
+## ## (do-template [<name> <offset>]
+## ##              (def <name> (int+ <offset>))
 
-## ## ## ##              [inc  1]
-## ## ## ##              [dec -1])
+## ##              [inc  1]
+## ##              [dec -1])
 
 ## (def (int= x y)
 ##   (-> Int Int Bool)
@@ -1222,8 +1195,6 @@
 ## ##          (return (flat-map (lambda [pattern] (list pattern body))
 ## ##                            patterns))))
 
-## ## (def null jvm-null)
-
 ## (defmacro (^ tokens)
 ##   (case' tokens
 ##          (#Cons [(#Meta [_ (#Symbol [_ class-name])]) #Nil])
@@ -1312,60 +1283,12 @@
 ##                                    (~ (replace-ident arg-name (` (#BoundT (~ (#Text name))))
 ##                                                      body)))))))))
 
-## (defmacro (Exists tokens)
-##   (case' tokens
-##          (#Cons [args (#Cons [body #Nil])])
-##          (return (list (` (All (~ args) (~ body)))))))
-
-## (def Any #AnyT)
-## (def Nothing #NothingT)
-## (def Bool (^ java.lang.Boolean))
-## (def Int (^ java.lang.Long))
-## (def Real (^ java.lang.Double))
-## (def Char (^ java.lang.Character))
-## (def Text (^ java.lang.String))
-
-## (deftype (List a)
-##   (| #Nil
-##      (#Cons (, a (List a)))))
-
-## (deftype #rec Type
-##   (| #AnyT
-##      #NothingT
-##      (#DataT Text)
-##      (#TupleT (List Type))
-##      (#VariantT (List (, Text Type)))
-##      (#RecordT (List (, Text Type)))
-##      (#LambdaT (, Type Type))
-##      (#BoundT Text)
-##      (#VarT Int)
-##      (#AllT (, (List (, Text Type)) Text Text Type))
-##      (#AppT (, Type Type))))
-
-## (deftype (Either l r)
-##   (| (#Left l)
-##      (#Right r)))
-
-## (deftype #rec Syntax
-##   (| (#Bool Bool)
-##      (#Int Int)
-##      (#Real Real)
-##      (#Char Char)
-##      (#Text Text)
-##      (#Form (List Syntax))
-##      (#Tuple (List Syntax))
-##      (#Record (List (, Text Syntax)))))
-
-## (deftype Macro
-##   (-> (List Syntax) CompilerState
-##       (Either Text (, CompilerState (List Syntax)))))
-
 ## (def (macro-expand syntax)
 ##   (-> Syntax (LuxStateM (List Syntax)))
 ##   (case' syntax
 ##          (#Form (#Cons [(#Symbol macro-name) args]))
 ##          (do [macro (get-macro macro-name)]
-##            ((coerce macro Macro) args))))
+##            ((:! macro Macro) args))))
 
 ## (defmacro (case tokens)
 ##   (case' tokens
@@ -1434,8 +1357,10 @@
 ##                        (: (~ def-body) (~ signature))))))))
 
 ## (defsig (Monad m)
-##   (: return (All [a] (-> a (m a))))
-##   (: bind (All [a b] (-> (-> a (m b)) (m a) (m b)))))
+##   (: (All [a] (-> a (m a)))
+##      return)
+##   (: (All [a b] (-> (-> a (m b)) (m a) (m b)))
+##      bind))
 
 ## (defstruct ListMonad (Monad List)
 ##   (def (return x)
@@ -1456,20 +1381,63 @@
 ##                   (= x y)))
 ##               (zip2 xs ys)))))
 
-## ## ## (def (with tokens)
-## ## ##   ...)
-
-## ## ## TODO: Full pattern-matching
-## ## ## TODO: Type-related macros
-## ## ## TODO: (Im|Ex)ports-related macros
-## ## ## TODO: Macro-related macros
-
-## ## ## (import "lux")
-## ## ## (module-alias "lux" "l")
-## ## ## (def-alias "lux;map" "map")
-
-## ## ## (def (require tokens)
-## ## ##   (case tokens
-## ## ##     ...))
-
-## ## ## (require lux #as l #refer [map])
+## ## (def (with tokens)
+## ##   ...)
+
+## ## (import "lux")
+## ## (module-alias "lux" "l")
+## ## (def-alias "lux;map" "map")
+
+## ## (def (require tokens)
+## ##   (case tokens
+## ##     ...))
+
+## ## (require lux #as l #refer [map])
+
+## (defsyntax #export (All [name (%? %name)] [args %args] body)
+##   (let [name' (case name
+##                 #None ""
+##                 (#Some name) name)
+##         arg-replacements (map (lambda [arg]
+##                                 [(#Symbol ["" arg]) (` (#Bound (~ arg)))])
+##                               args)
+##         args' (map (lambda [arg]
+##                      (#Symbol ["" arg]))
+##                    args)
+##         body' (replace-syntax arg-replacements body)]
+##     (return (list (` (#AllT [#Nil (~ name') (#Tuple (list (~@ args')))
+##                              (~ body')]))))))
+
+## (def (walk-syntax type)
+##   (case type
+##     (#Meta [_ (#Form (\list& op args))])
+##     (case op
+##       (#Meta [_ (#Symbol ident)])
+##       (do' [macro?? (find-macro ident)]
+##            (case macro??
+##              (#Some macro)
+##              (do' [expansion (macro args)]
+##                   (flat-map% walk-syntax expansion))
+
+##              #None
+##              (do' [flat-map% (map% walk-syntax args)]
+##                   (return' (list (fold (lambda [fun arg]
+##                                          (` (#AppT [(~ fun) (~ arg)])))
+##                                        op
+##                                        args))))))
+
+##       _
+##       (do' [flat-map% (map% walk-syntax args)]
+##            (return' (list (_meta (#Form (list op args')))))))
+
+##     _
+##     (return' (list type))))
+
+## (defsyntax #export (type type-syntax)
+##   (walk-syntax type-syntax))
+
+## (defsyntax #export (deftype [[name args] %usage] body)
+##   (return (list (` (def (~ name)
+##                      (: Type
+##                         (type (All [(~@ args)]
+##                                 (~ body)))))))))