Fixed directive extensions for Lux/Python.

25 files changed, 395 insertions, 218 deletions

diff --git a/stdlib/source/library/lux.lux b/stdlib/source/library/lux.lux
index 7ddfa427f..75575ebe4 100644
--- a/stdlib/source/library/lux.lux
+++ b/stdlib/source/library/lux.lux
@@ -3718,13 +3718,6 @@
                          cases)]
     output))
 
-(def: (on_either f x1 x2)
-  (All (_ a b)
-    (-> (-> a (Maybe b)) a a (Maybe b)))
-  (case (f x1)
-    {#None}   (f x2)
-    {#Some y} {#Some y}))
-
 (def: (in_env name state)
   (-> Text Lux (Maybe Type))
   (case state
@@ -3738,14 +3731,13 @@
                      [..#name _
                       ..#inner _
                       ..#locals [..#counter _ ..#mappings locals]
-                      ..#captured [..#counter _ ..#mappings closure]]
-                     (on_either (list#one (: (-> [Text [Type Any]] (Maybe Type))
-                                             (function (_ [bname [type _]])
-                                               (if (text#= name bname)
-                                                 {#Some type}
-                                                 {#None}))))
-                                (: (List [Text [Type Any]]) locals)
-                                (: (List [Text [Type Any]]) closure)))))
+                      ..#captured _]
+                     (list#one (: (-> [Text [Type Any]] (Maybe Type))
+                                  (function (_ [bname [type _]])
+                                    (if (text#= name bname)
+                                      {#Some type}
+                                      {#None})))
+                               locals))))
               scopes)))
 
 (def: (definition_type name state)
@@ -3839,24 +3831,25 @@
     [.let [[module name] full_name]
      current_module current_module_name]
     (function (_ compiler)
-      (let [temp (if (text#= "" module)
-                   (case (in_env name compiler)
-                     {#Some struct_type}
-                     {#Right [compiler struct_type]}
+      (let [temp (: (Either Text [Lux Type])
+                    (if (text#= "" module)
+                      (case (in_env name compiler)
+                        {#Some struct_type}
+                        {#Right [compiler struct_type]}
 
-                     _
-                     (case (definition_type [current_module name] compiler)
-                       {#Some struct_type}
-                       {#Right [compiler struct_type]}
+                        _
+                        (case (definition_type [current_module name] compiler)
+                          {#Some struct_type}
+                          {#Right [compiler struct_type]}
 
-                       _
-                       {#Left ($_ text#composite "Unknown var: " (symbol#encoded full_name))}))
-                   (case (definition_type full_name compiler)
-                     {#Some struct_type}
-                     {#Right [compiler struct_type]}
+                          _
+                          {#Left ($_ text#composite "Unknown var: " (symbol#encoded full_name))}))
+                      (case (definition_type full_name compiler)
+                        {#Some struct_type}
+                        {#Right [compiler struct_type]}
 
-                     _
-                     {#Left ($_ text#composite "Unknown var: " (symbol#encoded full_name))}))]
+                        _
+                        {#Left ($_ text#composite "Unknown var: " (symbol#encoded full_name))})))]
         (case temp
           {#Right [compiler {#Var type_id}]}
           (let [[..#info _ ..#source _ ..#current_module _ ..#modules _
@@ -4708,30 +4701,6 @@
     _
     (failure (..wrong_syntax_error [..prelude_module "symbol"]))))
 
-(def: (scope_type_vars state)
-  (Meta (List Nat))
-  (case state
-    [..#info info ..#source    source ..#current_module _   ..#modules modules
-     ..#scopes scopes ..#type_context types    ..#host    host
-     ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
-     ..#scope_type_vars scope_type_vars ..#eval _eval]
-    {#Right [state scope_type_vars]}))
-
-(macro: .public (:parameter tokens)
-  (case tokens
-    (^ (list [_ {#Nat idx}]))
-    (do meta_monad
-      [stvs ..scope_type_vars]
-      (case (..item idx (list#reversed stvs))
-        {#Some var_id}
-        (in (list (` {.#Ex (~ (nat$ var_id))})))
-
-        {#None}
-        (failure (text#composite "Indexed-type does not exist: " (nat#encoded idx)))))
-
-    _
-    (failure (..wrong_syntax_error (symbol ..$)))))
-
 (def: .public (same? reference sample)
   (All (_ a)
     (-> a a Bit))
@@ -4927,6 +4896,32 @@
       _
       (failure (..wrong_syntax_error (symbol ..for))))))
 
+... TODO: Delete "scope_type_vars" (including the #scope_type_vars Lux state) and ":parameter" ASAP.
+(for ["{old}" (as_is (def: (scope_type_vars state)
+                       (Meta (List Nat))
+                       (case state
+                         [..#info info ..#source    source ..#current_module _   ..#modules modules
+                          ..#scopes scopes ..#type_context types    ..#host    host
+                          ..#seed seed ..#expected  expected ..#location  location ..#extensions extensions
+                          ..#scope_type_vars scope_type_vars ..#eval _eval]
+                         {#Right [state scope_type_vars]}))
+
+                     (macro: .public (:parameter tokens)
+                       (case tokens
+                         (^ (list [_ {#Nat idx}]))
+                         (do meta_monad
+                           [stvs ..scope_type_vars]
+                           (case (..item idx (list#reversed stvs))
+                             {#Some var_id}
+                             (in (list (` {.#Ex (~ (nat$ var_id))})))
+
+                             {#None}
+                             (failure (text#composite "Indexed-type does not exist: " (nat#encoded idx)))))
+
+                         _
+                         (failure (..wrong_syntax_error (symbol ..$))))))]
+     (as_is))
+
 (macro: .public (using _imports)
   (do meta_monad
     [current_module ..current_module_name
diff --git a/stdlib/source/library/lux/abstract/enum.lux b/stdlib/source/library/lux/abstract/enum.lux
index 45026abc1..f136fc92d 100644
--- a/stdlib/source/library/lux/abstract/enum.lux
+++ b/stdlib/source/library/lux/abstract/enum.lux
@@ -1,8 +1,8 @@
 (.using
-  [library
-   [lux "*"]]
-  [//
-   ["[0]" order {"+" Order}]])
+ [library
+  [lux "*"]]
+ [//
+  ["[0]" order {"+" Order}]])
 
 (type: .public (Enum e)
   (Interface
@@ -12,14 +12,15 @@
 
 (def: .public (range enum from to)
   (All (_ a) (-> (Enum a) a a (List a)))
-  (let [(^open "[0]") enum]
+  (let [(^open "/#[0]") enum]
     (loop [end to
-           output {.#End}]
-      (cond (< end from)
-            (again (pred end) {.#Item end output})
+           output (`` (: (List (~~ (:of from)))
+                         {.#End}))]
+      (cond (/#< end from)
+            (again (/#pred end) {.#Item end output})
 
-            (< from end)
-            (again (succ end) {.#Item end output})
+            (/#< from end)
+            (again (/#succ end) {.#Item end output})
 
             ... (= end from)
             {.#Item end output}))))
diff --git a/stdlib/source/library/lux/control/lazy.lux b/stdlib/source/library/lux/control/lazy.lux
index 9e59da7dc..8d3c877d8 100644
--- a/stdlib/source/library/lux/control/lazy.lux
+++ b/stdlib/source/library/lux/control/lazy.lux
@@ -1,28 +1,33 @@
 (.using
-  [library
-   [lux "*"
-    [abstract
-     [functor {"+" Functor}]
-     [apply {"+" Apply}]
-     [monad {"+" Monad do}]
-     [equivalence {"+" Equivalence}]]
-    [control
-     ["[0]" io]
-     [parser
-      ["<[0]>" code]]
-     [concurrency
-      ["[0]" atom]]]
-    [macro {"+" with_symbols}
-     [syntax {"+" syntax:}]]
-    [type
-     abstract]]])
+ [library
+  [lux "*"
+   [abstract
+    [functor {"+" Functor}]
+    [apply {"+" Apply}]
+    [monad {"+" Monad do}]
+    [equivalence {"+" Equivalence}]]
+   [control
+    ["[0]" io]
+    [parser
+     ["<[0]>" code]]
+    [concurrency
+     ["[0]" atom]]]
+   [macro {"+" with_symbols}
+    [syntax {"+" syntax:}]]
+   [type {"+" :sharing}
+    abstract]]])
 
 (abstract: .public (Lazy a)
   (-> [] a)
 
   (def: (lazy' generator)
     (All (_ a) (-> (-> [] a) (Lazy a)))
-    (let [cache (atom.atom {.#None})]
+    (let [cache (atom.atom (:sharing [a]
+                                     (-> [] a)
+                                     generator
+
+                                     (Maybe a)
+                                     {.#None}))]
       (:abstraction (function (_ _)
                       (case (io.run! (atom.read! cache))
                         {.#Some value}
diff --git a/stdlib/source/library/lux/data/collection/array.lux b/stdlib/source/library/lux/data/collection/array.lux
index ea16cddfc..437c80bfa 100644
--- a/stdlib/source/library/lux/data/collection/array.lux
+++ b/stdlib/source/library/lux/data/collection/array.lux
@@ -275,10 +275,10 @@
   Nat
   (-- 0))
 
-(def: (list|-default array)
-  (All (_ a) (-> (Array a) (List a)))
+(def: (list|-default array empty)
+  (All (_ a) (-> (Array a) (List a) (List a)))
   (loop [idx (-- (size array))
-         output {.#End}]
+         output empty]
     (case idx
       (^ (static ..underflow))
       output
@@ -295,7 +295,8 @@
 (def: (list|+default default array)
   (All (_ a) (-> a (Array a) (List a)))
   (loop [idx (-- (size array))
-         output {.#End}]
+         output (`` (: (List (~~ (:of default)))
+                       {.#End}))]
     (case idx
       (^ (static ..underflow))
       output
@@ -312,7 +313,7 @@
     (list|+default default array)
     
     {.#None}
-    (list|-default array)))
+    (list|-default array {.#End})))
 
 (implementation: .public (equivalence (^open ",#[0]"))
   (All (_ a) (-> (Equivalence a) (Equivalence (Array a))))
diff --git a/stdlib/source/library/lux/data/collection/dictionary/ordered.lux b/stdlib/source/library/lux/data/collection/dictionary/ordered.lux
index 083ad161c..7437962f6 100644
--- a/stdlib/source/library/lux/data/collection/dictionary/ordered.lux
+++ b/stdlib/source/library/lux/data/collection/dictionary/ordered.lux
@@ -475,9 +475,6 @@
   (let [(^open "_#[0]") (value@ #&order dict)
         [?root found?] (loop [?root (value@ #root dict)]
                          (case ?root
-                           {.#None}
-                           [{.#None} #0]
-
                            {.#Some root}
                            (let [root_key (value@ #key root)
                                  root_val (value@ #value root)]
@@ -514,6 +511,9 @@
                                         #0])
                                      )))
                                ))
+
+                           {.#None}
+                           [{.#None} #0]
                            ))]
     (case ?root
       {.#None}
diff --git a/stdlib/source/library/lux/data/collection/list.lux b/stdlib/source/library/lux/data/collection/list.lux
index 28f4d3db7..e5130f985 100644
--- a/stdlib/source/library/lux/data/collection/list.lux
+++ b/stdlib/source/library/lux/data/collection/list.lux
@@ -382,7 +382,10 @@
                             (if (< x x')
                               [{.#Item x' pre} post]
                               [pre {.#Item x' post}]))
-                          [(list) (list)]
+                          (`` [(: (~~ (:of xs))
+                                  (list))
+                               (: (~~ (:of xs))
+                                  (list))])
                           xs')]
       ($_ composite (sorted < pre) (list x) (sorted < post)))))
 
diff --git a/stdlib/source/library/lux/data/collection/sequence.lux b/stdlib/source/library/lux/data/collection/sequence.lux
index 07ebeba76..746654c57 100644
--- a/stdlib/source/library/lux/data/collection/sequence.lux
+++ b/stdlib/source/library/lux/data/collection/sequence.lux
@@ -224,10 +224,8 @@
             ... If so, a brand-new root must be established, that is
             ... 1-level taller.
             (|> sequence
-                (with@ #root (|> (for [@.old
-                                       (: (Hierarchy (:parameter 0))
-                                          (empty_hierarchy []))]
-                                      (empty_hierarchy []))
+                (with@ #root (|> (`` (: (Hierarchy (~~ (:of val)))
+                                        (empty_hierarchy [])))
                                  (array.write! 0 {#Hierarchy (value@ #root sequence)})
                                  (array.write! 1 (..path (value@ #level sequence) (value@ #tail sequence)))))
                 (revised@ #level level_up))
@@ -293,10 +291,9 @@
       {try.#Success (if (n.< (tail_off sequence_size) idx)
                       (revised@ #root (hierarchy#has (value@ #level sequence) idx val)
                                 sequence)
-                      (revised@ #tail (for [@.old
-                                            (: (-> (Base (:parameter 0)) (Base (:parameter 0)))
-                                               (|>> array.clone (array.write! (branch_idx idx) val)))]
-                                           (|>> array.clone (array.write! (branch_idx idx) val)))
+                      (revised@ #tail (`` (: (-> (Base (~~ (:of val)))
+                                                 (Base (~~ (:of val))))
+                                             (|>> array.clone (array.write! (branch_idx idx) val))))
                                 sequence))}
       (exception.except ..index_out_of_bounds [sequence idx]))))
 
diff --git a/stdlib/source/library/lux/data/collection/tree/finger.lux b/stdlib/source/library/lux/data/collection/tree/finger.lux
index 270623c6e..7c8a244b1 100644
--- a/stdlib/source/library/lux/data/collection/tree/finger.lux
+++ b/stdlib/source/library/lux/data/collection/tree/finger.lux
@@ -15,8 +15,8 @@
   (Record
    [#monoid (Monoid t)
     #tag t
-    #root (Or v
-              [(Tree @ t v) (Tree @ t v)])])
+    #root (Either v
+                  [(Tree @ t v) (Tree @ t v)])])
 
   (type: .public (Builder @ t)
     (Interface
@@ -45,13 +45,13 @@
       (:abstraction
        [#monoid monoid
         #tag tag
-        #root {0 #0 value}]))
+        #root {.#Left value}]))
     
     (def: (branch left right)
       (:abstraction
        [#monoid monoid
         #tag (# monoid composite (..tag left) (..tag right))
-        #root {0 #1 [left right]}])))
+        #root {.#Right [left right]}])))
 
   (def: .public (value tree)
     (All (_ @ t v) (-> (Tree @ t v) v))
diff --git a/stdlib/source/library/lux/ffi.jvm.lux b/stdlib/source/library/lux/ffi.jvm.lux
index 59d2b2374..46ffa8021 100644
--- a/stdlib/source/library/lux/ffi.jvm.lux
+++ b/stdlib/source/library/lux/ffi.jvm.lux
@@ -1258,9 +1258,9 @@
 (syntax: .public (??? [expr <code>.any])
   (with_symbols [g!temp]
     (in (list (` (let [(~ g!temp) (~ expr)]
-                   (if ("jvm object null?" (~ g!temp))
-                     {.#None}
-                     {.#Some (~ g!temp)})))))))
+                   (if (not ("jvm object null?" (~ g!temp)))
+                     {.#Some (~ g!temp)}
+                     {.#None})))))))
 
 (syntax: .public (!!! [expr <code>.any])
   (with_symbols [g!value]
diff --git a/stdlib/source/library/lux/math/random.lux b/stdlib/source/library/lux/math/random.lux
index 469a17226..1b3a9426a 100644
--- a/stdlib/source/library/lux/math/random.lux
+++ b/stdlib/source/library/lux/math/random.lux
@@ -352,7 +352,7 @@
   (let [magic 6364136223846793005]
     (function (_ _)
       [(|> seed .nat (n.* magic) ("lux i64 +" increase) [increase] pcg_32)
-       (let [rot (|> seed .i64 (i64.right_shifted 59))]
+       (let [rot (|> seed .nat (i64.right_shifted 59))]
          (|> seed
              (i64.right_shifted 18)
              (i64.xor seed)
diff --git a/stdlib/source/library/lux/target/python.lux b/stdlib/source/library/lux/target/python.lux
index 87864e062..dc1b5e935 100644
--- a/stdlib/source/library/lux/target/python.lux
+++ b/stdlib/source/library/lux/target/python.lux
@@ -450,7 +450,7 @@
 
   (def: .public (comment commentary on)
     (All (_ brand) (-> Text (Code brand) (Code brand)))
-    (:abstraction (format "# "  (..safe commentary) \n+
+    (:abstraction (format "# "  (text.replaced text.\n "\n" commentary) \n+
                           (:representation on))))
   )
 
diff --git a/stdlib/source/library/lux/tool/compiler/default/platform.lux b/stdlib/source/library/lux/tool/compiler/default/platform.lux
index ef79450e9..f13ffecd2 100644
--- a/stdlib/source/library/lux/tool/compiler/default/platform.lux
+++ b/stdlib/source/library/lux/tool/compiler/default/platform.lux
@@ -51,6 +51,7 @@
      [phase
       ["[0]" extension {"+" Extender}]]]]
    [meta
+    [import {"+" Import}]
     [cli {"+" Compilation Library}
      ["[0]" compiler {"+" Compiler}]]
     ["[0]" archive {"+" Output Archive}
@@ -64,7 +65,6 @@
      ["ioW" archive]]]]]
  [program
   [compositor
-   [import {"+" Import}]
    ["[0]" static {"+" Static}]]])
 
 (with_expansions [<type_vars> (as_is anchor expression directive)
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis.lux
index 2d231f1cc..65b191979 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis.lux
@@ -159,7 +159,8 @@
 (def: .public (reification analysis)
   (-> Analysis (Reification Analysis))
   (loop [abstraction analysis
-         inputs (list)]
+         inputs (: (List Analysis)
+                   (list))]
     (.case abstraction
       {#Apply input next}
       (again next {.#Item input inputs})
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
index 1b693629a..6ca7137d2 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
@@ -3,7 +3,7 @@
   [lux "*"
    ["[0]" meta]
    [abstract
-    [monad {"+" do}]]
+    ["[0]" monad {"+" do}]]
    [control
     [pipe {"+" case>}]
     ["[0]" maybe]
@@ -53,25 +53,6 @@
   [invalid_type_application]
   )
 
-(def: prefix
-  (format (%.symbol (symbol ..type)) "#"))
-
-(def: .public (existential? type)
-  (-> Type Bit)
-  (case type
-    {.#Primitive actual {.#End}}
-    (text.starts_with? ..prefix actual)
-
-    _
-    false))
-
-(def: existential
-  (Operation Type)
-  (do phase.monad
-    [module (extension.lifted meta.current_module_name)
-     [id _] (/type.check check.existential)]
-    (in {.#Primitive (format ..prefix module "#" (%.nat id)) (list)})))
-
 (def: .public (quantified @var @parameter :it:)
   (-> check.Var Nat Type Type)
   (case :it:
@@ -111,33 +92,34 @@
 ... tagged variants).
 ... But, so long as the type being used for the inference can be treated
 ... as a function type, this method of inference should work.
-(def: .public (general archive analyse inferT args)
-  (-> Archive Phase Type (List Code) (Operation [Type (List Analysis)]))
+(def: (general' vars archive analyse inferT args)
+  (-> (List check.Var) Archive Phase Type (List Code) (Operation [Type_Context (List check.Var) Type (List Analysis)]))
   (case args
     {.#End}
     (do phase.monad
-      [_ (/type.inference inferT)]
-      (in [inferT (list)]))
+      [just_before (/type.check check.context)
+       _ (/type.inference inferT)]
+      (in [just_before vars inferT (list)]))
     
     {.#Item argC args'}
     (case inferT
       {.#Named name unnamedT}
-      (general archive analyse unnamedT args)
+      (general' vars archive analyse unnamedT args)
 
       {.#UnivQ _}
       (do phase.monad
         [[@var :var:] (/type.check check.var)]
-        (general archive analyse (maybe.trusted (type.applied (list :var:) inferT)) args))
+        (general' (list& @var vars) archive analyse (maybe.trusted (type.applied (list :var:) inferT)) args))
 
       {.#ExQ _}
       (do phase.monad
-        [:ex: ..existential]
-        (general archive analyse (maybe.trusted (type.applied (list :ex:) inferT)) args))
+        [:ex: /type.existential]
+        (general' vars archive analyse (maybe.trusted (type.applied (list :ex:) inferT)) args))
 
       {.#Apply inputT transT}
       (case (type.applied (list inputT) transT)
         {.#Some outputT}
-        (general archive analyse outputT args)
+        (general' vars archive analyse outputT args)
 
         {.#None}
         (/.except ..invalid_type_application [inferT]))
@@ -151,18 +133,18 @@
       ... things together more easily.
       {.#Function inputT outputT}
       (do phase.monad
-        [[outputT' args'A] (general archive analyse outputT args')
+        [[just_before vars outputT' args'A] (general' vars archive analyse outputT args')
          argA (<| (/.with_exception ..cannot_infer_argument [inputT argC])
                   (/type.expecting inputT)
                   (analyse archive argC))]
-        (in [outputT' (list& argA args'A)]))
+        (in [just_before vars outputT' (list& argA args'A)]))
 
       {.#Var infer_id}
       (do phase.monad
         [?inferT' (/type.check (check.peek infer_id))]
         (case ?inferT'
           {.#Some inferT'}
-          (general archive analyse inferT' args)
+          (general' vars archive analyse inferT' args)
 
           _
           (/.except ..cannot_infer [inferT args])))
@@ -171,6 +153,40 @@
       (/.except ..cannot_infer [inferT args]))
     ))
 
+(def: .public (general archive analyse inferT args)
+  (-> Archive Phase Type (List Code) (Operation [Type (List Analysis)]))
+  (do [! phase.monad]
+    [[just_before vars :inference: terms] (general' (list) archive analyse inferT args)]
+    (in [:inference: terms])
+    ... (case vars
+    ...   (^ (list))
+    ...   (in [:inference: terms])
+
+    ...   _
+    ...   (do !
+    ...     [:inference: (/type.check
+    ...                   (do [! check.monad]
+    ...                     [quantifications (monad.mix ! (function (_ @var level)
+    ...                                                     (do !
+    ...                                                       [:var: (check.try (check.identity vars @var))]
+    ...                                                       (case :var:
+    ...                                                         {try.#Success _}
+    ...                                                         (in level)
+
+    ...                                                         {try.#Failure _}
+    ...                                                         (do !
+    ...                                                           [.let [:var: (|> level (n.* 2) ++ {.#Parameter})]
+    ...                                                            _ (check.bind :var: @var)]
+    ...                                                           (in (++ level))))))
+    ...                                                 0
+    ...                                                 vars)
+    ...                      :inference:' (# ! each (type.univ_q quantifications) (check.clean vars :inference:))
+    ...                      _ (check.with just_before)]
+    ...                     (in :inference:')))
+    ...      _ (/type.inference :inference:)]
+    ...     (in [:inference: terms])))
+    ))
+
 (def: (with_recursion @self recursion)
   (-> Nat Type Type Type)
   (function (again it)
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
index c066115ec..bd2c04844 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
@@ -3,10 +3,18 @@
   [lux "*"
    ["[0]" meta]
    [abstract
-    [monad {"+" do}]]
+    ["[0]" monad {"+" do}]]
    [control
     ["[0]" function]
     ["[0]" try]]
+   [data
+    ["[0]" text
+     ["%" format {"+" format}]]
+    [collection
+     ["[0]" list]]]
+   [math
+    [number
+     ["n" nat]]]
    [type
     ["[0]" check {"+" Check}]]]]
  ["/" // {"+" Operation}
@@ -16,11 +24,6 @@
    [///
     ["[0]" phase]]]])
 
-(def: .public (expecting expected)
-  (All (_ a) (-> Type (Operation a) (Operation a)))
-  (extension.localized (value@ .#expected) (with@ .#expected)
-                       (function.constant {.#Some expected})))
-
 (def: .public (check action)
   (All (_ a) (-> (Check a) (Operation a)))
   (function (_ (^@ stateE [bundle state]))
@@ -32,6 +35,34 @@
       {try.#Failure error}
       ((/.failure error) stateE))))
 
+(def: prefix
+  (format (%.symbol (symbol ..type)) "#"))
+
+(def: .public (existential? type)
+  (-> Type Bit)
+  (case type
+    {.#Primitive actual {.#End}}
+    (text.starts_with? ..prefix actual)
+
+    _
+    false))
+
+(def: (existential' module id)
+  (-> Text Nat Type)
+  {.#Primitive (format ..prefix module "#" (%.nat id)) (list)})
+
+(def: .public existential
+  (Operation Type)
+  (do phase.monad
+    [module (extension.lifted meta.current_module_name)
+     [id _] (..check check.existential)]
+    (in (..existential' module id))))
+
+(def: .public (expecting expected)
+  (All (_ a) (-> Type (Operation a) (Operation a)))
+  (extension.localized (value@ .#expected) (with@ .#expected)
+                       (function.constant {.#Some expected})))
+
 (def: .public fresh
   (All (_ a) (-> (Operation a) (Operation a)))
   (extension.localized (value@ .#type_context) (with@ .#type_context)
@@ -40,8 +71,44 @@
 (def: .public (inference actualT)
   (-> Type (Operation Any))
   (do phase.monad
-    [expectedT (extension.lifted meta.expected_type)]
-    (..check (check.check expectedT actualT))))
+    [module (extension.lifted meta.current_module_name)
+     expectedT (extension.lifted meta.expected_type)]
+    (..check (check.check expectedT actualT)
+             ... (do [! check.monad]
+             ...   [pre check.context
+             ...    it (check.check expectedT actualT)
+             ...    post check.context
+             ...    .let [pre#var_counter (value@ .#var_counter pre)]]
+             ...   (if (n.< (value@ .#var_counter post)
+             ...            pre#var_counter)
+             ...     (do !
+             ...       [.let [new! (: (-> [Nat (Maybe Type)] (Maybe Nat))
+             ...                      (function (_ [id _])
+             ...                        (if (n.< id pre#var_counter)
+             ...                          {.#Some id}
+             ...                          {.#None})))
+             ...              new_vars (|> post
+             ...                           (value@ .#var_bindings)
+             ...                           (list.all new!))]
+             ...        _ (monad.each ! (function (_ @new)
+             ...                          (do !
+             ...                            [:new: (check.try (check.identity new_vars @new))]
+             ...                            (case :new:
+             ...                              {try.#Success :new:}
+             ...                              (in :new:)
+             
+             ...                              {try.#Failure error}
+             ...                              (do !
+             ...                                [[id _] check.existential
+             ...                                 .let [:new: (..existential' module id)]
+             ...                                 _ (check.bind :new: @new)]
+             ...                                (in :new:)))))
+             ...                      new_vars)
+             ...        expectedT' (check.clean new_vars expectedT)
+             ...        _ (check.with pre)]
+             ...       (check.check expectedT' actualT))
+             ...     (in it)))
+             )))
 
 (def: .public (with_var it)
   (All (_ a) (-> (-> [check.Var Type] (Operation a))
@@ -50,7 +117,8 @@
     [var (..check check.var)
      .let [[@it :it:] var]
      it (it var)
-     _ (..check (check.forget! @it))]
+     ... _ (..check (check.forget! @it))
+     ]
     (in it)))
 
 (def: .public (inferring action)
@@ -58,5 +126,10 @@
   (do phase.monad
     [[@it :it:] (..check check.var)
      it (..expecting :it: action)
-     :it: (..check (check.clean :it:))]
+     :it: (..check (check.clean (list) :it:))
+     ... :it: (..check (do check.monad
+     ...                 [:it: (check.identity (list) @it)
+     ...                  _ (check.forget! @it)]
+     ...                 (in :it:)))
+     ]
     (in [:it: it])))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/complex.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/complex.lux
index 726860314..cce7b1f00 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/complex.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/complex.lux
@@ -105,7 +105,7 @@
     (function (again valueC)
       (do [! ///.monad]
         [expectedT (///extension.lifted meta.expected_type)
-         expectedT' (/type.check (check.clean expectedT))]
+         expectedT' (/type.check (check.clean (list) expectedT))]
         (/.with_exception ..cannot_analyse_variant [expectedT' lefts right? valueC]
           (case expectedT
             {.#Sum _}
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux
index a7d889777..2338824c4 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/jvm.lux
@@ -461,7 +461,7 @@
          [var_id varT] (typeA.check check.var)
          arrayA (<| (typeA.expecting (.type (array.Array varT)))
                     (analyse archive arrayC))
-         varT (typeA.check (check.clean varT))
+         varT (typeA.check (check.clean (list) varT))
          arrayJT (jvm_array_type (.type (array.Array varT)))]
         (in {/////analysis.#Extension extension_name (list (/////analysis.text (..signature arrayJT))
                                                            arrayA)}))
@@ -667,7 +667,7 @@
          _ (typeA.inference varT)
          arrayA (<| (typeA.expecting (.type (array.Array varT)))
                     (analyse archive arrayC))
-         varT (typeA.check (check.clean varT))
+         varT (typeA.check (check.clean (list) varT))
          arrayJT (jvm_array_type (.type (array.Array varT)))
          idxA (<| (typeA.expecting ..int)
                   (analyse archive idxC))]
@@ -710,7 +710,7 @@
          _ (typeA.inference (.type (array.Array varT)))
          arrayA (<| (typeA.expecting (.type (array.Array varT)))
                     (analyse archive arrayC))
-         varT (typeA.check (check.clean varT))
+         varT (typeA.check (check.clean (list) varT))
          arrayJT (jvm_array_type (.type (array.Array varT)))
          idxA (<| (typeA.expecting ..int)
                   (analyse archive idxC))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/directive/lux.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/directive/lux.lux
index 04006e52f..e159172b2 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/directive/lux.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/directive/lux.lux
@@ -146,7 +146,7 @@
                                 (do !
                                   [[code//type codeA] (typeA.inferring
                                                        (analyse archive codeC))
-                                   code//type (typeA.check (check.clean code//type))]
+                                   code//type (typeA.check (check.clean (list) code//type))]
                                   (in [code//type codeA]))
 
                                 {.#Some expected}
diff --git a/stdlib/source/library/lux/tool/compiler/meta/archive.lux b/stdlib/source/library/lux/tool/compiler/meta/archive.lux
index d8347d9fd..4ec08ed90 100644
--- a/stdlib/source/library/lux/tool/compiler/meta/archive.lux
+++ b/stdlib/source/library/lux/tool/compiler/meta/archive.lux
@@ -108,7 +108,7 @@
         {try.#Success [/#next
                        (|> archive
                            :representation
-                           (revised@ #resolver (dictionary.has module [/#next {.#None}]))
+                           (revised@ #resolver (dictionary.has module [/#next (: (Maybe (Entry Any)) {.#None})]))
                            (revised@ #next ++)
                            :abstraction)]})))
 
@@ -261,7 +261,7 @@
       (in (:abstraction
            [#next next
             #resolver (list#mix (function (_ [module id] archive)
-                                  (dictionary.has module [id {.#None}] archive))
+                                  (dictionary.has module [id (: (Maybe (Entry Any)) {.#None})] archive))
                                 (value@ #resolver (:representation ..empty))
                                 reservations)]))))
   )
diff --git a/stdlib/source/library/lux/tool/compiler/meta/export.lux b/stdlib/source/library/lux/tool/compiler/meta/export.lux
index 79c5a2a44..9b21de75b 100644
--- a/stdlib/source/library/lux/tool/compiler/meta/export.lux
+++ b/stdlib/source/library/lux/tool/compiler/meta/export.lux
@@ -30,7 +30,13 @@
 (def: .public file
   "library.tar")
 
-(def: commons
+(def: .public mode
+  ($_ tar.and
+      tar.read_by_owner tar.write_by_owner
+      tar.read_by_group tar.write_by_group
+      tar.read_by_other))
+
+(def: .public ownership
   tar.Ownership
   (let [commons (: tar.Owner
                    [tar.#name tar.anonymous
@@ -51,11 +57,8 @@
                                                                 tar.path)]
                                                       (try#each (|>> [path
                                                                       (instant.of_millis +0)
-                                                                      ($_ tar.and
-                                                                          tar.read_by_owner tar.write_by_owner
-                                                                          tar.read_by_group tar.write_by_group
-                                                                          tar.read_by_other)
-                                                                      ..commons]
+                                                                      ..mode
+                                                                      ..ownership]
                                                                      {tar.#Normal})
                                                                 (tar.content source_code)))))
                                       (try#each sequence.of_list)))
diff --git a/stdlib/source/library/lux/tool/compiler/meta/import.lux b/stdlib/source/library/lux/tool/compiler/meta/import.lux
new file mode 100644
index 000000000..d3a356c43
--- /dev/null
+++ b/stdlib/source/library/lux/tool/compiler/meta/import.lux
@@ -0,0 +1,74 @@
+(.using
+ [library
+  [lux {"-" Module}
+   [abstract
+    ["[0]" monad {"+" Monad do}]]
+   [control
+    ["[0]" try {"+" Try}]
+    ["[0]" exception {"+" exception:}]
+    [concurrency
+     ["[0]" async {"+" Async}]]
+    ["<>" parser
+     ["<[0]>" binary]]]
+   [data
+    [binary {"+" Binary}]
+    ["[0]" text
+     ["%" format]]
+    [collection
+     ["[0]" dictionary {"+" Dictionary}]
+     ["[0]" sequence]]
+    [format
+     ["[0]" tar]]]
+   [tool
+    [compiler
+     [meta
+      [cli {"+" Library Module}]]]]
+   [world
+    ["[0]" file]]]])
+
+(def: Action
+  (type (All (_ a) (Async (Try a)))))
+
+(exception: .public useless_tar_entry)
+
+(exception: .public (duplicate [library Library
+                                module Module])
+  (exception.report
+   ["Module" (%.text module)]
+   ["Library" (%.text library)]))
+
+(type: .public Import
+  (Dictionary file.Path Binary))
+
+(def: (import_library system library import)
+  (-> (file.System Async) Library Import (Action Import))
+  (let [! async.monad]
+    (|> library
+        (# system read)
+        (# ! each (let [! try.monad]
+                    (|>> (# ! each (<binary>.result tar.parser))
+                         (# ! conjoint)
+                         (# ! each (|>> sequence.list
+                                        (monad.mix ! (function (_ entry import)
+                                                       (case entry
+                                                         {tar.#Normal [path instant mode ownership content]}
+                                                         (let [path (tar.from_path path)]
+                                                           (case (dictionary.has' path (tar.data content) import)
+                                                             {try.#Failure error}
+                                                             (exception.except ..duplicate [library path])
+
+                                                             import'
+                                                             import'))
+                                                         
+                                                         _
+                                                         (exception.except ..useless_tar_entry [])))
+                                                   import)))
+                         (# ! conjoint)))))))
+
+(def: .public (import system libraries)
+  (-> (file.System Async) (List Library) (Action Import))
+  (monad.mix (: (Monad Action)
+                (try.with async.monad))
+             (..import_library system)
+             (dictionary.empty text.hash)
+             libraries))
diff --git a/stdlib/source/library/lux/tool/compiler/meta/io/archive.lux b/stdlib/source/library/lux/tool/compiler/meta/io/archive.lux
index 63cae0681..b9b99208f 100644
--- a/stdlib/source/library/lux/tool/compiler/meta/io/archive.lux
+++ b/stdlib/source/library/lux/tool/compiler/meta/io/archive.lux
@@ -30,11 +30,11 @@
     ["[0]" file]]]]
  [program
   [compositor
-   [import {"+" Import}]
    ["[0]" static {"+" Static}]]]
  ["[0]" // {"+" Context}
   ["[1][0]" context]
   ["/[1]" //
+   [import {"+" Import}]
    ["[0]" archive {"+" Output Archive}
     ["[0]" registry {"+" Registry}]
     ["[0]" unit]
diff --git a/stdlib/source/library/lux/tool/compiler/meta/io/context.lux b/stdlib/source/library/lux/tool/compiler/meta/io/context.lux
index 2f99ddce1..d576571eb 100644
--- a/stdlib/source/library/lux/tool/compiler/meta/io/context.lux
+++ b/stdlib/source/library/lux/tool/compiler/meta/io/context.lux
@@ -22,11 +22,9 @@
      ["[0]" list]]]
    [world
     ["[0]" file]]]]
- [program
-  [compositor
-   [import {"+" Import}]]]
  ["[0]" // {"+" Context Code}
   ["/[1]" // "_"
+   [import {"+" Import}]
    ["/[1]" // {"+" Input}]
    [archive
     [module
diff --git a/stdlib/source/library/lux/type/check.lux b/stdlib/source/library/lux/type/check.lux
index 31ec9da05..984456187 100644
--- a/stdlib/source/library/lux/type/check.lux
+++ b/stdlib/source/library/lux/type/check.lux
@@ -299,10 +299,7 @@
       _
       (except ..invalid_type_application [funcT argT]))))
 
-(type: Ring
-  (Set Var))
-
-(def: (ring' start)
+(def: .public (ring' start)
   (-> Var (Check (List Var)))
   (function (_ context)
     (loop [current start
@@ -326,7 +323,7 @@
 
 ... TODO: Optimize this by not using sets anymore.
 (def: ring
-  (-> Var (Check Ring))
+  (-> Var (Check (Set Var)))
   (|>> ..ring'
        (check#each (set.of_list n.hash))))
 
@@ -336,15 +333,7 @@
                 (set.member? it @1))
               (..ring @0)))
 
-(exception: (invalid_alias [var Var
-                            expected (List Var)
-                            actual (List Var)])
-  (exception.report
-   ["Var" (n#encoded var)]
-   ["Expected" (exception.listing n#encoded expected)]
-   ["Actual" (exception.listing n#encoded actual)]))
-
-(exception: (cannot_identify [var Var])
+(exception: .public (cannot_identify [var Var])
   (exception.report
    ["Var" (n#encoded var)]))
 
@@ -358,18 +347,18 @@
 
       {.#None}
       (do !
-        [existing_aliases (..ring @)
-         _ (if (list.every? (set.member? existing_aliases) aliases)
-             (in [])
-             (..except ..invalid_alias [@ aliases (set.list existing_aliases)]))
-         .let [forbidden_aliases (set.of_list n.hash (list& @ aliases))
-               allowed_aliases (set.difference forbidden_aliases existing_aliases)]]
-        (case (set.list allowed_aliases)
-          {.#Item identity _}
-          (in {.#Var identity})
-          
-          {.#None}
-          (..except ..cannot_identify [@]))))))
+        [existing_aliases (..ring @)]
+        (if (n.< 2 (set.size existing_aliases))
+          (..except ..cannot_identify [@])
+          (do !
+            [.let [forbidden_aliases (set.of_list n.hash (list& @ aliases))
+                   allowed_aliases (set.difference forbidden_aliases existing_aliases)]]
+            (case (set.list allowed_aliases)
+              {.#Item identity _}
+              (in {.#Var identity})
+              
+              {.#None}
+              (..except ..cannot_identify [@]))))))))
 
 (def: (erase! @)
   (-> Var (Check Any))
@@ -639,7 +628,7 @@
       _
       ..silent_failure!)))
 
-(def: (with exception parameter check)
+(def: (with_exception exception parameter check)
   (All (_ e a) (-> (Exception e) e (Check a) (Check a)))
   (|>> check
        (exception.with exception parameter)))
@@ -652,7 +641,7 @@
             @.php false]
            (same? expected actual))
     (check#in assumptions)
-    (with ..type_check_failed [expected actual]
+    (with_exception ..type_check_failed [expected actual]
       (case [expected actual]
         [{.#Var idE} {.#Var idA}]
         (check_vars check' assumptions idE idA)
@@ -774,12 +763,17 @@
   (function (_ context)
     {try.#Success [context context]}))
 
-(def: .public (clean inputT)
-  (-> Type (Check Type))
+(def: .public (with context)
+  (-> Type_Context (Check Any))
+  (function (_ _)
+    {try.#Success [context []]}))
+
+(def: .public (clean aliases inputT)
+  (-> (List Var) Type (Check Type))
   (case inputT
     {.#Primitive name paramsT+}
     (|> paramsT+
-        (monad.each ..monad clean)
+        (monad.each ..monad (clean aliases))
         (check#each (|>> {.#Primitive name})))
 
     (^or {.#Parameter _} {.#Ex _} {.#Named _})
@@ -788,26 +782,43 @@
     (^template [<tag>]
       [{<tag> leftT rightT}
        (do ..monad
-         [leftT' (clean leftT)]
-         (|> (clean rightT)
+         [leftT' (clean aliases leftT)]
+         (|> (clean aliases rightT)
              (check#each (|>> {<tag> leftT'}))))])
     ([.#Sum] [.#Product] [.#Function] [.#Apply])
 
     {.#Var @}
-    (do ..monad
-      [?actualT (peek @)]
-      (case ?actualT
-        {.#Some actualT}
-        (clean actualT)
+    (case aliases
+      (^ (list))
+      (do ..monad
+        [?actualT (peek @)]
+        (case ?actualT
+          {.#Some actualT}
+          (clean aliases actualT)
 
-        _
-        (in inputT)))
+          _
+          (in inputT)))
+
+      _
+      (do ..monad
+        [:it: (..try (..identity aliases @))]
+        (case :it:
+          {try.#Success :it:}
+          (case :it:
+            {.#Var _}
+            (in inputT)
+
+            _
+            (clean aliases :it:))
+
+          failure
+          (in inputT))))
 
     (^template [<tag>]
       [{<tag> envT+ unquantifiedT}
        (do [! ..monad]
-         [envT+' (monad.each ! clean envT+)
-          unquantifiedT' (clean unquantifiedT)]
+         [envT+' (monad.each ! (clean aliases) envT+)
+          unquantifiedT' (clean aliases unquantifiedT)]
          (in {<tag> envT+' unquantifiedT'}))])
     ([.#UnivQ] [.#ExQ])
     ))
diff --git a/stdlib/source/library/lux/world/program.lux b/stdlib/source/library/lux/world/program.lux
index 950f19206..5fdc9cc21 100644
--- a/stdlib/source/library/lux/world/program.lux
+++ b/stdlib/source/library/lux/world/program.lux
@@ -306,10 +306,11 @@
   (Program IO)
 
   (def: (available_variables _)
-    (with_expansions [<jvm> (io.io (|> (java/lang/System::getenv)
-                                       java/util/Map::keySet
-                                       java/util/Set::iterator
-                                       ..jvm##consume))]
+    (with_expansions [<jvm> (|> (java/lang/System::getenv)
+                                java/util/Map::keySet
+                                java/util/Set::iterator
+                                ..jvm##consume
+                                io.io)]
       (for [@.old <jvm>
             @.jvm <jvm>
             @.js (io.io (if ffi.on_node_js?
@@ -325,9 +326,7 @@
             @.python (# io.monad each (array.list {.#None}) (os/environ::keys []))
             ... Lua offers no way to get all the environment variables available.
             @.lua (io.io (list))
-            @.ruby (|> (RubyEnv::keys [])
-                       (array.list {.#None})
-                       io.io)
+            @.ruby (io.io (array.list {.#None} (RubyEnv::keys [])))
             ... @.php (do io.monad
             ...         [environment (..getenv/0 [])]
             ...         (in (|> environment