- Changed the name of AllT (for-all type) to UnivQ (universal quantification).

- UnivQ no longer stores the environment as key-val pairs with Text names, but instead stores it as type-lists with variables accessed via an index through a (updated) BoundT.
- UnivQ no longer stores the name of the type-fun, not the name of the type-arg.

1 files changed, 456 insertions, 426 deletions

diff --git a/source/lux.lux b/source/lux.lux
index 815f95c69..d96b18fcb 100644
--- a/source/lux.lux
+++ b/source/lux.lux
@@ -45,12 +45,12 @@
 ##      (#Cons a (List a))))
 (_lux_def List
   (9 ["lux" "List"]
-     (7 (0) "lux;List" "a"
+     (7 (0)
         (1 (1 ## "lux;Nil"
             (2 (0))
             (1 ## "lux;Cons"
-             (2 (1 (4 "a")
-                   (1 (8 (4 "lux;List") (4 "a"))
+             (2 (1 (4 1)
+                   (1 (8 (4 0) (4 1))
                       (0))))
              (0)))))))
 (_lux_export List)
@@ -61,11 +61,11 @@
 ##      (1 a)))
 (_lux_def Maybe
   (9 ["lux" "Maybe"]
-     (7 (0) "lux;Maybe" "a"
+     (7 (0)
         (1 (1 ## "lux;None"
             (2 (0))
             (1 ## "lux;Some"
-             (4 "a")
+             (4 1)
              (0)))))))
 (_lux_export Maybe)
 (_lux_declare-tags [#None #Some] Maybe)
@@ -75,61 +75,59 @@
 ##      (#VariantT (List Type))
 ##      (#TupleT (List Type))
 ##      (#LambdaT Type Type)
-##      (#BoundT Text)
+##      (#BoundT Int)
 ##      (#VarT Int)
-##      (#AllT (List (, Text Type)) Text Text Type)
+##      (#UnivQ (List Type) Type)
 ##      (#AppT Type Type)
 ##      (#NamedT Ident Type)
 ## ))
 (_lux_def Type
   (9 ["lux" "Type"]
-     (_lux_case (8 (4 "Type") (4 "_"))
+     (_lux_case (8 (4 0) (4 1))
        Type
-       (_lux_case (8 List (2 (1 Text (1 Type (0)))))
-         TypeEnv
-         (_lux_case (8 List Type)
-           TypeList
-           (8 (7 (0) "Type" "_"
-                 (1 (1 ## "lux;DataT"
-                     Text
-                     (1 ## "lux;VariantT"
-                      TypeList
-                      (1 ## "lux;TupleT"
-                       TypeList
-                       (1 ## "lux;LambdaT"
-                        (2 (1 Type (1 Type (0))))
-                        (1 ## "lux;BoundT"
-                         Text
-                         (1 ## "lux;VarT"
-                          Int
-                          (1 ## "lux;ExT"
-                           Int
-                           (1 ## "lux;AllT"
-                            (2 (1 TypeEnv (1 Text (1 Text (1 Type (0))))))
-                            (1 ## "lux;AppT"
-                             (2 (1 Type (1 Type (0))))
-                             (1 ## "lux;NamedT"
-                              (2 (1 Ident (1 Type (0))))
-                              (0)))))))))))))
-              Void))))))
+       (_lux_case (8 List Type)
+         TypeList
+         (8 (7 (0)
+               (1 (1 ## "lux;DataT"
+                   Text
+                   (1 ## "lux;VariantT"
+                    TypeList
+                    (1 ## "lux;TupleT"
+                     TypeList
+                     (1 ## "lux;LambdaT"
+                      (2 (1 Type (1 Type (0))))
+                      (1 ## "lux;BoundT"
+                       Int
+                       (1 ## "lux;VarT"
+                        Int
+                        (1 ## "lux;ExT"
+                         Int
+                         (1 ## "lux;UnivQ"
+                          (2 (1 TypeList (1 Type (0))))
+                          (1 ## "lux;AppT"
+                           (2 (1 Type (1 Type (0))))
+                           (1 ## "lux;NamedT"
+                            (2 (1 Ident (1 Type (0))))
+                            (0)))))))))))))
+            Void)))))
 (_lux_export Type)
-(_lux_declare-tags [#DataT #VariantT #TupleT #LambdaT #BoundT #VarT #ExT #AllT #AppT #NamedT] Type)
+(_lux_declare-tags [#DataT #VariantT #TupleT #LambdaT #BoundT #VarT #ExT #UnivQ #AppT #NamedT] Type)
 
 ## (deftype (Bindings k v)
 ##   (& #counter Int
 ##      #mappings (List (, k v))))
 (_lux_def Bindings
   (#NamedT ["lux" "Bindings"]
-           (#AllT [#Nil "lux;Bindings" "k"
-                   (#AllT [#None "" "v"
+           (#UnivQ #Nil
+                   (#UnivQ #Nil
                            (#TupleT (#Cons ## "lux;counter"
                                      Int
                                      (#Cons ## "lux;mappings"
-                                      (#AppT [List
-                                              (#TupleT (#Cons [(#BoundT "k")
-                                                               (#Cons [(#BoundT "v")
-                                                                       #Nil])]))])
-                                      #Nil)))])])))
+                                      (#AppT List
+                                             (#TupleT (#Cons (#BoundT 3)
+                                                             (#Cons (#BoundT 1)
+                                                                    #Nil))))
+                                      #Nil)))))))
 (_lux_export Bindings)
 (_lux_declare-tags [#counter #mappings] Bindings)
 
@@ -140,19 +138,19 @@
 ##      #closure (Bindings k v)))
 (_lux_def Env
   (#NamedT ["lux" "Env"]
-           (#AllT #Nil "lux;Env" "k"
-                  (#AllT #None "" "v"
-                         (#TupleT (#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)))))))))
+           (#UnivQ #Nil
+                   (#UnivQ #Nil
+                           (#TupleT (#Cons ## "lux;name"
+                                     Text
+                                     (#Cons ## "lux;inner-closures"
+                                      Int
+                                      (#Cons ## "lux;locals"
+                                       (#AppT (#AppT Bindings (#BoundT 3))
+                                              (#BoundT 1))
+                                       (#Cons ## "lux;closure"
+                                        (#AppT (#AppT Bindings (#BoundT 3))
+                                               (#BoundT 1))
+                                        #Nil)))))))))
 (_lux_export Env)
 (_lux_declare-tags [#name #inner-closures #locals #closure] Env)
 
@@ -167,13 +165,13 @@
 ##   (| (#Meta m v)))
 (_lux_def Meta
   (#NamedT ["lux" "Meta"]
-           (#AllT #Nil "lux;Meta" "m"
-                  (#AllT #None "" "v"
-                         (#VariantT (#Cons ## "lux;Meta"
-                                     (#TupleT (#Cons (#BoundT "m")
-                                                     (#Cons (#BoundT "v")
-                                                            #Nil)))
-                                     #Nil))))))
+           (#UnivQ #Nil
+                   (#UnivQ #Nil
+                           (#VariantT (#Cons ## "lux;Meta"
+                                       (#TupleT (#Cons (#BoundT 3)
+                                                       (#Cons (#BoundT 1)
+                                                              #Nil)))
+                                       #Nil))))))
 (_lux_export Meta)
 (_lux_declare-tags [#Meta] Meta)
 
@@ -190,36 +188,36 @@
 ##      (#RecordS (List (, (w (AST' w)) (w (AST' w)))))))
 (_lux_def AST'
   (#NamedT ["lux" "AST'"]
-           (_lux_case (#AppT (#BoundT "w")
-                             (#AppT (#BoundT "lux;AST'")
-                                    (#BoundT "w")))
+           (_lux_case (#AppT (#BoundT 1)
+                             (#AppT (#BoundT 0)
+                                    (#BoundT 1)))
              AST
              (_lux_case (#AppT [List AST])
                ASTList
-               (#AllT #Nil "lux;AST'" "w"
-                      (#VariantT (#Cons ## "lux;BoolS"
-                                  Bool
-                                  (#Cons ## "lux;IntS"
-                                   Int
-                                   (#Cons ## "lux;RealS"
-                                    Real
-                                    (#Cons ## "lux;CharS"
-                                     Char
-                                     (#Cons ## "lux;TextS"
-                                      Text
-                                      (#Cons ## "lux;SymbolS"
-                                       Ident
-                                       (#Cons ## "lux;TagS"
+               (#UnivQ #Nil
+                       (#VariantT (#Cons ## "lux;BoolS"
+                                   Bool
+                                   (#Cons ## "lux;IntS"
+                                    Int
+                                    (#Cons ## "lux;RealS"
+                                     Real
+                                     (#Cons ## "lux;CharS"
+                                      Char
+                                      (#Cons ## "lux;TextS"
+                                       Text
+                                       (#Cons ## "lux;SymbolS"
                                         Ident
-                                        (#Cons ## "lux;FormS"
-                                         ASTList
-                                         (#Cons ## "lux;TupleS"
+                                        (#Cons ## "lux;TagS"
+                                         Ident
+                                         (#Cons ## "lux;FormS"
                                           ASTList
-                                          (#Cons ## "lux;RecordS"
-                                           (#AppT List (#TupleT (#Cons AST (#Cons AST #Nil))))
-                                           #Nil)
-                                          )))))))))
-                                 ))))))
+                                          (#Cons ## "lux;TupleS"
+                                           ASTList
+                                           (#Cons ## "lux;RecordS"
+                                            (#AppT List (#TupleT (#Cons AST (#Cons AST #Nil))))
+                                            #Nil)
+                                           )))))))))
+                                  ))))))
 (_lux_export AST')
 (_lux_declare-tags [#BoolS #IntS #RealS #CharS #TextS #SymbolS #TagS #FormS #TupleS #RecordS] AST')
 
@@ -239,26 +237,26 @@
 ##      (#Right r)))
 (_lux_def Either
   (#NamedT ["lux" "Either"]
-           (#AllT #Nil "lux;Either" "l"
-                  (#AllT #None "" "r"
-                         (#VariantT (#Cons ## "lux;Left"
-                                     (#BoundT "l")
-                                     (#Cons ## "lux;Right"
-                                      (#BoundT "r")
-                                      #Nil)))))))
+           (#UnivQ #Nil
+                   (#UnivQ #Nil
+                           (#VariantT (#Cons ## "lux;Left"
+                                       (#BoundT 3)
+                                       (#Cons ## "lux;Right"
+                                        (#BoundT 1)
+                                        #Nil)))))))
 (_lux_export Either)
 (_lux_declare-tags [#Left #Right] Either)
 
 ## (deftype (StateE s a)
 ##   (-> s (Either Text (, s a))))
 (_lux_def StateE
-  (#AllT [#Nil "lux;StateE" "s"
-          (#AllT [#None "" "a"
-                  (#LambdaT [(#BoundT "s")
-                             (#AppT [(#AppT [Either Text])
-                                     (#TupleT (#Cons [(#BoundT "s")
-                                                      (#Cons [(#BoundT "a")
-                                                              #Nil])]))])])])]))
+  (#UnivQ #Nil
+          (#UnivQ #Nil
+                  (#LambdaT (#BoundT 3)
+                            (#AppT (#AppT Either Text)
+                                   (#TupleT (#Cons (#BoundT 3)
+                                                   (#Cons (#BoundT 1)
+                                                          #Nil))))))))
 
 ## (deftype Source
 ##   (List (Meta Cursor Text)))
@@ -291,18 +289,16 @@
 ##      (#AliasD Ident)))
 (_lux_def DefData'
   (#NamedT ["lux" "DefData'"]
-           (#AllT [#Nil "lux;DefData'" ""
-                   (#VariantT (#Cons [## "lux;ValueD"
-                                      (#TupleT (#Cons [Type
-                                                       (#Cons [Unit
-                                                               #Nil])]))
-                                      (#Cons [## "lux;TypeD"
-                                              Type
-                                              (#Cons [## "lux;MacroD"
-                                                      (#BoundT "")
-                                                      (#Cons [## "lux;AliasD"
-                                                              Ident
-                                                              #Nil])])])]))])))
+           (#UnivQ #Nil
+                   (#VariantT (#Cons ## "lux;ValueD"
+                               (#TupleT (#Cons Type (#Cons Unit #Nil)))
+                               (#Cons ## "lux;TypeD"
+                                Type
+                                (#Cons ## "lux;MacroD"
+                                 (#BoundT 1)
+                                 (#Cons ## "lux;AliasD"
+                                  Ident
+                                  #Nil))))))))
 (_lux_export DefData')
 (_lux_declare-tags [#ValueD #TypeD #MacroD #AliasD] DefData')
 
@@ -328,34 +324,34 @@
 ##      ))
 (_lux_def Module
   (#NamedT ["lux" "Module"]
-           (#AllT [#Nil "lux;Module" "Compiler"
-                   (#TupleT (#Cons [## "lux;module-aliases"
-                                    (#AppT [List (#TupleT (#Cons [Text (#Cons [Text #Nil])]))])
-                                    (#Cons [## "lux;defs"
-                                            (#AppT [List (#TupleT (#Cons [Text
-                                                                          (#Cons [(#TupleT (#Cons [Bool (#Cons [(#AppT [DefData' (#LambdaT [ASTList
-                                                                                                                                            (#AppT [(#AppT [StateE (#BoundT "Compiler")])
-                                                                                                                                                    ASTList])])])
-                                                                                                                #Nil])]))
-                                                                                  #Nil])]))])
-                                            (#Cons [## "lux;imports"
-                                                    (#AppT [List Text])
-                                                    (#Cons [## "lux;tags"
-                                                            (#AppT [List
-                                                                    (#TupleT (#Cons Text
-                                                                                    (#Cons (#TupleT (#Cons Int
-                                                                                                           (#Cons (#AppT [List Ident])
-                                                                                                                  (#Cons Type
-                                                                                                                         #Nil))))
-                                                                                           #Nil)))])
-                                                            (#Cons [## "lux;types"
-                                                                    (#AppT [List
-                                                                            (#TupleT (#Cons Text
-                                                                                            (#Cons (#TupleT (#Cons (#AppT [List Ident])
-                                                                                                                   (#Cons Type
-                                                                                                                          #Nil)))
-                                                                                                   #Nil)))])
-                                                                    #Nil])])])])]))])))
+           (#UnivQ #Nil
+                   (#TupleT (#Cons ## "lux;module-aliases"
+                             (#AppT List (#TupleT (#Cons Text (#Cons Text #Nil))))
+                             (#Cons ## "lux;defs"
+                              (#AppT List (#TupleT (#Cons Text
+                                                          (#Cons (#TupleT (#Cons Bool (#Cons (#AppT DefData' (#LambdaT ASTList
+                                                                                                                       (#AppT (#AppT StateE (#BoundT 1))
+                                                                                                                              ASTList)))
+                                                                                             #Nil)))
+                                                                 #Nil))))
+                              (#Cons ## "lux;imports"
+                               (#AppT List Text)
+                               (#Cons ## "lux;tags"
+                                (#AppT List
+                                       (#TupleT (#Cons Text
+                                                       (#Cons (#TupleT (#Cons Int
+                                                                              (#Cons (#AppT List Ident)
+                                                                                     (#Cons Type
+                                                                                            #Nil))))
+                                                              #Nil))))
+                                (#Cons ## "lux;types"
+                                 (#AppT List
+                                        (#TupleT (#Cons Text
+                                                        (#Cons (#TupleT (#Cons (#AppT List Ident)
+                                                                               (#Cons Type
+                                                                                      #Nil)))
+                                                               #Nil))))
+                                 #Nil)))))))))
 (_lux_export Module)
 (_lux_declare-tags [#module-aliases #defs #imports #tags #types] Module)
 
@@ -372,30 +368,30 @@
 ## ))
 (_lux_def Compiler
   (#NamedT ["lux" "Compiler"]
-           (#AppT [(#AllT [#Nil "lux;Compiler" ""
-                           (#TupleT (#Cons [## "lux;source"
-                                            Source
-                                            (#Cons [## "lux;cursor"
-                                                    Cursor
-                                                    (#Cons [## "lux;modules"
-                                                            (#AppT [List (#TupleT (#Cons [Text
-                                                                                          (#Cons [(#AppT [Module (#AppT [(#BoundT "lux;Compiler") (#BoundT "")])])
-                                                                                                  #Nil])]))])
-                                                            (#Cons [## "lux;envs"
-                                                                    (#AppT [List (#AppT [(#AppT [Env Text])
-                                                                                         (#TupleT (#Cons [LuxVar (#Cons [Type #Nil])]))])])
-                                                                    (#Cons [## "lux;type-vars"
-                                                                            (#AppT [(#AppT [Bindings Int]) Type])
-                                                                            (#Cons [## "lux;expected"
-                                                                                    Type
-                                                                                    (#Cons [## "lux;seed"
-                                                                                            Int
-                                                                                            (#Cons [## "lux;eval?"
-                                                                                                    Bool
-                                                                                                    (#Cons [## "lux;host"
-                                                                                                            Host
-                                                                                                            #Nil])])])])])])])])]))])
-                   Void])))
+           (#AppT (#UnivQ #Nil
+                          (#TupleT (#Cons ## "lux;source"
+                                    Source
+                                    (#Cons ## "lux;cursor"
+                                     Cursor
+                                     (#Cons ## "lux;modules"
+                                      (#AppT List (#TupleT (#Cons Text
+                                                                  (#Cons (#AppT Module (#AppT (#BoundT 0) (#BoundT 1)))
+                                                                         #Nil))))
+                                      (#Cons ## "lux;envs"
+                                       (#AppT List (#AppT (#AppT Env Text)
+                                                          (#TupleT (#Cons LuxVar (#Cons Type #Nil)))))
+                                       (#Cons ## "lux;type-vars"
+                                        (#AppT (#AppT Bindings Int) Type)
+                                        (#Cons ## "lux;expected"
+                                         Type
+                                         (#Cons ## "lux;seed"
+                                          Int
+                                          (#Cons ## "lux;eval?"
+                                           Bool
+                                           (#Cons ## "lux;host"
+                                            Host
+                                            #Nil)))))))))))
+                  Void)))
 (_lux_export Compiler)
 (_lux_declare-tags [#source #cursor #modules #envs #type-vars #expected #seed #eval? #host] Compiler)
 
@@ -431,13 +427,13 @@
 ##         (Either Text (, Compiler a))))
 ##   ...)
 (_lux_def return
-  (_lux_: (#AllT #Nil "" "a"
-                 (#LambdaT (#BoundT "a")
-                           (#LambdaT Compiler
-                                     (#AppT (#AppT Either Text)
-                                            (#TupleT (#Cons Compiler
-                                                            (#Cons (#BoundT "a")
-                                                                   #Nil)))))))
+  (_lux_: (#UnivQ #Nil
+                  (#LambdaT (#BoundT 1)
+                            (#LambdaT Compiler
+                                      (#AppT (#AppT Either Text)
+                                             (#TupleT (#Cons Compiler
+                                                             (#Cons (#BoundT 1)
+                                                                    #Nil)))))))
           (_lux_lambda _ val
             (_lux_lambda _ state
               (#Right state val)))))
@@ -448,27 +444,42 @@
 ##         (Either Text (, Compiler a))))
 ##   ...)
 (_lux_def fail
-  (_lux_: (#AllT #Nil "" "a"
-                 (#LambdaT Text
-                           (#LambdaT Compiler
-                                     (#AppT (#AppT Either Text)
-                                            (#TupleT (#Cons Compiler
-                                                            (#Cons (#BoundT "a")
-                                                                   #Nil)))))))
+  (_lux_: (#UnivQ #Nil
+                  (#LambdaT Text
+                            (#LambdaT Compiler
+                                      (#AppT (#AppT Either Text)
+                                             (#TupleT (#Cons Compiler
+                                                             (#Cons (#BoundT 1)
+                                                                    #Nil)))))))
           (_lux_lambda _ msg
             (_lux_lambda _ state
               (#Left msg)))))
 
-(_lux_def text$
-  (_lux_: (#LambdaT Text AST)
-          (_lux_lambda _ text
-            (_meta (#TextS text)))))
+(_lux_def bool$
+  (_lux_: (#LambdaT Bool AST)
+          (_lux_lambda _ value
+            (_meta (#BoolS value)))))
 
 (_lux_def int$
   (_lux_: (#LambdaT Int AST)
           (_lux_lambda _ value
             (_meta (#IntS value)))))
 
+(_lux_def real$
+  (_lux_: (#LambdaT Real AST)
+          (_lux_lambda _ value
+            (_meta (#RealS value)))))
+
+(_lux_def char$
+  (_lux_: (#LambdaT Char AST)
+          (_lux_lambda _ value
+            (_meta (#CharS value)))))
+
+(_lux_def text$
+  (_lux_: (#LambdaT Text AST)
+          (_lux_lambda _ text
+            (_meta (#TextS text)))))
+
 (_lux_def symbol$
   (_lux_: (#LambdaT Ident AST)
           (_lux_lambda _ ident
@@ -542,7 +553,7 @@
                              #Nil))
               
               _
-              (fail "Wrong syntax for lambda")))))
+              (fail "Wrong syntax for lambda''")))))
 (_lux_declare-macro lambda'')
 
 (_lux_def def''
@@ -601,7 +612,7 @@
                                       #Nil]))
 
                       _
-                      (fail "Wrong syntax for def"))
+                      (fail "Wrong syntax for def''"))
                     )))
 (_lux_declare-macro def'')
 
@@ -638,82 +649,179 @@
 
 (defmacro (->' tokens)
   (_lux_case tokens
-    (#Cons [input (#Cons [output #Nil])])
-    (return (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "LambdaT"]))
-                                           (#Cons [(_meta (#TupleS (#Cons [input (#Cons [output #Nil])])))
-                                                   #Nil])])))
-                    #Nil]))
-
-    (#Cons [input (#Cons [output others])])
-    (return (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "LambdaT"]))
-                                           (#Cons [(_meta (#TupleS (#Cons [input
-                                                                           (#Cons [(_meta (#FormS (#Cons [(_meta (#SymbolS ["lux" "->'"]))
-                                                                                                          (#Cons [output others])])))
-                                                                                   #Nil])])))
-                                                   #Nil])])))
-                    #Nil]))
+    (#Cons input (#Cons output #Nil))
+    (return (#Cons (_meta (#FormS (#Cons (tag$ ["lux" "LambdaT"])
+                                         (#Cons (_meta (#TupleS (#Cons input (#Cons output #Nil))))
+                                                #Nil))))
+                   #Nil))
+
+    (#Cons input (#Cons output others))
+    (return (#Cons (_meta (#FormS (#Cons (tag$ ["lux" "LambdaT"])
+                                         (#Cons (_meta (#TupleS (#Cons input
+                                                                       (#Cons (_meta (#FormS (#Cons (symbol$ ["lux" "->'"])
+                                                                                                    (#Cons output others))))
+                                                                              #Nil))))
+                                                #Nil))))
+                   #Nil))
 
     _
     (fail "Wrong syntax for ->'")))
 
-(defmacro (All' tokens)
+(defmacro ($' tokens)
   (_lux_case tokens
-    (#Cons [(#Meta [_ (#TupleS #Nil)])
-            (#Cons [body #Nil])])
-    (return (#Cons [body
-                    #Nil]))
-
-    (#Cons [(#Meta [_ (#TupleS (#Cons [(#Meta [_ (#SymbolS ["" arg-name])]) other-args]))])
-            (#Cons [body #Nil])])
-    (return (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "AllT"]))
-                                           (#Cons [(_meta (#TupleS (#Cons [(_meta (#TagS ["lux" "None"]))
-                                                                           (#Cons [(_meta (#TextS ""))
-                                                                                   (#Cons [(_meta (#TextS arg-name))
-                                                                                           (#Cons [(_meta (#FormS (#Cons [(_meta (#SymbolS ["lux" "All'"]))
-                                                                                                                          (#Cons [(_meta (#TupleS other-args))
-                                                                                                                                  (#Cons [body
-                                                                                                                                          #Nil])])])))
-                                                                                                   #Nil])])])])))
-                                                   #Nil])])))
-                    #Nil]))
+    (#Cons x #Nil)
+    (return tokens)
+
+    (#Cons x (#Cons y xs))
+    (return (#Cons (_meta (#FormS (#Cons (symbol$ ["lux" "$'"])
+                                         (#Cons (_meta (#FormS (#Cons (tag$ ["lux" "AppT"])
+                                                                      (#Cons x (#Cons y #Nil)))))
+                                                xs))))
+                   #Nil))
 
     _
-    (fail "Wrong syntax for All'")))
+    (fail "Wrong syntax for $'")))
 
-(defmacro (B' tokens)
-  (_lux_case tokens
-    (#Cons [(#Meta [_ (#SymbolS ["" bound-name])])
-            #Nil])
-    (return (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "BoundT"]))
-                                           (#Cons [(_meta (#TextS bound-name))
-                                                   #Nil])])))
-                    #Nil]))
+(def'' (map f xs)
+  (#UnivQ #Nil
+          (#UnivQ #Nil
+                  (->' (->' (#BoundT 3) (#BoundT 1)) ($' List (#BoundT 3)) ($' List (#BoundT 1)))))
+  (_lux_case xs
+    #Nil
+    #Nil
+
+    (#Cons x xs')
+    (#Cons (f x) (map f xs'))))
+
+(def'' RepEnv
+  Type
+  ($' List (#TupleT (#Cons Text (#Cons AST #Nil)))))
+
+(def'' (make-env xs ys)
+  (->' ($' List Text) ($' List AST) RepEnv)
+  (_lux_case (_lux_: (#TupleT (#Cons ($' List Text) (#Cons ($' List AST) #Nil)))
+                     [xs ys])
+    [(#Cons x xs') (#Cons y ys')]
+    (#Cons [x y] (make-env xs' ys'))
 
     _
-    (fail "Wrong syntax for B'")))
+    #Nil))
 
-(defmacro ($' tokens)
-  (_lux_case tokens
-    (#Cons [x #Nil])
-    (return tokens)
+(def'' (text:= x y)
+  (->' Text Text Bool)
+  (_jvm_invokevirtual "java.lang.Object" "equals" ["java.lang.Object"]
+                      x [y]))
+
+(def'' (get-rep key env)
+  (->' Text RepEnv ($' Maybe AST))
+  (_lux_case env
+    #Nil
+    #None
+
+    (#Cons [k v] env')
+    (_lux_case (text:= k key)
+      true
+      (#Some v)
+
+      false
+      (get-rep key env'))))
+
+(def'' (replace-syntax reps syntax)
+  (->' RepEnv AST AST)
+  (_lux_case syntax
+    (#Meta _ (#SymbolS "" name))
+    (_lux_case (get-rep name reps)
+      (#Some replacement)
+      replacement
+
+      #None
+      syntax)
+
+    (#Meta _ (#FormS parts))
+    (#Meta _ (#FormS (map (replace-syntax reps) parts)))
 
-    (#Cons [x (#Cons [y xs])])
-    (return (#Cons [(_meta (#FormS (#Cons [(_meta (#SymbolS ["lux" "$'"]))
-                                           (#Cons [(_meta (#FormS (#Cons [(_meta (#TagS ["lux" "AppT"]))
-                                                                          (#Cons [(_meta (#TupleS (#Cons [x (#Cons [y #Nil])])))
-                                                                                  #Nil])])))
-                                                   xs])])))
-                    #Nil]))
+    (#Meta _ (#TupleS members))
+    (#Meta _ (#TupleS (map (replace-syntax reps) members)))
 
+    (#Meta _ (#RecordS slots))
+    (#Meta _ (#RecordS (map (_lux_: (->' (#TupleT (#Cons AST (#Cons AST #Nil))) (#TupleT (#Cons AST (#Cons AST #Nil))))
+                                    (lambda'' [slot]
+                                              (_lux_case slot
+                                                [k v]
+                                                [(replace-syntax reps k) (replace-syntax reps v)])))
+                            slots)))
+    
     _
-    (fail "Wrong syntax for $'")))
+    syntax)
+  )
+
+(def'' (update-bounds ast)
+  (->' AST AST)
+  (_lux_case ast
+    (#Meta _ (#BoolS value))
+    (bool$ value)
+
+    (#Meta _ (#IntS value))
+    (int$ value)
+
+    (#Meta _ (#RealS value))
+    (real$ value)
+
+    (#Meta _ (#CharS value))
+    (char$ value)
+
+    (#Meta _ (#TextS value))
+    (text$ value)
+
+    (#Meta _ (#SymbolS value))
+    (symbol$ value)
+
+    (#Meta _ (#TagS value))
+    (tag$ value)
+
+    (#Meta _ (#TupleS members))
+    (tuple$ (map update-bounds members))
+
+    (#Meta _ (#RecordS pairs))
+    (record$ (map (_lux_: (->' (#TupleT (#Cons AST (#Cons AST #Nil))) (#TupleT (#Cons AST (#Cons AST #Nil))))
+                          (lambda'' [pair]
+                               (let'' [name val] pair
+                                      [name (update-bounds val)])))
+                  pairs))
+
+    (#Meta _ (#FormS (#Cons (#Meta _ (#TagS "lux" "BoundT")) (#Cons (#Meta _ (#IntS idx)) #Nil))))
+    (form$ (#Cons (tag$ ["lux" "BoundT"]) (#Cons (int$ (_jvm_ladd 2 idx)) #Nil)))
+
+    (#Meta _ (#FormS members))
+    (form$ (map update-bounds members)))
+  )
+
+(defmacro (All' tokens)
+  (_lux_case tokens
+    (#Cons (#Meta _ (#TupleS (#Cons (#Meta _ (#SymbolS "" arg-name)) other-args)))
+           (#Cons body #Nil))
+    (let'' bound-var (_meta (#FormS (#Cons (tag$ ["lux" "BoundT"]) (#Cons (int$ 1) #Nil))))
+           (let'' body' (replace-syntax (#Cons [arg-name bound-var] #Nil)
+                                        (update-bounds body))
+                  (return (#Cons (_meta (#FormS (#Cons (tag$ ["lux" "UnivQ"])
+                                                       (#Cons (tag$ ["lux" "Nil"])
+                                                              (#Cons (_lux_case other-args
+                                                                       #Nil
+                                                                       body'
+
+                                                                       _
+                                                                       (_meta (#FormS (#Cons (symbol$ ["lux" "All'"])
+                                                                                             (#Cons (_meta (#TupleS other-args))
+                                                                                                    (#Cons body'
+                                                                                                           #Nil))))))
+                                                                     #Nil)))))
+                                 #Nil))))
+
+    _
+    (fail "Wrong syntax for All'")))
 
 (def'' (foldL f init xs)
-  (All' [a b]
-        (->' (->' (B' a) (B' b) (B' a))
-             (B' a)
-             ($' List (B' b))
-             (B' a))) 
+  (All' [a b] (->' (->' a b a) a ($' List b) a)) 
   (_lux_case xs
     #Nil
     init
@@ -722,8 +830,7 @@
     (foldL f (f init x) xs')))
 
 (def'' (reverse list)
-  (All' [a]
-        (->' ($' List (B' a)) ($' List (B' a))))
+  (All' [a] (->' ($' List a) ($' List a)))
   (foldL (lambda'' [tail head] (#Cons head tail))
          #Nil
          list))
@@ -822,8 +929,7 @@
     ))
 
 (def''' (as-pairs xs)
-  (All' [a]
-        (->' ($' List (B' a)) ($' List (#TupleT (list (B' a) (B' a))))))
+  (All' [a] (->' ($' List a) ($' List (#TupleT (list a a)))))
   (_lux_case xs
     (#Cons [x (#Cons [y xs'])])
     (#Cons [[x y] (as-pairs xs')])
@@ -846,24 +952,14 @@
     _
     (fail "Wrong syntax for let'")))
 
-(def''' (map f xs)
-  (All' [a b]
-        (->' (->' (B' a) (B' b)) ($' List (B' a)) ($' List (B' b))))
-  (_lux_case xs
-    #Nil
-    #Nil
-
-    (#Cons [x xs'])
-    (#Cons [(f x) (map f xs')])))
-
 (def''' (any? p xs)
   (All' [a]
-        (->' (->' (B' a) Bool) ($' List (B' a)) Bool))
+        (->' (->' a Bool) ($' List a) Bool))
   (_lux_case xs
     #Nil
     false
 
-    (#Cons [x xs'])
+    (#Cons x xs')
     (_lux_case (p x)
       true  true
       false (any? p xs'))))
@@ -894,17 +990,17 @@
                          (_meta (#TupleS (list token (untemplate-list tokens')))))))))
 
 (def''' #export (list:++ xs ys)
-  (All' [a] (->' ($' List (B' a)) ($' List (B' a)) ($' List (B' a))))
+  (All' [a] (->' ($' List a) ($' List a) ($' List a)))
   (_lux_case xs
-    (#Cons [x xs'])
-    (#Cons [x (list:++ xs' ys)])
+    (#Cons x xs')
+    (#Cons x (list:++ xs' ys))
 
     #Nil
     ys))
 
 (defmacro #export ($ tokens)
   (_lux_case tokens
-    (#Cons [op (#Cons [init args])])
+    (#Cons op (#Cons init args))
     (return (list (foldL (lambda' [a1 a2] (form$ (list op a1 a2)))
                          init
                          args)))
@@ -1044,7 +1140,7 @@
 (def''' #export Lux
   Type
   (All' [a]
-        (->' Compiler ($' Either Text (#TupleT (list Compiler (B' a)))))))
+        (->' Compiler ($' Either Text (#TupleT (list Compiler a))))))
 
 ## (defsig (Monad m)
 ##   (: (All [a] (-> a (m a)))
@@ -1055,40 +1151,40 @@
   Type
   (#NamedT ["lux" "Monad"]
            (All' [m]
-                 (#TupleT (list (All' [a] (->' (B' a) ($' (B' m) (B' a))))
-                                (All' [a b] (->' (->' (B' a) ($' (B' m) (B' b)))
-                                                 ($' (B' m) (B' a))
-                                                 ($' (B' m) (B' b)))))))))
+                 (#TupleT (list (All' [a] (->' a ($' m a)))
+                                (All' [a b] (->' (->' a ($' m b))
+                                                 ($' m a)
+                                                 ($' m b))))))))
 (_lux_declare-tags [#return #bind] Monad)
 
 (def''' Maybe/Monad
   ($' Monad Maybe)
   {#return
    (lambda' return [x]
-       (#Some x))
+            (#Some x))
    
    #bind
    (lambda' [f ma]
-       (_lux_case ma
-         #None     #None
-         (#Some a) (f a)))})
+            (_lux_case ma
+              #None     #None
+              (#Some a) (f a)))})
 
 (def''' Lux/Monad
   ($' Monad Lux)
   {#return
    (lambda' [x]
-       (lambda' [state]
-           (#Right state x)))
+            (lambda' [state]
+                     (#Right state x)))
    
    #bind
    (lambda' [f ma]
-       (lambda' [state]
-           (_lux_case (ma state)
-             (#Left msg)
-             (#Left msg)
+            (lambda' [state]
+                     (_lux_case (ma state)
+                       (#Left msg)
+                       (#Left msg)
 
-             (#Right state' a)
-             (f a state'))))})
+                       (#Right state' a)
+                       (f a state'))))})
 
 (defmacro #export (^ tokens)
   (_lux_case tokens
@@ -1116,16 +1212,16 @@
     (#Cons monad (#Cons (#Meta _ (#TupleS bindings)) (#Cons body #Nil)))
     (let' [body' (foldL (_lux_: (-> AST (, AST AST) AST)
                                 (lambda' [body' binding]
-                                    (let' [[var value] binding]
-                                          (_lux_case var
-                                            (#Meta _ (#TagS "" "let"))
-                                            (`' (;let' (~ value) (~ body')))
-
-                                            _
-                                            (`' (bind (_lux_lambda (~ (symbol$ ["" ""]))
-                                                        (~ var)
-                                                        (~ body'))
-                                                      (~ value)))))))
+                                         (let' [[var value] binding]
+                                               (_lux_case var
+                                                 (#Meta _ (#TagS "" "let"))
+                                                 (`' (;let' (~ value) (~ body')))
+
+                                                 _
+                                                 (`' (bind (_lux_lambda (~ (symbol$ ["" ""]))
+                                                             (~ var)
+                                                             (~ body'))
+                                                           (~ value)))))))
                         body
                         (reverse (as-pairs bindings)))]
           (return (list (`' (_lux_case (~ monad)
@@ -1139,10 +1235,10 @@
   ## (All [m a b]
   ##   (-> (Monad m) (-> a (m b)) (List a) (m (List b))))
   (All' [m a b]
-        (-> ($' Monad (B' m))
-            (-> (B' a) ($' (B' m) (B' b)))
-            ($' List (B' a))
-            ($' (B' m) ($' List (B' b)))))
+        (-> ($' Monad m)
+            (-> a ($' m b))
+            ($' List a)
+            ($' m ($' List b))))
   (let' [{#;return wrap #;bind _} m]
         (_lux_case xs
           #Nil
@@ -1157,14 +1253,14 @@
 
 (def''' (. f g)
   (All' [a b c]
-        (-> (-> (B' b) (B' c)) (-> (B' a) (B' b)) (-> (B' a) (B' c))))
+        (-> (-> b c) (-> a b) (-> a c)))
   (lambda' [x]
            (f (g x))))
 
 (def''' (get-ident x)
   (-> AST ($' Maybe Ident))
   (_lux_case x
-    (#Meta [_ (#SymbolS sname)])
+    (#Meta _ (#SymbolS sname))
     (#Some sname)
 
     _
@@ -1173,7 +1269,7 @@
 (def''' (get-name x)
   (-> AST ($' Maybe Text))
   (_lux_case x
-    (#Meta [_ (#SymbolS ["" sname])])
+    (#Meta _ (#SymbolS "" sname))
     (#Some sname)
 
     _
@@ -1182,46 +1278,16 @@
 (def''' (tuple->list tuple)
   (-> AST ($' Maybe ($' List AST)))
   (_lux_case tuple
-    (#Meta [_ (#TupleS members)])
+    (#Meta _ (#TupleS members))
     (#Some members)
 
     _
     #None))
 
-(def''' RepEnv
-  Type
-  ($' List (, Text AST)))
-
-(def''' (make-env xs ys)
-  (-> ($' List Text) ($' List AST) RepEnv)
-  (_lux_case (_lux_: (, ($' List Text) ($' List AST))
-                     [xs ys])
-    [(#Cons [x xs']) (#Cons [y ys'])]
-    (#Cons [[x y] (make-env xs' ys')])
-
-    _
-    #Nil))
-
-(def''' (text:= x y)
-  (-> Text Text Bool)
-  (_jvm_invokevirtual "java.lang.Object" "equals" ["java.lang.Object"]
-                      x [y]))
-
-(def''' (get-rep key env)
-  (-> Text RepEnv ($' Maybe AST))
-  (_lux_case env
-    #Nil
-    #None
-
-    (#Cons [[k v] env'])
-    (if (text:= k key)
-      (#Some v)
-      (get-rep key env'))))
-
 (def''' (apply-template env template)
   (-> RepEnv AST AST)
   (_lux_case template
-    (#Meta [_ (#SymbolS ["" sname])])
+    (#Meta _ (#SymbolS "" sname))
     (_lux_case (get-rep sname env)
       (#Some subst)
       subst
@@ -1229,13 +1295,13 @@
       _
       template)
 
-    (#Meta [_ (#TupleS elems)])
+    (#Meta _ (#TupleS elems))
     (tuple$ (map (apply-template env) elems))
 
-    (#Meta [_ (#FormS elems)])
+    (#Meta _ (#FormS elems))
     (form$ (map (apply-template env) elems))
 
-    (#Meta [_ (#RecordS members)])
+    (#Meta _ (#RecordS members))
     (record$ (map (_lux_: (-> (, AST AST) (, AST AST))
                           (lambda' [kv]
                                    (let' [[slot value] kv]
@@ -1247,7 +1313,7 @@
 
 (def''' (join-map f xs)
   (All' [a b]
-        (-> (-> (B' a) ($' List (B' b))) ($' List (B' a)) ($' List (B' b))))
+        (-> (-> a ($' List b)) ($' List a) ($' List b)))
   (_lux_case xs
     #Nil
     #Nil
@@ -1339,63 +1405,33 @@
   (let' [[module name] ident]
         ($ text:++ module ";" name)))
 
-(def''' (replace-syntax reps syntax)
-  (-> RepEnv AST AST)
-  (_lux_case syntax
-    (#Meta [_ (#SymbolS ["" name])])
-    (_lux_case (get-rep name reps)
-      (#Some replacement)
-      replacement
-
-      #None
-      syntax)
-
-    (#Meta [_ (#FormS parts)])
-    (#Meta [_ (#FormS (map (replace-syntax reps) parts))])
-
-    (#Meta [_ (#TupleS members)])
-    (#Meta [_ (#TupleS (map (replace-syntax reps) members))])
-
-    (#Meta [_ (#RecordS slots)])
-    (#Meta [_ (#RecordS (map (_lux_: (-> (, AST AST) (, AST AST))
-                                     (lambda' [slot]
-                                              (let' [[k v] slot]
-                                                    [(replace-syntax reps k) (replace-syntax reps v)])))
-                             slots))])
-    
-    _
-    syntax)
-  )
+(def''' (make-bound idx)
+  (-> Int AST)
+  (`' (#;BoundT (~ (int$ idx)))))
 
 (defmacro #export (All tokens)
-  (let' [[self-ident tokens'] (_lux_: (, Text ASTList)
-                                      (_lux_case tokens
-                                        (#Cons [(#Meta [_ (#SymbolS ["" self-ident])]) tokens'])
-                                        [self-ident tokens']
-
-                                        _
-                                        ["" tokens]))]
-        (_lux_case tokens'
-          (#Cons [(#Meta [_ (#TupleS args)]) (#Cons [body #Nil])])
-          (_lux_case (map% Maybe/Monad get-name args)
-            (#Some idents)
-            (_lux_case idents
-              #Nil
-              (return (list body))
-              
-              (#Cons [harg targs])
-              (let' [replacements (map (_lux_: (-> Text (, Text AST))
-                                               (lambda' [ident] [ident (`' (#;BoundT (~ (text$ ident))))]))
-                                       (list& self-ident idents))
-                     body' (foldL (lambda' [body' arg']
-                                           (`' (#;AllT [#;None "" (~ (text$ arg')) (~ body')])))
-                                  (replace-syntax replacements body)
-                                  (reverse targs))]
-                    ## (#;Some #;Nil)
-                    (return (list (`' (#;AllT [#;None (~ (text$ self-ident)) (~ (text$ harg)) (~ body')]))))))
+  (let' [[self-name tokens] (_lux_: (, Text ASTList)
+                                    (_lux_case tokens
+                                      (#Cons (#Meta _ (#SymbolS "" self-name)) tokens)
+                                      [self-name tokens]
+
+                                      _
+                                      ["" tokens]))]
+        (_lux_case tokens
+          (#Cons (#Meta _ (#TupleS (#Cons harg targs))) (#Cons body #Nil))
+          (_lux_case (map% Maybe/Monad get-name (#Cons harg targs))
+            (#Some names)
+            (let' [body' (foldL (lambda' [body' name']
+                                         (`' (#;UnivQ #;Nil (~ (|> body'
+                                                                   (update-bounds)
+                                                                   (replace-syntax (list [name' (make-bound 1)])))))))
+                                (replace-syntax (list [self-name (make-bound -2)])
+                                                body)
+                                names)]
+                  (return (list body')))
             
             #None
-            (fail "'All' arguments must be symbols."))
+            (fail "\"All\" arguments must be symbols."))
           
           _
           (fail "Wrong syntax for All"))
@@ -2162,8 +2198,8 @@
     (#VarT id)
     ($ text:++ "⌈" (->text id) "⌋")
 
-    (#BoundT name)
-    name
+    (#BoundT idx)
+    (->text idx)
 
     (#ExT ?id)
     ($ text:++ "⟨" (->text ?id) "⟩")
@@ -2171,15 +2207,28 @@
     (#AppT ?lambda ?param)
     ($ text:++ "(" (type:show ?lambda) " " (type:show ?param) ")")
 
-    (#AllT ?env ?name ?arg ?body)
-    ($ text:++ "(All " ?name " [" ?arg "] " (type:show ?body) ")")
+    (#UnivQ ?env ?body)
+    ($ text:++ "(All " (type:show ?body) ")")
 
     (#NamedT name type)
     (ident->text name)
     ))
 
+(def (@ idx xs)
+  (All [a]
+    (-> Int (List a) (Maybe a)))
+  (case xs
+    #Nil
+    #None
+
+    (#Cons x xs')
+    (if (i= idx 0)
+      (#Some x)
+      (@ (i- idx 1) xs')
+      )))
+
 (def (beta-reduce env type)
-  (-> (List (, Text Type)) Type Type)
+  (-> (List Type) Type Type)
   (case type
     (#VariantT ?cases)
     (#VariantT (map (beta-reduce env) ?cases))
@@ -2190,10 +2239,10 @@
     (#AppT ?type-fn ?type-arg)
     (#AppT (beta-reduce env ?type-fn) (beta-reduce env ?type-arg))
 
-    (#AllT ?local-env ?local-name ?local-arg ?local-def)
+    (#UnivQ ?local-env ?local-def)
     (case ?local-env
       #Nil
-      (#AllT env ?local-name ?local-arg ?local-def)
+      (#UnivQ env ?local-def)
 
       _
       type)
@@ -2201,8 +2250,8 @@
     (#LambdaT ?input ?output)
     (#LambdaT (beta-reduce env ?input) (beta-reduce env ?output))
 
-    (#BoundT ?name)
-    (case (get ?name env)
+    (#BoundT idx)
+    (case (@ idx env)
       (#Some bound)
       bound
 
@@ -2219,11 +2268,8 @@
 (def (apply-type type-fn param)
   (-> Type Type (Maybe Type))
   (case type-fn
-    (#AllT env name arg body)
-    (#Some (beta-reduce (|> env
-                            (put name type-fn)
-                            (put arg param))
-                        body))
+    (#UnivQ env body)
+    (#Some (beta-reduce (list& type-fn param env) body))
 
     (#AppT F A)
     (do Maybe/Monad
@@ -2247,7 +2293,7 @@
       [output (apply-type fun arg)]
       (resolve-struct-type output))
 
-    (#AllT _ _ _ body)
+    (#UnivQ _ body)
     (resolve-struct-type body)
 
     (#NamedT name type)
@@ -2294,7 +2340,7 @@
     (#AppT fun arg)
     (resolve-type-tags fun)
 
-    (#AllT env name arg body)
+    (#UnivQ env body)
     (resolve-type-tags body)
     
     (#NamedT [module name] _)
@@ -2556,19 +2602,6 @@
       (#Left ($ text:++ "Unknown module: " module)))
     ))
 
-(def (@ idx xs)
-  (All [a]
-    (-> Int (List a) (Maybe a)))
-  (case xs
-    #Nil
-    #None
-
-    (#Cons x xs')
-    (if (i= idx 0)
-      (#Some x)
-      (@ (i- idx 1) xs')
-      )))
-
 (def (split-with' p ys xs)
   (All [a]
     (-> (-> a Bool) (List a) (List a) (, (List a) (List a))))
@@ -3139,8 +3172,8 @@
     (#LambdaT in out)
     (` (#;LambdaT (~ (type->syntax in)) (~ (type->syntax out))))
     
-    (#BoundT name)
-    (` (#;BoundT (~ (text$ name))))
+    (#BoundT idx)
+    (` (#;BoundT (~ (int$ idx))))
     
     (#VarT id)
     (` (#;VarT (~ (int$ id))))
@@ -3148,12 +3181,9 @@
     (#ExT id)
     (` (#;ExT (~ (int$ id))))
     
-    (#AllT env name arg type)
-    (let [env' (untemplate-list (map (: (-> (, Text Type) AST)
-                                        (lambda [[label type]]
-                                          (tuple$ (list (text$ label) (type->syntax type)))))
-                                     env))]
-      (` (#;AllT (~ env') (~ (text$ name)) (~ (text$ arg)) (~ (type->syntax type)))))
+    (#UnivQ env type)
+    (let [env' (untemplate-list (map type->syntax env))]
+      (` (#;UnivQ (~ env') (~ (type->syntax type)))))
     
     (#AppT fun arg)
     (` (#;AppT (~ (type->syntax fun)) (~ (type->syntax arg))))