Fixes for the pure-Lux JVM compiler machinery. [Part 12]

19 files changed, 1361 insertions, 608 deletions

diff --git a/documentation/bookmark/back_end/c++.md b/documentation/bookmark/back_end/c++.md
index 21664d692..d7436b3bb 100644
--- a/documentation/bookmark/back_end/c++.md
+++ b/documentation/bookmark/back_end/c++.md
@@ -1,5 +1,6 @@
 # Reference
 
+0. [Misra Parallelism Safety-critical Guidelines for C++11, 17, Then C++20, 23 - CppCon 2021](https://www.youtube.com/watch?v=hVv7Nc3f4Jo)
 0. [Back to Basics: Move Semantics - Nicolai Josuttis - CppCon 2021](https://www.youtube.com/watch?v=Bt3zcJZIalk)
 0. [Type-and-resource Safety in Modern C++ - Bjarne Stroustrup - CppCon 2021](https://www.youtube.com/watch?v=l3rvjWfBzZI)
 0. [Exceptional C++ - Victor Ciura - CppCon 2021](https://www.youtube.com/watch?v=SjlfhyZn2yA)
diff --git a/stdlib/source/library/lux/math/random.lux b/stdlib/source/library/lux/math/random.lux
index 13bac71cf..469a17226 100644
--- a/stdlib/source/library/lux/math/random.lux
+++ b/stdlib/source/library/lux/math/random.lux
@@ -195,30 +195,28 @@
 
 (def: .public (and left right)
   (All (_ a b) (-> (Random a) (Random b) (Random [a b])))
-  (do ..monad
-    [=left left
-     =right right]
-    (in [=left =right])))
+  (function (_ prng)
+    (let [[prng left] (left prng)
+          [prng right] (right prng)]
+      [prng [left right]])))
 
 (def: .public (or left right)
   (All (_ a b) (-> (Random a) (Random b) (Random (Or a b))))
-  (do [! ..monad]
-    [? bit]
-    (if ?
-      (do !
-        [=left left]
-        (in {0 #0 =left}))
-      (do !
-        [=right right]
-        (in {0 #1 =right})))))
+  (function (_ prng)
+    (let [[prng ?] (..bit prng)]
+      (if ?
+        (let [[prng left] (left prng)]
+          [prng {0 #0 left}])
+        (let [[prng right] (right prng)]
+          [prng {0 #1 right}])))))
 
 (def: .public (either left right)
   (All (_ a) (-> (Random a) (Random a) (Random a)))
-  (do ..monad
-    [? bit]
-    (if ?
-      left
-      right)))
+  (function (_ prng)
+    (let [[prng ?] (..bit prng)]
+      (if ?
+        (left prng)
+        (right prng)))))
 
 (def: .public (rec gen)
   (All (_ a) (-> (-> (Random a) (Random a)) (Random a)))
diff --git a/stdlib/source/library/lux/test.lux b/stdlib/source/library/lux/test.lux
index 7f0c76d58..d9555ec44 100644
--- a/stdlib/source/library/lux/test.lux
+++ b/stdlib/source/library/lux/test.lux
@@ -103,7 +103,7 @@
     [left left]
     (# ! each (..and' left) right)))
 
-(def: .public (context description)
+(def: (context' description)
   (-> Text Test Test)
   (random#each (async#each (function (_ [tally documentation])
                              [tally (|> documentation
@@ -112,6 +112,10 @@
                                         (text.interposed ..separator)
                                         (format description ..separator))]))))
 
+(def: .public context
+  (-> Text Test Test)
+  (|>> %.text context'))
+
 (def: failure_prefix "[Failure] ")
 (def: success_prefix "[Success] ")
 
@@ -131,11 +135,11 @@
 
 (def: .public (test message condition)
   (-> Text Bit Test)
-  (random#in (..assertion message condition)))
+  (random#in (..assertion (%.text message) condition)))
 
 (def: .public (lifted message random)
   (-> Text (Random Bit) Test)
-  (random#each (..assertion message) random))
+  (random#each (..assertion (%.text message)) random))
 
 (def: pcg_32_magic_inc
   Nat
@@ -293,7 +297,7 @@
     (random#each (async#each (function (_ [tally documentation])
                                [(revised@ #actual_coverage (set.union coverage) tally)
                                 documentation]))
-                 (..context context test))))
+                 (..context' context test))))
 
 (def: (symbol_code symbol)
   (-> Symbol Code)
@@ -356,7 +360,7 @@
 (def: (covering' module coverage test)
   (-> Text Text Test Test)
   (let [coverage (..coverage module coverage)]
-    (|> (..context module test)
+    (|> (..context' module test)
         (random#each (async#each (function (_ [tally documentation])
                                    [(revised@ #expected_coverage (set.union coverage) tally)
                                     (|> documentation
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
new file mode 100644
index 000000000..1d903e7d6
--- /dev/null
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
@@ -0,0 +1,231 @@
+(.using
+ [library
+  [lux "*"
+   ["[0]" meta]
+   [abstract
+    [monad {"+" do}]]
+   [control
+    [pipe {"+" case>}]
+    ["[0]" maybe]
+    ["[0]" exception {"+" exception:}]]
+   [data
+    ["[0]" text
+     ["%" format {"+" format}]]
+    [collection
+     ["[0]" list ("[1]#[0]" functor monoid)]]]
+   [macro
+    ["[0]" template]]
+   [math
+    [number
+     ["n" nat]]]
+   ["[0]" type
+    ["[0]" check]]]]
+ ["/" // {"+" Analysis Operation Phase}
+  ["[1][0]" type]
+  [//
+   [phase
+    ["[0]" extension]]
+   [///
+    ["[0]" phase ("[1]#[0]" monad)]
+    [meta
+     [archive {"+" Archive}]]]]])
+
+(exception: .public (cannot_infer [type Type
+                                   arguments (List Code)])
+  (exception.report
+   ["Type" (%.type type)]
+   ["Arguments" (exception.listing %.code arguments)]))
+
+(exception: .public (cannot_infer_argument [type Type
+                                            argument Code])
+  (exception.report
+   ["Type" (%.type type)]
+   ["Argument" (%.code argument)]))
+
+(template [<name>]
+  [(exception: .public (<name> [type Type])
+     (exception.report
+      ["Type" (%.type type)]))]
+
+  [not_a_variant]
+  [not_a_record]
+  [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)})))
+
+... Type-inference works by applying some (potentially quantified) type
+... to a sequence of values.
+... Function types are used for this, although inference is not always
+... done for function application (alternative uses may be records and
+... 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)]))
+  (case args
+    {.#End}
+    (do phase.monad
+      [_ (/type.inference inferT)]
+      (in [inferT (list)]))
+    
+    {.#Item argC args'}
+    (case inferT
+      {.#Named name unnamedT}
+      (general archive analyse unnamedT args)
+
+      {.#UnivQ _}
+      (do phase.monad
+        [[var_id varT] (/type.check check.var)]
+        (general archive analyse (maybe.trusted (type.applied (list varT) inferT)) args))
+
+      {.#ExQ _}
+      (do [! phase.monad]
+        [exT ..existential]
+        (general archive analyse (maybe.trusted (type.applied (list exT) inferT)) args))
+
+      {.#Apply inputT transT}
+      (case (type.applied (list inputT) transT)
+        {.#Some outputT}
+        (general archive analyse outputT args)
+
+        {.#None}
+        (/.except ..invalid_type_application [inferT]))
+
+      ... Arguments are inferred back-to-front because, by convention,
+      ... Lux functions take the most important arguments *last*, which
+      ... means that the most information for doing proper inference is
+      ... located in the last arguments to a function call.
+      ... By inferring back-to-front, a lot of type-annotations can be
+      ... avoided in Lux code, since the inference algorithm can piece
+      ... things together more easily.
+      {.#Function inputT outputT}
+      (do phase.monad
+        [[outputT' args'A] (general archive analyse outputT args')
+         argA (<| (/.with_stack ..cannot_infer_argument [inputT argC])
+                  (/type.expecting inputT)
+                  (analyse archive argC))]
+        (in [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)
+
+          _
+          (/.except ..cannot_infer [inferT args])))
+
+      _
+      (/.except ..cannot_infer [inferT args]))
+    ))
+
+(def: (with_recursion @self recursion)
+  (-> Nat Type Type Type)
+  (function (again it)
+    (case it
+      (^or {.#Parameter index}
+           {.#Apply {.#Primitive "" {.#End}}
+                    {.#Parameter index}})
+      (if (n.= @self index)
+        recursion
+        it)
+      
+      (^template [<tag>]
+        [{<tag> left right}
+         {<tag> (again left) (again right)}])
+      ([.#Sum] [.#Product] [.#Function] [.#Apply])
+      
+      (^template [<tag>]
+        [{<tag> environment quantified}
+         {<tag> (list#each again environment)
+                (with_recursion (n.+ 2 @self) recursion quantified)}])
+      ([.#UnivQ] [.#ExQ])
+      
+      {.#Primitive name parameters}
+      {.#Primitive name (list#each again parameters)}
+
+      _
+      it)))
+
+(def: parameters
+  (-> Nat (List Type))
+  (|>> list.indices
+       (list#each (|>> (n.* 2) ++ {.#Parameter}))
+       list.reversed))
+
+(template [<name> <types> <inputs> <exception> <when> <then>]
+  [(`` (def: .public (<name> (~~ (template.spliced <inputs>)) complex)
+         (-> (~~ (template.spliced <types>)) Type (Operation Type))
+         (loop [depth 0
+                it complex]
+           (case it
+             {.#Named name it}
+             (again depth it)
+
+             (^template [<tag>]
+               [{<tag> env it}
+                (phase#each (|>> {<tag> env})
+                            (again (++ depth) it))])
+             ([.#UnivQ]
+              [.#ExQ])
+
+             {.#Apply parameter abstraction}
+             (case (type.applied (list parameter) abstraction)
+               {.#Some it}
+               (again depth it)
+
+               {.#None}
+               (/.except ..invalid_type_application [it]))
+
+             {<when> _}
+             <then>
+
+             _
+             (/.except <exception> [complex])))))]
+
+  [record [Nat] [arity] ..not_a_record
+   .#Product
+   (let [[lefts right] (|> it
+                           type.flat_tuple
+                           (list.split_at (-- arity)))]
+     (phase#in (type.function
+                 (list#each (..with_recursion (|> depth -- (n.* 2)) complex)
+                            (list#composite lefts (list (type.tuple right))))
+                 (type.application (parameters depth) complex))))]
+  [variant [Nat Bit] [lefts right?] ..not_a_variant
+   .#Sum
+   (|> it
+       type.flat_variant
+       (list.after lefts)
+       (case> {.#Item [head tail]}
+              (let [case (if right?
+                           (type.variant tail)
+                           head)]
+                (-> (if (n.= 0 depth)
+                      case
+                      (..with_recursion (|> depth -- (n.* 2)) complex case))
+                    (type.application (parameters depth) complex)))
+
+              {.#End}
+              (-> .Nothing complex))
+       phase#in)]
+  )
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux
index 8f7a67a0c..5a2018656 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/function.lux
@@ -16,12 +16,12 @@
     ["[0]" check]]]]
  ["[0]" // "_"
   ["[1][0]" scope]
-  ["[1][0]" inference]
   ["/[1]" // "_"
    ["[1][0]" extension]
    [//
     ["/" analysis {"+" Analysis Operation Phase}
-     ["[1][0]" type]]
+     ["[1][0]" type]
+     ["[1][0]" inference]]
     [///
      ["[1]" phase]
      [reference {"+"}
@@ -111,5 +111,5 @@
   (-> Phase (List Code) Type Analysis Phase)
   (<| (/.with_stack ..cannot_apply [functionT functionC argsC+])
       (do ///.monad
-        [[applyT argsA+] (//inference.general archive analyse functionT argsC+)])
+        [[applyT argsA+] (/inference.general archive analyse functionT argsC+)])
       (in (/.reified [functionA argsA+]))))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/inference.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/inference.lux
deleted file mode 100644
index ea03f2719..000000000
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/inference.lux
+++ /dev/null
@@ -1,306 +0,0 @@
-(.using
- [library
-  [lux "*"
-   ["[0]" meta]
-   [abstract
-    [monad {"+" do}]]
-   [control
-    ["[0]" maybe]
-    ["[0]" exception {"+" exception:}]]
-   [data
-    ["[0]" text
-     ["%" format {"+" format}]]
-    [collection
-     ["[0]" list ("[1]#[0]" functor monoid)]]]
-   [math
-    [number
-     ["n" nat]]]
-   ["[0]" type
-    ["[0]" check]]]]
- ["[0]" /// "_"
-  ["[1][0]" extension]
-  [//
-   ["/" analysis {"+" Analysis Operation Phase}
-    [complex {"+" Tag}]
-    ["[1][0]" type]]
-   [///
-    ["[1]" phase ("[1]#[0]" monad)]
-    [meta
-     [archive {"+" Archive}]]]]])
-
-(exception: .public (variant_tag_out_of_bounds [size Nat
-                                                tag Tag
-                                                type Type])
-  (exception.report
-   ["Tag" (%.nat tag)]
-   ["Variant size" (%.int (.int size))]
-   ["Variant type" (%.type type)]))
-
-(exception: .public (cannot_infer [type Type
-                                   args (List Code)])
-  (exception.report
-   ["Type" (%.type type)]
-   ["Arguments" (exception.listing %.code args)]))
-
-(exception: .public (cannot_infer_argument [inferred Type
-                                            argument Code])
-  (exception.report
-   ["Inferred Type" (%.type inferred)]
-   ["Argument" (%.code argument)]))
-
-(exception: .public (smaller_variant_than_expected [expected Nat
-                                                    actual Nat])
-  (exception.report
-   ["Expected" (%.int (.int expected))]
-   ["Actual" (%.int (.int actual))]))
-
-(template [<name>]
-  [(exception: .public (<name> [type Type])
-     (%.type type))]
-
-  [not_a_variant_type]
-  [not_a_record_type]
-  [invalid_type_application]
-  )
-
-(def: (replace parameter_idx replacement type)
-  (-> Nat Type Type Type)
-  (case type
-    {.#Primitive name params}
-    {.#Primitive name (list#each (replace parameter_idx replacement) params)}
-
-    (^template [<tag>]
-      [{<tag> left right}
-       {<tag>
-        (replace parameter_idx replacement left)
-        (replace parameter_idx replacement right)}])
-    ([.#Sum]
-     [.#Product]
-     [.#Function]
-     [.#Apply])
-    
-    {.#Parameter idx}
-    (if (n.= parameter_idx idx)
-      replacement
-      type)
-
-    (^template [<tag>]
-      [{<tag> env quantified}
-       {<tag> (list#each (replace parameter_idx replacement) env)
-              (replace (n.+ 2 parameter_idx) replacement quantified)}])
-    ([.#UnivQ]
-     [.#ExQ])
-    
-    _
-    type))
-
-(def: (named_type location id)
-  (-> Location Nat Type)
-  (let [name (format "{New Type " (%.location location) " " (%.nat id) "}")]
-    {.#Primitive name (list)}))
-
-(def: new_named_type
-  (Operation Type)
-  (do ///.monad
-    [location (///extension.lifted meta.location)
-     [ex_id _] (/type.check check.existential)]
-    (in (named_type location ex_id))))
-
-... Type-inference works by applying some (potentially quantified) type
-... to a sequence of values.
-... Function types are used for this, although inference is not always
-... done for function application (alternative uses may be records and
-... 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)]))
-  (case args
-    {.#End}
-    (do ///.monad
-      [_ (/type.inference inferT)]
-      (in [inferT (list)]))
-    
-    {.#Item argC args'}
-    (case inferT
-      {.#Named name unnamedT}
-      (general archive analyse unnamedT args)
-
-      {.#UnivQ _}
-      (do ///.monad
-        [[var_id varT] (/type.check check.var)]
-        (general archive analyse (maybe.trusted (type.applied (list varT) inferT)) args))
-
-      {.#ExQ _}
-      (do [! ///.monad]
-        [[var_id varT] (/type.check check.var)
-         output (general archive analyse
-                         (maybe.trusted (type.applied (list varT) inferT))
-                         args)
-         bound? (/type.check (check.bound? var_id))
-         _ (if bound?
-             (in [])
-             (do !
-               [newT new_named_type]
-               (/type.check (check.check varT newT))))]
-        (in output))
-
-      {.#Apply inputT transT}
-      (case (type.applied (list inputT) transT)
-        {.#Some outputT}
-        (general archive analyse outputT args)
-
-        {.#None}
-        (/.except ..invalid_type_application inferT))
-
-      ... Arguments are inferred back-to-front because, by convention,
-      ... Lux functions take the most important arguments *last*, which
-      ... means that the most information for doing proper inference is
-      ... located in the last arguments to a function call.
-      ... By inferring back-to-front, a lot of type-annotations can be
-      ... avoided in Lux code, since the inference algorithm can piece
-      ... things together more easily.
-      {.#Function inputT outputT}
-      (do ///.monad
-        [[outputT' args'A] (general archive analyse outputT args')
-         argA (<| (/.with_stack ..cannot_infer_argument [inputT argC])
-                  (/type.expecting inputT)
-                  (analyse archive argC))]
-        (in [outputT' (list& argA args'A)]))
-
-      {.#Var infer_id}
-      (do ///.monad
-        [?inferT' (/type.check (check.peek infer_id))]
-        (case ?inferT'
-          {.#Some inferT'}
-          (general archive analyse inferT' args)
-
-          _
-          (/.except ..cannot_infer [inferT args])))
-
-      _
-      (/.except ..cannot_infer [inferT args]))
-    ))
-
-(def: (substitute_bound target sub)
-  (-> Nat Type Type Type)
-  (function (again base)
-    (case base
-      {.#Primitive name parameters}
-      {.#Primitive name (list#each again parameters)}
-
-      (^template [<tag>]
-        [{<tag> left right}
-         {<tag> (again left) (again right)}])
-      ([.#Sum] [.#Product] [.#Function] [.#Apply])
-      
-      {.#Parameter index}
-      (if (n.= target index)
-        sub
-        base)
-
-      (^template [<tag>]
-        [{<tag> environment quantified}
-         {<tag> (list#each again environment) quantified}])
-      ([.#UnivQ] [.#ExQ])
-
-      _
-      base)))
-
-... Turns a record type into the kind of function type suitable for inference.
-(def: (record' record_size target originalT inferT)
-  (-> Nat Nat Type Type (Operation Type))
-  (case inferT
-    {.#Named name unnamedT}
-    (record' record_size target originalT unnamedT)
-
-    (^template [<tag>]
-      [{<tag> env bodyT}
-       (do ///.monad
-         [bodyT+ (record' record_size (n.+ 2 target) originalT bodyT)]
-         (in {<tag> env bodyT+}))])
-    ([.#UnivQ]
-     [.#ExQ])
-
-    {.#Apply inputT funcT}
-    (case (type.applied (list inputT) funcT)
-      {.#Some outputT}
-      (record' record_size target originalT outputT)
-
-      {.#None}
-      (/.except ..invalid_type_application inferT))
-
-    {.#Product _}
-    (let [[lefts right] (list.split_at (-- record_size) (type.flat_tuple inferT))]
-      (///#in (|> inferT
-                  (type.function (list#composite lefts (list (type.tuple right))))
-                  (substitute_bound target originalT))))
-
-    _
-    (/.except ..not_a_record_type inferT)))
-
-(def: .public (record record_size inferT)
-  (-> Nat Type (Operation Type))
-  (record' record_size (n.- 2 0) inferT inferT))
-
-... Turns a variant type into the kind of function type suitable for inference.
-(def: .public (variant tag expected_size inferT)
-  (-> Tag Nat Type (Operation Type))
-  (loop [depth 0
-         currentT inferT]
-    (case currentT
-      {.#Named name unnamedT}
-      (do ///.monad
-        [unnamedT+ (again depth unnamedT)]
-        (in unnamedT+))
-
-      (^template [<tag>]
-        [{<tag> env bodyT}
-         (do ///.monad
-           [bodyT+ (again (++ depth) bodyT)]
-           (in {<tag> env bodyT+}))])
-      ([.#UnivQ]
-       [.#ExQ])
-
-      {.#Sum _}
-      (let [cases (type.flat_variant currentT)
-            actual_size (list.size cases)
-            boundary (-- expected_size)]
-        (cond (or (n.= expected_size actual_size)
-                  (and (n.> expected_size actual_size)
-                       (n.< boundary tag)))
-              (case (list.item tag cases)
-                {.#Some caseT}
-                (///#in (if (n.= 0 depth)
-                          (type.function (list caseT) currentT)
-                          (let [replace' (replace (|> depth -- (n.* 2)) inferT)]
-                            (type.function (list (replace' caseT))
-                              (replace' currentT)))))
-
-                {.#None}
-                (/.except ..variant_tag_out_of_bounds [expected_size tag inferT]))
-              
-              (n.< expected_size actual_size)
-              (/.except ..smaller_variant_than_expected [expected_size actual_size])
-
-              (n.= boundary tag)
-              (let [caseT (type.variant (list.after boundary cases))]
-                (///#in (if (n.= 0 depth)
-                          (type.function (list caseT) currentT)
-                          (let [replace' (replace (|> depth -- (n.* 2)) inferT)]
-                            (type.function (list (replace' caseT))
-                              (replace' currentT))))))
-              
-              ... else
-              (/.except ..variant_tag_out_of_bounds [expected_size tag inferT])))
-
-      {.#Apply inputT funcT}
-      (case (type.applied (list inputT) funcT)
-        {.#Some outputT}
-        (variant tag expected_size outputT)
-
-        {.#None}
-        (/.except ..invalid_type_application inferT))
-
-      _
-      (/.except ..not_a_variant_type inferT))))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/structure.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/structure.lux
index 66cf6c80d..cdf65a6ad 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/structure.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/analysis/structure.lux
@@ -27,26 +27,18 @@
     ["[0]" check]]]]
  ["[0]" // "_"
   ["[1][0]" simple]
-  ["[1][0]" inference]
   ["/[1]" // "_"
    ["[1][0]" extension]
    [//
     ["/" analysis {"+" Analysis Operation Phase}
      ["[1][0]" complex {"+" Tag}]
-     ["[1][0]" type]]
+     ["[1][0]" type]
+     ["[1][0]" inference]]
     [///
      ["[1]" phase]
      [meta
       [archive {"+" Archive}]]]]]])
 
-(exception: .public (invalid_variant_type [type Type
-                                           tag Tag
-                                           code Code])
-  (exception.report
-   ["Type" (%.type type)]
-   ["Tag" (%.nat tag)]
-   ["Expression" (%.code code)]))
-
 (template [<name>]
   [(exception: .public (<name> [type Type
                                 members (List Code)])
@@ -59,7 +51,8 @@
   )
 
 (exception: .public (not_a_quantified_type [type Type])
-  (%.type type))
+  (exception.report
+   ["Type" (%.type type)]))
 
 (template [<name>]
   [(exception: .public (<name> [type Type
@@ -70,6 +63,7 @@
       ["Tag" (%.nat tag)]
       ["Expression" (%.code code)]))]
 
+  [invalid_variant_type]
   [cannot_analyse_variant]
   [cannot_infer_numeric_tag]
   )
@@ -78,7 +72,7 @@
   [(exception: .public (<name> [key Symbol
                                 record (List [Symbol Code])])
      (exception.report
-      ["Tag" (%.code (code.symbol key))]
+      ["Slot" (%.code (code.symbol key))]
       ["Record" (%.code (code.tuple (|> record
                                         (list#each (function (_ [keyI valC])
                                                      (list (code.symbol keyI) valC)))
@@ -90,7 +84,7 @@
 (exception: .public (slot_does_not_belong_to_record [key Symbol
                                                      type Type])
   (exception.report
-   ["Tag" (%.code (code.symbol key))]
+   ["Slot" (%.code (code.symbol key))]
    ["Type" (%.type type)]))
 
 (exception: .public (record_size_mismatch [expected Nat
@@ -117,16 +111,12 @@
         (/.with_stack ..cannot_analyse_variant [expectedT' tag valueC]
           (case expectedT
             {.#Sum _}
-            (let [flat (type.flat_variant expectedT)]
-              (case (list.item tag flat)
-                {.#Some variant_type}
-                (do !
-                  [valueA (<| (/type.expecting variant_type)
-                              (analyse archive valueC))]
-                  (in (/.variant [lefts right? valueA])))
-
-                {.#None}
-                (/.except //inference.variant_tag_out_of_bounds [(list.size flat) tag expectedT])))
+            (|> (analyse archive valueC)
+                (# ! each (|>> [lefts right?] /.variant))
+                (/type.expecting (|> expectedT
+                                     type.flat_variant
+                                     (list.item tag)
+                                     (maybe.else .Nothing))))
 
             {.#Named name unnamedT}
             (<| (/type.expecting unnamedT)
@@ -289,8 +279,8 @@
     (case expectedT
       {.#Var _}
       (do !
-        [inferenceT (//inference.variant idx case_size variantT)
-         [inferredT valueA+] (//inference.general archive analyse inferenceT (list valueC))]
+        [inferenceT (/inference.variant lefts right? variantT)
+         [inferredT valueA+] (/inference.general archive analyse inferenceT (list valueC))]
         (in (/.variant [lefts right? (|> valueA+ list.head maybe.trusted)])))
 
       _
@@ -430,8 +420,8 @@
               (case expectedT
                 {.#Var _}
                 (do !
-                  [inferenceT (//inference.record record_size recordT)
-                   [inferredT membersA] (//inference.general archive analyse inferenceT membersC)]
+                  [inferenceT (/inference.record record_size recordT)
+                   [inferredT membersA] (/inference.general archive analyse inferenceT membersC)]
                   (in (/.tuple membersA)))
 
                 _
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 2bc7d831e..b45be6e93 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
@@ -48,13 +48,13 @@
    ["[1][0]" bundle]
    ["/[1]" // "_"
     [analysis
-     ["[0]A" inference]
      ["[0]" scope]]
     ["/[1]" // "_"
      ["[1][0]" analysis {"+" Analysis Operation Phase Handler Bundle}
       ["[1]/[0]" complex]
       ["[1]/[0]" pattern]
-      ["[0]A" type]]
+      ["[0]A" type]
+      ["[0]A" inference]]
      ["[1][0]" synthesis]
      [///
       ["[0]" phase ("[1]#[0]" monad)]
@@ -1663,13 +1663,18 @@
 (def: .public protected_tag "protected")
 (def: .public default_tag "default")
 
+(def: .public visibility'
+  (<text>.Parser Visibility)
+  ($_ <>.or
+      (<text>.this ..public_tag)
+      (<text>.this ..private_tag)
+      (<text>.this ..protected_tag)
+      (<text>.this ..default_tag)
+      ))
+
 (def: .public visibility
   (Parser Visibility)
-  ($_ <>.or
-      (<code>.text! ..public_tag)
-      (<code>.text! ..private_tag)
-      (<code>.text! ..protected_tag)
-      (<code>.text! ..default_tag)))
+  (<text>.then ..visibility' <code>.text))
 
 (def: .public (visibility_analysis visibility)
   (-> Visibility Analysis)
@@ -1691,7 +1696,7 @@
    (Type Return)
    (List Exception)])
 
-(def: abstract_tag "abstract")
+(def: .public abstract_tag "abstract")
 
 (def: .public abstract_method_definition
   (Parser (Abstract_Method Code))
@@ -1796,9 +1801,9 @@
                                      (/////analysis.bit strict_fp?)
                                      (/////analysis.tuple (list#each annotation_analysis annotationsA))
                                      (/////analysis.tuple (list#each var_analysis vars))
+                                     (/////analysis.tuple (list#each class_analysis exceptions))
                                      (/////analysis.text self_name)
                                      (/////analysis.tuple (list#each ..argument_analysis arguments))
-                                     (/////analysis.tuple (list#each class_analysis exceptions))
                                      (/////analysis.tuple (list#each typed_analysis super_arguments))
                                      {/////analysis.#Function
                                       (list#each (|>> /////analysis.variable)
@@ -1819,7 +1824,7 @@
    (List Exception)
    a])
 
-(def: virtual_tag "virtual")
+(def: .public virtual_tag "virtual")
 
 (def: .public virtual_method_definition
   (Parser (Virtual_Method Code))
@@ -2070,7 +2075,7 @@
                   mapping
                   override_mapping))))
 
-(def: .public (hide_method_body arity bodyA)
+(def: .public (hidden_method_body arity bodyA)
   (-> Nat Analysis Analysis)
   (<| /////analysis.tuple
       (list (/////analysis.unit))
@@ -2145,7 +2150,7 @@
                                      {/////analysis.#Function
                                       (list#each (|>> /////analysis.variable)
                                                  (scope.environment scope))
-                                      (..hide_method_body (list.size arguments) bodyA)}
+                                      (..hidden_method_body (list.size arguments) bodyA)}
                                      ))))))
 
 (type: .public (Method_Definition a)
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/directive/jvm.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/directive/jvm.lux
index 8d23b355c..1e3b1eabc 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/directive/jvm.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/directive/jvm.lux
@@ -7,9 +7,11 @@
    [control
     [pipe {"+" case>}]
     ["[0]" try {"+" Try} ("[1]#[0]" functor)]
+    ["[0]" exception]
     ["<>" parser ("[1]#[0]" monad)
      ["<[0]>" code {"+" Parser}]
-     ["<[0]>" text]]]
+     ["<[0]>" text]
+     ["<[0]>" synthesis]]]
    [data
     [binary {"+" Binary}]
     ["[0]" product]
@@ -18,17 +20,19 @@
     [collection
      ["[0]" list ("[1]#[0]" functor mix)]
      ["[0]" dictionary]
-     ["[0]" sequence]]
+     ["[0]" sequence]
+     ["[0]" set {"+" Set}]]
     ["[0]" format "_"
      ["[1]" binary]]]
    [macro
     ["[0]" template]]
    [math
     [number
-     ["[0]" i32]]]
+     ["[0]" i32]
+     ["n" nat]]]
    [target
     [jvm
-     ["_" bytecode {"+" Bytecode}]
+     ["_" bytecode {"+" Bytecode} ("[1]#[0]" monad)]
      ["[0]" modifier {"+" Modifier} ("[1]#[0]" monoid)]
      ["[0]" attribute]
      ["[0]" field]
@@ -49,21 +53,28 @@
    [tool
     [compiler
      ["[0]" phase]
+     [reference
+      [variable {"+" Register}]]
      [meta
       [archive {"+" Archive}
        ["[0]" artifact]
-       ["[0]" unit]]]
+       ["[0]" unit]]
+      ["[0]" cache "_"
+       ["[1]" artifact]]]
      [language
       [lux
-       ["[0]" synthesis]
+       ["[0]" synthesis {"+" Synthesis}]
        ["[0]" generation]
        ["[0]" directive {"+" Handler Bundle}]
-       ["[0]" analysis
+       ["[0]" analysis {"+" Analysis}
         ["[0]A" type]]
        [phase
+        [analysis
+         ["[0]A" scope]]
         [generation
          [jvm
-          ["[0]" runtime {"+" Anchor Definition Extender}]]]
+          ["[0]" runtime {"+" Anchor Definition Extender}]
+          ["[0]" value]]]
         ["[0]" extension
          ["[0]" bundle]
          [analysis
@@ -93,17 +104,21 @@
               {ffi.#ProtectedP} method.protected
               {ffi.#DefaultP} modifier.empty)))
 
-(def: visibility
-  (Parser (Modifier field.Field))
+(def: visibility'
+  (<text>.Parser (Modifier field.Field))
   (`` ($_ <>.either
           (~~ (template [<label> <modifier>]
-                [(<>.after (<code>.text! <label>) (<>#in <modifier>))]
+                [(<>.after (<text>.this <label>) (<>#in <modifier>))]
 
                 ["public" field.public]
                 ["private" field.private]
                 ["protected" field.protected]
                 ["default" modifier.empty])))))
 
+(def: visibility
+  (Parser (Modifier field.Field))
+  (<text>.then ..visibility' <code>.text))
+
 (def: inheritance
   (Parser (Modifier class.Class))
   (`` ($_ <>.either
@@ -175,16 +190,16 @@
       ..variable
       ))
 
-(type: Method_Definition
+(type: (Method_Definition a)
   (Variant
-   {#Constructor (jvm.Constructor Code)}
-   {#Virtual_Method (jvm.Virtual_Method Code)}
-   {#Static_Method (jvm.Static_Method Code)}
-   {#Overriden_Method (jvm.Overriden_Method Code)}
-   {#Abstract_Method (jvm.Abstract_Method Code)}))
+   {#Constructor (jvm.Constructor a)}
+   {#Virtual_Method (jvm.Virtual_Method a)}
+   {#Static_Method (jvm.Static_Method a)}
+   {#Overriden_Method (jvm.Overriden_Method a)}
+   {#Abstract_Method (jvm.Abstract_Method a)}))
 
 (def: method
-  (Parser Method_Definition)
+  (Parser (Method_Definition Code))
   ($_ <>.or
       jvm.constructor_definition
       jvm.virtual_method_definition
@@ -236,17 +251,421 @@
     (field.field (modifier#composite visibility state)
                  name type true sequence.empty)))
 
-(def: (method_definition archive supers [mapping selfT] [analyse synthesize generate])
+(def: annotation_parameter_synthesis
+  (<synthesis>.Parser (jvm.Annotation_Parameter Synthesis))
+  (<synthesis>.tuple (<>.and <synthesis>.text <synthesis>.any)))
+
+(def: annotation_synthesis
+  (<synthesis>.Parser (jvm.Annotation Synthesis))
+  (<synthesis>.tuple (<>.and <synthesis>.text (<>.some ..annotation_parameter_synthesis))))
+
+(template [<name> <type> <text>]
+  [(def: <name>
+     (<synthesis>.Parser (Type <type>))
+     (<text>.then <text> <synthesis>.text))]
+
+  [value_type_synthesis Value parser.value]
+  [class_type_synthesis Class parser.class]
+  [var_type_synthesis Var parser.var]
+  [return_type_synthesis Return parser.return]
+  )
+
+(def: argument_synthesis
+  (<synthesis>.Parser Argument)
+  (<synthesis>.tuple (<>.and <synthesis>.text ..value_type_synthesis)))
+
+(def: input_synthesis
+  (<synthesis>.Parser (Typed Synthesis))
+  (<synthesis>.tuple (<>.and ..value_type_synthesis <synthesis>.any)))
+
+(def: (hidden_method_body arity body)
+  (-> Nat Synthesis Synthesis)
+  (case [arity body]
+    [0 _] body
+    [1 _] body
+    
+    [2 {synthesis.#Control {synthesis.#Branch {synthesis.#Let _ 2 hidden}}}]
+    hidden
+    
+    [_ {synthesis.#Control {synthesis.#Branch {synthesis.#Case _ path}}}]
+    (loop [path (: synthesis.Path path)]
+      (case path
+        (^or {synthesis.#Pop}
+             {synthesis.#Access _}
+             {synthesis.#Bind _}
+             {synthesis.#Bit_Fork _}
+             {synthesis.#I64_Fork _}
+             {synthesis.#F64_Fork _}
+             {synthesis.#Text_Fork _}
+             {synthesis.#Alt _})
+        body
+        
+        {synthesis.#Seq _ next}
+        (again next)
+        
+        {synthesis.#Then hidden}
+        hidden))
+
+    _
+    body))
+
+(def: (method_body arity)
+  (-> Nat (<synthesis>.Parser Synthesis))
+  (<| (<>#each (function (_ [env offset inits it]) it))
+      (<synthesis>.function 1)
+      (<synthesis>.loop (<>.exactly 0 <synthesis>.any))
+      <synthesis>.tuple
+      ($_ <>.either
+          (<| (<>.after (<synthesis>.text! ""))
+              (<>#each (..hidden_method_body arity))
+              <synthesis>.any)
+          <synthesis>.any)))
+
+(def: constructor_synthesis
+  (<synthesis>.Parser (jvm.Constructor Synthesis))
+  (<| <synthesis>.tuple
+      (<>.after (<synthesis>.text! jvm.constructor_tag))
+      ($_ <>.and
+          (<text>.then jvm.visibility' <synthesis>.text)
+          <synthesis>.bit
+          (<synthesis>.tuple (<>.some ..annotation_synthesis))
+          (<synthesis>.tuple (<>.some ..var_type_synthesis))
+          (<synthesis>.tuple (<>.some ..class_type_synthesis))
+          <synthesis>.text
+          (do <>.monad
+            [args (<synthesis>.tuple (<>.some ..argument_synthesis))]
+            ($_ <>.and
+                (in args)
+                (<synthesis>.tuple (<>.some ..input_synthesis))
+                (..method_body (list.size args))))
+          )))
+
+(def: overriden_method_synthesis
+  (<synthesis>.Parser (jvm.Overriden_Method Synthesis))
+  (<| <synthesis>.tuple
+      (<>.after (<synthesis>.text! jvm.overriden_tag))
+      ($_ <>.and
+          ..class_type_synthesis
+          <synthesis>.text
+          <synthesis>.bit
+          (<synthesis>.tuple (<>.some ..annotation_synthesis))
+          (<synthesis>.tuple (<>.some ..var_type_synthesis))
+          <synthesis>.text
+          (do <>.monad
+            [args (<synthesis>.tuple (<>.some ..argument_synthesis))]
+            ($_ <>.and
+                (in args)
+                ..return_type_synthesis
+                (<synthesis>.tuple (<>.some ..class_type_synthesis))
+                (..method_body (list.size args))))
+          )))
+
+(def: virtual_method_synthesis
+  (<synthesis>.Parser (jvm.Virtual_Method Synthesis))
+  (<| <synthesis>.tuple
+      (<>.after (<synthesis>.text! jvm.virtual_tag))
+      ($_ <>.and
+          <synthesis>.text
+          (<text>.then jvm.visibility' <synthesis>.text)
+          <synthesis>.bit
+          <synthesis>.bit
+          (<synthesis>.tuple (<>.some ..annotation_synthesis))
+          (<synthesis>.tuple (<>.some ..var_type_synthesis))
+          <synthesis>.text
+          (do <>.monad
+            [args (<synthesis>.tuple (<>.some ..argument_synthesis))]
+            ($_ <>.and
+                (in args)
+                ..return_type_synthesis
+                (<synthesis>.tuple (<>.some ..class_type_synthesis))
+                (..method_body (list.size args))))
+          )))
+
+(def: static_method_synthesis
+  (<synthesis>.Parser (jvm.Static_Method Synthesis))
+  (<| <synthesis>.tuple
+      (<>.after (<synthesis>.text! jvm.static_tag))
+      ($_ <>.and
+          <synthesis>.text
+          (<text>.then jvm.visibility' <synthesis>.text)
+          <synthesis>.bit
+          (<synthesis>.tuple (<>.some ..annotation_synthesis))
+          (<synthesis>.tuple (<>.some ..var_type_synthesis))
+          (do <>.monad
+            [args (<synthesis>.tuple (<>.some ..argument_synthesis))]
+            ($_ <>.and
+                (in args)
+                ..return_type_synthesis
+                (<synthesis>.tuple (<>.some ..class_type_synthesis))
+                (..method_body (list.size args))))
+          )))
+
+(def: abstract_method_synthesis
+  (<synthesis>.Parser (jvm.Abstract_Method Synthesis))
+  (<| <synthesis>.tuple
+      (<>.after (<synthesis>.text! jvm.abstract_tag))
+      ($_ <>.and
+          <synthesis>.text
+          (<text>.then jvm.visibility' <synthesis>.text)
+          (<synthesis>.tuple (<>.some ..annotation_synthesis))
+          (<synthesis>.tuple (<>.some ..var_type_synthesis))
+          (<synthesis>.tuple (<>.some ..argument_synthesis))
+          ..return_type_synthesis
+          (<synthesis>.tuple (<>.some ..class_type_synthesis))
+          )))
+
+(def: method_synthesis
+  (<synthesis>.Parser (Method_Definition Synthesis))
+  ($_ <>.or
+      ..constructor_synthesis
+      ..virtual_method_synthesis
+      ..static_method_synthesis
+      ..overriden_method_synthesis
+      ..abstract_method_synthesis
+      ))
+
+(def: composite
+  (-> (List (Bytecode Any)) (Bytecode Any))
+  (|>> list.reversed
+       (list#mix _.composite (_#in []))))
+
+(def: constructor_name
+  "<init>")
+
+(def: (method_argument lux_register argumentT jvm_register)
+  (-> Register (Type Value) Register [Register (Bytecode Any)])
+  (case (type.primitive? argumentT)
+    {.#Left argumentT}
+    [(n.+ 1 jvm_register)
+     (if (n.= lux_register jvm_register)
+       (_#in [])
+       ($_ _.composite
+           (_.aload jvm_register)
+           (_.astore lux_register)))]
+    
+    {.#Right argumentT}
+    (template.let [(wrap_primitive <shift> <load> <type>)
+                   [[(n.+ <shift> jvm_register)
+                     ($_ _.composite
+                         (<load> jvm_register)
+                         (value.wrap <type>)
+                         (_.astore lux_register))]]]
+      (`` (cond (~~ (template [<shift> <load> <type>]
+                      [(# type.equivalence = <type> argumentT)
+                       (wrap_primitive <shift> <load> <type>)]
+
+                      [1 _.iload type.boolean]
+                      [1 _.iload type.byte]
+                      [1 _.iload type.short]
+                      [1 _.iload type.int]
+                      [1 _.iload type.char]
+                      [1 _.fload type.float]
+                      [2 _.lload type.long]))
+
+                ... (# type.equivalence = type.double argumentT)
+                (wrap_primitive 2 _.dload type.double))))))
+
+(def: .public (method_arguments offset types)
+  (-> Nat (List (Type Value)) (Bytecode Any))
+  (|> types
+      list.enumeration
+      (list#mix (function (_ [lux_register type] [jvm_register before])
+                  (let [[jvm_register' after] (method_argument (n.+ offset lux_register) type jvm_register)]
+                    [jvm_register' ($_ _.composite before after)]))
+                (: [Register (Bytecode Any)] [offset (_#in [])]))
+      product.right))
+
+(def: (constructor_method_generation archive super_class method)
+  (-> Archive (Type Class) (jvm.Constructor Synthesis) (Operation (Resource Method)))
+  (<| (let [[privacy strict_floating_point? annotations method_tvars exceptions
+             self arguments constructor_argumentsS
+             bodyS] method])
+      (do [! phase.monad]
+        [generate directive.generation])
+      directive.lifted_generation
+      (do !
+        [constructor_argumentsG (monad.each ! (|>> product.right (generate archive))
+                                            constructor_argumentsS)
+         bodyG (generate archive bodyS)
+         .let [[super_name super_vars] (parser.read_class super_class)
+               super_constructorT (type.method [(list)
+                                                (list#each product.left constructor_argumentsS)
+                                                type.void
+                                                (list)])
+               argumentsT (list#each product.right arguments)]]
+        (in (method.method ($_ modifier#composite
+                               (..method_privacy privacy)
+                               (if strict_floating_point?
+                                 method.strict
+                                 modifier.empty))
+                           ..constructor_name
+                           (type.method [method_tvars argumentsT type.void exceptions])
+                           (list)
+                           {.#Some ($_ _.composite
+                                       (_.aload 0)
+                                       (..composite constructor_argumentsG)
+                                       (_.invokespecial super_class ..constructor_name super_constructorT)
+                                       (method_arguments 1 argumentsT)
+                                       bodyG
+                                       _.return
+                                       )})))))
+
+(def: (method_return returnT)
+  (-> (Type Return) (Bytecode Any))
+  (case (type.void? returnT)
+    {.#Right returnT}
+    _.return
+
+    {.#Left returnT}
+    (case (type.primitive? returnT)
+      {.#Left returnT}
+      (case (type.class? returnT)
+        {.#Some class_name}
+        ($_ _.composite
+            (_.checkcast returnT)
+            _.areturn)
+
+        {.#None}
+        _.areturn)
+      
+      {.#Right returnT}
+      (template.let [(unwrap_primitive <return> <type>)
+                     [($_ _.composite
+                          (value.unwrap <type>)
+                          <return>)]]
+        (`` (cond (~~ (template [<return> <type>]
+                        [(# type.equivalence = <type> returnT)
+                         (unwrap_primitive <return> <type>)]
+
+                        [_.ireturn type.boolean]
+                        [_.ireturn type.byte]
+                        [_.ireturn type.short]
+                        [_.ireturn type.int]
+                        [_.ireturn type.char]
+                        [_.freturn type.float]
+                        [_.lreturn type.long]))
+
+                  ... (# type.equivalence = type.double returnT)
+                  (unwrap_primitive _.dreturn type.double)))))))
+
+(def: (overriden_method_generation archive method)
+  (-> Archive (jvm.Overriden_Method Synthesis) (Operation (Resource Method)))
+  (do [! phase.monad]
+    [.let [[super method_name strict_floating_point? annotations
+            method_tvars self arguments returnJ exceptionsJ
+            bodyS] method]
+     generate directive.generation]
+    (directive.lifted_generation
+     (do !
+       [bodyG (generate archive bodyS)
+        .let [argumentsT (list#each product.right arguments)]]
+       (in (method.method ($_ modifier#composite
+                              method.public
+                              (if strict_floating_point?
+                                method.strict
+                                modifier.empty))
+                          method_name
+                          (type.method [method_tvars argumentsT returnJ exceptionsJ])
+                          (list)
+                          {.#Some ($_ _.composite
+                                      (method_arguments 1 argumentsT)
+                                      bodyG
+                                      (method_return returnJ))}))))))
+
+(def: (virtual_method_generation archive method)
+  (-> Archive (jvm.Virtual_Method Synthesis) (Operation (Resource Method)))
+  (do [! phase.monad]
+    [.let [[method_name privacy final? strict_floating_point? annotations method_tvars
+            self arguments returnJ exceptionsJ
+            bodyS] method]
+     generate directive.generation]
+    (directive.lifted_generation
+     (do !
+       [bodyG (generate archive bodyS)
+        .let [argumentsT (list#each product.right arguments)]]
+       (in (method.method ($_ modifier#composite
+                              (..method_privacy privacy)
+                              (if strict_floating_point?
+                                method.strict
+                                modifier.empty)
+                              (if final?
+                                method.final
+                                modifier.empty))
+                          method_name
+                          (type.method [method_tvars argumentsT returnJ exceptionsJ])
+                          (list)
+                          {.#Some ($_ _.composite
+                                      (method_arguments 1 argumentsT)
+                                      bodyG
+                                      (method_return returnJ))}))))))
+
+(def: (static_method_generation archive method)
+  (-> Archive (jvm.Static_Method Synthesis) (Operation (Resource Method)))
+  (do [! phase.monad]
+    [.let [[method_name privacy strict_floating_point? annotations method_tvars
+            arguments returnJ exceptionsJ
+            bodyS] method]
+     generate directive.generation]
+    (directive.lifted_generation
+     (do !
+       [bodyG (generate archive bodyS)
+        .let [argumentsT (list#each product.right arguments)]]
+       (in (method.method ($_ modifier#composite
+                              (..method_privacy privacy)
+                              method.static
+                              (if strict_floating_point?
+                                method.strict
+                                modifier.empty))
+                          method_name
+                          (type.method [method_tvars argumentsT returnJ exceptionsJ])
+                          (list)
+                          {.#Some ($_ _.composite
+                                      (method_arguments 0 argumentsT)
+                                      bodyG
+                                      (method_return returnJ))}))))))
+
+(def: (abstract_method_generation method)
+  (-> (jvm.Abstract_Method Synthesis) (Resource Method))
+  (let [[name privacy annotations variables
+         arguments return exceptions] method]
+    (method.method ($_ modifier#composite
+                       (..method_privacy privacy)
+                       method.abstract)
+                   name
+                   (type.method [variables (list#each product.right arguments) return exceptions])
+                   (list)
+                   {.#None})))
+
+(def: (method_generation archive super_class method)
+  (-> Archive (Type Class) (Method_Definition Synthesis) (Operation (Resource Method)))
+  (case method
+    {#Constructor method}
+    (..constructor_method_generation archive super_class method)
+    
+    {#Overriden_Method method}
+    (..overriden_method_generation archive method)
+    
+    {#Virtual_Method method}
+    (..virtual_method_generation archive method)
+    
+    {#Static_Method method}
+    (..static_method_generation archive method)
+
+    {#Abstract_Method method}
+    (# phase.monad in (..abstract_method_generation method))))
+
+(def: (method_definition archive super interfaces [mapping selfT] [analyse synthesize generate])
   (-> Archive
+      (Type Class)
       (List (Type Class))
       [Mapping .Type]
       [analysis.Phase
        synthesis.Phase
        (generation.Phase Anchor (Bytecode Any) Definition)]
-      (-> Method_Definition (Operation synthesis.Synthesis)))
+      (-> (Method_Definition Code) (Operation [(Set unit.ID) (Resource Method)])))
   (function (_ methodC)
     (do phase.monad
-      [methodA (: (Operation analysis.Analysis)
+      [methodA (: (Operation Analysis)
                   (directive.lifted_analysis
                    (case methodC
                      {#Constructor method}
@@ -259,12 +678,21 @@
                      (jvm.analyse_static_method analyse archive mapping method)
                      
                      {#Overriden_Method method}
-                     (jvm.analyse_overriden_method analyse archive selfT mapping supers method)
+                     (jvm.analyse_overriden_method analyse archive selfT mapping (list& super interfaces) method)
 
                      {#Abstract_Method method}
-                     (jvm.analyse_abstract_method analyse archive method))))]
-      (directive.lifted_synthesis
-       (synthesize archive methodA)))))
+                     (jvm.analyse_abstract_method analyse archive method))))
+       methodS (: (Operation Synthesis)
+                  (directive.lifted_synthesis
+                   (synthesize archive methodA)))
+       dependencies (directive.lifted_generation
+                     (cache.dependencies archive methodS))
+       methodS' (|> methodS
+                    list
+                    (<synthesis>.result ..method_synthesis)
+                    phase.lifted)
+       methodG (method_generation archive super methodS')]
+      (in [dependencies methodG]))))
 
 (def: class_name
   (|>> parser.read_class product.left name.internal))
@@ -335,11 +763,8 @@
                 ... type.boolean type.byte type.short type.int type.char
                 _.ireturn)))))
 
-(def: constructor_name
-  "<init>")
-
 (def: (mock_method super method)
-  (-> (Type Class) ..Method_Definition (Resource method.Method))
+  (-> (Type Class) (Method_Definition Code) (Resource method.Method))
   (case method
     {#Constructor [privacy strict_floating_point? annotations variables exceptions
                    self arguments constructor_arguments
@@ -419,7 +844,7 @@
 (def: (mock declaration super interfaces inheritance fields methods)
   (-> Declaration
       (Type Class) (List (Type Class))
-      (Modifier class.Class) (List ..Field) (List ..Method_Definition)
+      (Modifier class.Class) (List ..Field) (List (Method_Definition Code))
       (Try [External Binary]))
   (mock_class declaration super interfaces
               (list#each ..field_definition fields)
@@ -436,12 +861,12 @@
   [class_declaration [External (List (Type Var))] parser.declaration']
   )
 
-(def: (save_class! name bytecode)
-  (-> Text Binary (Operation Any))
+(def: (save_class! name bytecode dependencies)
+  (-> Text Binary (Set unit.ID) (Operation Any))
   (directive.lifted_generation
    (do [! phase.monad]
      [.let [artifact [name bytecode]]
-      artifact_id (generation.learn_custom name unit.none)
+      artifact_id (generation.learn_custom name dependencies)
       _ (generation.execute! artifact)
       _ (generation.save! artifact_id {.#Some name} artifact)
       _ (generation.log! (format "JVM Class " name))]
@@ -487,20 +912,15 @@
          .let [mapping (list#mix (function (_ [parameterJ parameterT] mapping)
                                    (dictionary.has (parser.name parameterJ) parameterT mapping))
                                  luxT.fresh
-                                 parameters)]
-         superT (directive.lifted_analysis
-                 (typeA.check (luxT.check (luxT.class mapping) (..signature super))))
-         interfaceT+ (directive.lifted_analysis
-                      (typeA.check (monad.each check.monad
-                                               (|>> ..signature (luxT.check (luxT.class mapping)))
-                                               interfaces)))
+                                 parameters)
+               selfT {.#Primitive name (list#each product.right parameters)}]
          state (extension.lifted phase.state)
-         .let [selfT {.#Primitive name (list#each product.right parameters)}]
-         methods (monad.each ! (..method_definition archive (list& super interfaces) [mapping selfT]
+         methods (monad.each ! (..method_definition archive super interfaces [mapping selfT]
                                                     [(value@ [directive.#analysis directive.#phase] state)
                                                      (value@ [directive.#synthesis directive.#phase] state)
                                                      (value@ [directive.#generation directive.#phase] state)])
                              methods)
+         .let [all_dependencies (cache.all (list#each product.left methods))]
          bytecode (<| (# ! each (format.result class.writer))
                       phase.lifted
                       (class.class version.v6_0
@@ -512,9 +932,9 @@
                                    (..class_name super)
                                    (list#each ..class_name interfaces)
                                    (list#each ..field_definition fields)
-                                   (list) ... (list#each ..method_definition methods)
+                                   (list#each product.right methods)
                                    sequence.empty))
-         _ (..save_class! name bytecode)]
+         _ (..save_class! name bytecode all_dependencies)]
         (in directive.no_requirements)))]))
 
 (def: (method_declaration (^open "/[0]"))
diff --git a/stdlib/source/library/lux/tool/compiler/meta/packager/ruby.lux b/stdlib/source/library/lux/tool/compiler/meta/packager/ruby.lux
index 3d7854861..658c0e886 100644
--- a/stdlib/source/library/lux/tool/compiler/meta/packager/ruby.lux
+++ b/stdlib/source/library/lux/tool/compiler/meta/packager/ruby.lux
@@ -35,7 +35,8 @@
     ["[0]" artifact]
     ["[0]" module]
     ["[0]" descriptor]
-    ["[0]" document {"+" Document}]]
+    ["[0]" document {"+" Document}]
+    ["[0]" unit]]
    ["[0]" cache "_"
     ["[1]/[0]" module {"+" Order}]
     ["[1]/[0]" artifact]]
@@ -43,11 +44,10 @@
     ["[1]" archive]]
    [//
     [language
-     ["$" lux
-      [generation {"+" Context}]]]]]])
+     ["$" lux]]]]])
 
 (def: (bundle_module module module_id necessary_dependencies output)
-  (-> descriptor.Module module.ID (Set Context) Output (Try (Maybe _.Statement)))
+  (-> descriptor.Module module.ID (Set unit.ID) Output (Try (Maybe _.Statement)))
   (do [! try.monad]
     []
     (case (|> output
@@ -81,7 +81,7 @@
   (|>> %.nat (text.suffix ".rb")))
 
 (def: (write_module mapping necessary_dependencies [module [module_id entry]] sink)
-  (-> (Dictionary descriptor.Module module.ID) (Set Context)
+  (-> (Dictionary descriptor.Module module.ID) (Set unit.ID)
       [descriptor.Module [module.ID (archive.Entry .Module)]]
       (List [module.ID [Text Binary]])
       (Try (List [module.ID [Text Binary]])))
diff --git a/stdlib/source/test/lux/ffi.jvm.lux b/stdlib/source/test/lux/ffi.jvm.lux
index ea54c56d7..f77fbc54f 100644
--- a/stdlib/source/test/lux/ffi.jvm.lux
+++ b/stdlib/source/test/lux/ffi.jvm.lux
@@ -1,35 +1,35 @@
 (.using
-  [library
-   [lux "*"
-    ["_" test {"+" Test}]
-    ["[0]" type ("[1]#[0]" equivalence)]
-    ["[0]" meta]
-    [abstract
-     [monad {"+" do}]]
-    [control
-     [pipe {"+" case>}]
-     ["[0]" try]
-     ["[0]" exception]
-     [parser
-      ["<[0]>" code]]]
-    [data
-     ["[0]" bit ("[1]#[0]" equivalence)]
-     ["[0]" text ("[1]#[0]" equivalence)
-      ["%" format {"+" format}]]
-     [collection
-      ["[0]" array {"+" Array}]]]
-    ["[0]" macro
-     [syntax {"+" syntax:}]
-     ["[0]" code]
-     ["[0]" template]]
-    [math
-     ["[0]" random {"+" Random}]
-     [number
-      ["n" nat]
-      ["i" int ("[1]#[0]" equivalence)]
-      ["f" frac ("[1]#[0]" equivalence)]]]]]
-  [\\library
-   ["[0]" /]])
+ [library
+  [lux "*"
+   ["_" test {"+" Test}]
+   ["[0]" type ("[1]#[0]" equivalence)]
+   ["[0]" meta]
+   [abstract
+    [monad {"+" do}]]
+   [control
+    [pipe {"+" case>}]
+    ["[0]" try]
+    ["[0]" exception]
+    [parser
+     ["<[0]>" code]]]
+   [data
+    ["[0]" bit ("[1]#[0]" equivalence)]
+    ["[0]" text ("[1]#[0]" equivalence)
+     ["%" format {"+" format}]]
+    [collection
+     ["[0]" array {"+" Array}]]]
+   ["[0]" macro
+    [syntax {"+" syntax:}]
+    ["[0]" code]
+    ["[0]" template]]
+   [math
+    ["[0]" random {"+" Random}]
+    [number
+     ["n" nat]
+     ["i" int ("[1]#[0]" equivalence)]
+     ["f" frac ("[1]#[0]" equivalence)]]]]]
+ [\\library
+  ["[0]" /]])
 
 (/.import: java/lang/Boolean)
 (/.import: java/lang/Long)
@@ -252,11 +252,11 @@
    (actual3 [] a)])
 
 (/.interface: test/TestInterface4
-  ([] actual4 [long long long] long))
+  ([] actual4 [long long] long))
 
 (/.import: test/TestInterface4
   ["[1]::[0]"
-   (actual4 [long long long] long)])
+   (actual4 [long long] long)])
 
 (def: for_interface
   Test
@@ -327,20 +327,20 @@
                             []
                             (test/TestInterface4
                              [] (actual4 self [actual_left long
-                                               actual_right long
-                                               _ long])
+                                               actual_right long])
                              long
                              (:as java/lang/Long
                                   (i.+ (:as Int actual_left)
                                        (:as Int actual_right)))))]
              (i.= expected
-                  (test/TestInterface4::actual4 left right right object/4)))]]
+                  (test/TestInterface4::actual4 left right object/4)))]]
     (_.cover [/.interface: /.object]
              (and example/0!
                   example/1!
                   example/2!
                   example/3!
-                  example/4!))))
+                  example/4!
+                  ))))
 
 (/.class: "final" test/TestClass0 [test/TestInterface0]
   ... Fields
@@ -464,8 +464,7 @@
   ... Methods
   (test/TestInterface4
    [] (actual4 self [actual_left long
-                     actual_right long
-                     _ long])
+                     actual_right long])
    long
    (:as java/lang/Long
         (i.+ (:as Int actual_left)
@@ -550,7 +549,7 @@
            (let [expected (i.+ left right)
                  object/8 (test/TestClass8::new)]
              (i.= expected
-                  (test/TestInterface4::actual4 left right right object/8)))]
+                  (test/TestInterface4::actual4 left right object/8)))]
 
      .let [random_long (: (Random java/lang/Long)
                           (# ! each (|>> (:as java/lang/Long))
diff --git a/stdlib/source/test/lux/macro/code.lux b/stdlib/source/test/lux/macro/code.lux
index 4c6eb7e38..ffa65358b 100644
--- a/stdlib/source/test/lux/macro/code.lux
+++ b/stdlib/source/test/lux/macro/code.lux
@@ -1,31 +1,31 @@
 (.using
-  [library
-   [lux "*"
-    ["_" test {"+" Test}]
-    [abstract
-     [monad {"+" do}]
-     [\\specification
-      ["$[0]" equivalence]]]
-    [control
-     ["[0]" try {"+" Try}]]
-    [data
-     ["[0]" product]
-     ["[0]" text]
-     [collection
-      ["[0]" list ("[1]#[0]" functor)]]]
-    [math
-     ["[0]" random {"+" Random} ("[1]#[0]" monad)]
-     [number
-      ["n" nat]]]
-    [meta
-     ["[0]" location]]
-    [tool
-     [compiler
-      [language
-       [lux
-        ["[0]" syntax]]]]]]]
-  [\\library
-   ["[0]" /]])
+ [library
+  [lux "*"
+   ["_" test {"+" Test}]
+   [abstract
+    [monad {"+" do}]
+    [\\specification
+     ["$[0]" equivalence]]]
+   [control
+    ["[0]" try {"+" Try}]]
+   [data
+    ["[0]" product]
+    ["[0]" text]
+    [collection
+     ["[0]" list ("[1]#[0]" functor)]]]
+   [math
+    ["[0]" random {"+" Random} ("[1]#[0]" monad)]
+    [number
+     ["n" nat]]]
+   [meta
+    ["[0]" location]]
+   [tool
+    [compiler
+     [language
+      [lux
+       ["[0]" syntax]]]]]]]
+ [\\library
+  ["[0]" /]])
 
 (def: random_text
   (Random Text)
@@ -78,10 +78,11 @@
    (function (_ replacement_simulation)
      (let [for_sequence (: (-> (-> (List Code) Code) (Random [Code Code]))
                            (function (_ to_code)
-                             (do [! random.monad]
-                               [parts (..random_sequence replacement_simulation)]
-                               (in [(to_code (list#each product.left parts))
-                                    (to_code (list#each product.right parts))]))))]
+                             (random.only (|>> product.left (# /.equivalence = original) not)
+                                          (do [! random.monad]
+                                            [parts (..random_sequence replacement_simulation)]
+                                            (in [(to_code (list#each product.left parts))
+                                                 (to_code (list#each product.right parts))])))))]
        ($_ random.either
            (random#in [original substitute])
            (do [! random.monad]
diff --git a/stdlib/source/test/lux/target/ruby.lux b/stdlib/source/test/lux/target/ruby.lux
index 281ffe594..ee6b63d1c 100644
--- a/stdlib/source/test/lux/target/ruby.lux
+++ b/stdlib/source/test/lux/target/ruby.lux
@@ -432,7 +432,8 @@
   Test
   (do [! random.monad]
     [float/0 random.safe_frac
-     $global (# ! each /.global (random.ascii/lower 10))]
+     $global (# ! each /.global (random.ascii/lower 10))
+     pattern (# ! each /.string (random.ascii/lower 11))]
     ($_ _.and
         (_.cover [/.global]
                  (expression (|>> (:as Text) (text#= "global-variable"))
@@ -461,6 +462,24 @@
         (_.cover [/.command_line_arguments]
                  (expression (|>> (:as Int) (i.= +0))
                              (/.the "length" /.command_line_arguments)))
+        (_.cover [/.last_string_matched]
+                 (expression (|>> (:as Bit))
+                             (|> ($_ /.then
+                                     (/.statement
+                                      (|> (/.manual "Regexp")
+                                          (/.new (list pattern) {.#None})
+                                          (/.do "match" (list pattern) {.#None})))
+                                     (/.return (/.= pattern /.last_string_matched)))
+                                 [(list)] (/.lambda {.#None})
+                                 (/.apply_lambda/* (list)))))
+        (_.cover [/.last_regexp_match]
+                 (expression (|>> (:as Bit))
+                             (|> (/.return (|> (/.manual "Regexp")
+                                               (/.new (list pattern) {.#None})
+                                               (/.do "match" (list pattern) {.#None})
+                                               (/.= /.last_regexp_match)))
+                                 [(list)] (/.lambda {.#None})
+                                 (/.apply_lambda/* (list)))))
         )))
 
 (def: test|local_var
diff --git a/stdlib/source/test/lux/test.lux b/stdlib/source/test/lux/test.lux
index b2334c7bc..feec778bb 100644
--- a/stdlib/source/test/lux/test.lux
+++ b/stdlib/source/test/lux/test.lux
@@ -1,25 +1,26 @@
 (.using
-  [library
-   [lux "*"
-    [abstract
-     [monad {"+" do}]]
-    [control
-     ["[0]" io]
-     ["[0]" exception]
-     [concurrency
-      ["[0]" async]
-      ["[0]" atom {"+" Atom}]]]
-    [data
-     ["[0]" text ("[1]#[0]" equivalence)]
-     [collection
-      ["[0]" list]
-      ["[0]" set]]]
-    [math
-     ["[0]" random]
-     [number
-      ["n" nat]]]]]
-  [\\library
-   ["[0]" /]])
+ [library
+  [lux "*"
+   [abstract
+    [monad {"+" do}]]
+   [control
+    ["[0]" io]
+    ["[0]" exception]
+    [concurrency
+     ["[0]" async]
+     ["[0]" atom {"+" Atom}]]]
+   [data
+    ["[0]" text ("[1]#[0]" equivalence)
+     ["%" format]]
+    [collection
+     ["[0]" list]
+     ["[0]" set]]]
+   [math
+    ["[0]" random]
+    [number
+     ["n" nat]]]]]
+ [\\library
+  ["[0]" /]])
 
 (def: (verify expected_message/0 expected_message/1 successes failures [tally message])
   (-> Text Text Nat Nat [/.Tally Text] Bit)
@@ -237,8 +238,8 @@
                     [[success_tally success_message] success_assertion
                      [failure_tally failure_message] failure_assertion]
                     (/.cover' [/.test]
-                              (and (text.ends_with? expected_message/0 success_message)
-                                   (text.ends_with? expected_message/0 failure_message)
+                              (and (text.ends_with? (%.text expected_message/0) success_message)
+                                   (text.ends_with? (%.text expected_message/0) failure_message)
                                    (and (n.= 1 (value@ /.#successes success_tally))
                                         (n.= 0 (value@ /.#failures success_tally)))
                                    (and (n.= 0 (value@ /.#successes failure_tally))
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/analysis.lux b/stdlib/source/test/lux/tool/compiler/language/lux/analysis.lux
index 8f6a7b381..ccca4213f 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/analysis.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis.lux
@@ -30,6 +30,7 @@
   ["[1][0]" macro]
   ["[1][0]" type]
   ["[1][0]" module]
+  ["[1][0]" inference]
   [////
    ["[1][0]" reference
     ["[2][0]" variable]]
@@ -442,4 +443,5 @@
             /macro.test
             /type.test
             /module.test
+            /inference.test
             ))))
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
new file mode 100644
index 000000000..672a8f25a
--- /dev/null
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
@@ -0,0 +1,406 @@
+(.using
+ [library
+  [lux "*"
+   ["_" test {"+" Test}]
+   [abstract
+    [monad {"+" do}]]
+   [control
+    ["[0]" maybe ("[1]#[0]" functor)]
+    ["[0]" try {"+" Try} ("[1]#[0]" functor)]
+    ["[0]" exception {"+" Exception}]]
+   [data
+    ["[0]" product]
+    ["[0]" bit ("[1]#[0]" equivalence)]
+    ["[0]" text]
+    [collection
+     ["[0]" list ("[1]#[0]" monad)]]]
+   [macro
+    ["[0]" code]]
+   [math
+    ["[0]" random {"+" Random} ("[1]#[0]" monad)]
+    [number
+     ["n" nat]]]
+   [meta
+    ["[0]" symbol "_"
+     ["$[1]" \\test]]]
+   ["[0]" type ("[1]#[0]" equivalence)
+    ["[0]" check {"+" Check}]]]]
+ [\\library
+  ["[0]" /
+   ["/[1]" //
+    [evaluation {"+" Eval}]
+    ["[1][0]" macro]
+    ["[1][0]" type]
+    ["[1][0]" module]
+    ["[1][0]" complex]
+    [//
+     [phase
+      ["[2][0]" analysis]
+      ["[2][0]" extension
+       ["[1]/[0]"analysis "_"
+        ["[1]" lux]]]]
+     [///
+      ["[2][0]" phase ("[1]#[0]" monad)]
+      [meta
+       ["[0]" archive]]]]]]])
+
+(def: (eval archive type term)
+  Eval
+  (/phase#in []))
+
+(def: (expander macro inputs state)
+  //macro.Expander
+  {try.#Success ((.macro macro) inputs state)})
+
+(def: random_state
+  (Random Lux)
+  (do random.monad
+    [version random.nat
+     host (random.ascii/lower 1)]
+    (in (//.state (//.info version host)))))
+
+(def: primitive
+  (Random Type)
+  (do random.monad
+    [name (random.ascii/lower 1)]
+    (in {.#Primitive name (list)})))
+
+(def: analysis
+  //.Phase
+  (/analysis.phase ..expander))
+
+(def: (fails? exception try)
+  (All (_ e a) (-> (Exception e) (Try a) Bit))
+  (case try
+    {try.#Success _}
+    false
+    
+    {try.#Failure error}
+    (text.contains? (value@ exception.#label exception) error)))
+
+(def: simple_parameter
+  (Random [Type Code])
+  (`` ($_ random.either
+          (~~ (template [<type> <random> <code>]
+                [(random#each (|>> <code> [<type>]) <random>)]
+
+                [.Bit random.bit code.bit]
+                [.Nat random.nat code.nat]
+                [.Int random.int code.int]
+                [.Rev random.rev code.rev]
+                [.Frac random.frac code.frac]
+                [.Text (random.ascii/lower 1) code.text]
+                ))
+          )))
+
+(def: test|general
+  Test
+  (do [! random.monad]
+    [lux ..random_state
+     .let [state [/extension.#bundle (/extension/analysis.bundle ..eval)
+                  /extension.#state lux]]
+     expected ..primitive
+     name ($symbol.random 1 1)
+     [type/0 term/0] ..simple_parameter
+     arity (# ! each (n.% 10) random.nat)
+     nats (random.list arity random.nat)]
+    ($_ _.and
+        (_.cover [/.general]
+                 (and (|> (/.general archive.empty ..analysis expected (list))
+                          (//type.expecting expected)
+                          (/phase.result state)
+                          (try#each (|>> product.left (type#= expected)))
+                          (try.else false))
+                      (|> (/.general archive.empty ..analysis
+                                     (type.function (list.repeated arity .Nat) expected)
+                                     (list#each code.nat nats))
+                          (//type.expecting expected)
+                          (/phase.result state)
+                          (try#each (function (_ [actual analysis/*])
+                                      (and (type#= expected actual)
+                                           (# (list.equivalence //.equivalence) =
+                                              (list#each (|>> //.nat) nats)
+                                              analysis/*))))
+                          (try.else false))
+                      (|> (/.general archive.empty ..analysis
+                                     (type (-> type/0 expected))
+                                     (list term/0))
+                          (//type.expecting expected)
+                          (/phase.result state)
+                          (try#each (|>> product.left (type#= expected)))
+                          (try.else false))
+                      (|> (/.general archive.empty ..analysis
+                                     (type {.#Named name (-> type/0 expected)})
+                                     (list term/0))
+                          (//type.expecting expected)
+                          (/phase.result state)
+                          (try#each (|>> product.left (type#= expected)))
+                          (try.else false))
+                      (|> (/.general archive.empty ..analysis
+                                     (type (All (_ a) (-> a a)))
+                                     (list term/0))
+                          (//type.expecting type/0)
+                          (/phase#each (|>> product.left check.clean //type.check))
+                          /phase#conjoint
+                          (/phase.result state)
+                          (try#each (type#= type/0))
+                          (try.else false))
+                      (|> (/.general archive.empty ..analysis
+                                     (type ((All (_ a) (-> a a)) type/0))
+                                     (list term/0))
+                          (//type.expecting type/0)
+                          (/phase.result state)
+                          (try#each (|>> product.left (type#= type/0)))
+                          (try.else false))
+                      (|> (do /phase.monad
+                            [[@var varT] (//type.check check.var)
+                             _ (//type.check (check.check varT (type (-> type/0 expected))))]
+                            (/.general archive.empty ..analysis varT (list term/0)))
+                          (//type.expecting expected)
+                          (/phase#each (|>> product.left check.clean //type.check))
+                          /phase#conjoint
+                          (/phase.result state)
+                          (try#each (type#= expected))
+                          (try.else false))
+                      ))
+        (_.cover [/.cannot_infer]
+                 (and (|> (/.general archive.empty ..analysis expected (list term/0))
+                          (//type.expecting expected)
+                          (/phase.result state)
+                          (..fails? /.cannot_infer))
+                      (|> (do /phase.monad
+                            [[@var varT] (//type.check check.var)]
+                            (/.general archive.empty ..analysis varT (list term/0)))
+                          (//type.expecting expected)
+                          (/phase.result state)
+                          (..fails? /.cannot_infer))))
+        (_.cover [/.cannot_infer_argument]
+                 (|> (/.general archive.empty ..analysis
+                                (type (-> expected expected))
+                                (list term/0))
+                     (//type.expecting expected)
+                     (/phase.result state)
+                     (..fails? /.cannot_infer_argument)))
+        (_.cover [/.existential?]
+                 (|> (/.general archive.empty ..analysis
+                                (type (Ex (_ a) (-> a a)))
+                                (list (` ("lux io error" ""))))
+                     //type.inferring
+                     (//module.with_module 0 (product.left name))
+                     (/phase#each (|>> product.right product.left check.clean //type.check))
+                     /phase#conjoint
+                     (/phase.result state)
+                     (try#each /.existential?)
+                     (try.else false)))
+        )))
+
+(def: test|variant
+  Test
+  (do [! random.monad]
+    [lux ..random_state
+     .let [state [/extension.#bundle (/extension/analysis.bundle ..eval)
+                  /extension.#state lux]]
+     name ($symbol.random 1 1)
+     arity (# ! each (|>> (n.% 5) (n.+ 2)) random.nat)
+     [type/0 term/0] ..simple_parameter
+     [type/1 term/1] (random.only (|>> product.left (same? type/0) not)
+                                  ..simple_parameter)
+     types/*,terms,* (random.list arity ..simple_parameter)
+     tag (# ! each (n.% arity) random.nat)
+     .let [[lefts right?] (//complex.choice arity tag)]
+     arbitrary_right? random.bit]
+    ($_ _.and
+        (_.cover [/.variant]
+                 (let [variantT (type.variant (list#each product.left types/*,terms,*))
+                       [tagT tagC] (|> types/*,terms,*
+                                       (list.item tag)
+                                       (maybe.else [Any (' [])]))
+                       variant?' (: (-> Type (Maybe Type) Nat Bit Code Bit)
+                                    (function (_ variant inferred lefts right? term)
+                                      (|> (do /phase.monad
+                                            [inferT (/.variant lefts right? variant)
+                                             [_ [it _]] (|> (/.general archive.empty ..analysis inferT (list term))
+                                                            //type.inferring)]
+                                            (case inferred
+                                              {.#Some inferred}
+                                              (//type.check
+                                               (do check.monad
+                                                 [_ (check.check inferred it)
+                                                  _ (check.check it inferred)]
+                                                 (in true)))
+                                              
+                                              {.#None}
+                                              (in true)))
+                                          (//module.with_module 0 (product.left name))
+                                          (/phase#each product.right)
+                                          (/phase.result state)
+                                          (try.else false))))
+                       variant? (: (-> Type Nat Bit Code Bit)
+                                   (function (_ type lefts right? term)
+                                     (variant?' type {.#Some type} lefts right? term)))
+
+                       can_match_case!
+                       (variant? variantT lefts right? tagC)
+
+                       names_do_not_matter!
+                       (variant? {.#Named name variantT} lefts right? tagC)
+
+                       cases_independent_of_parameters_conform_to_anything!
+                       (variant? (type (Maybe type/0)) 0 #0 (' []))
+
+                       cases_dependent_on_parameters_are_tettered_to_those_parameters!
+                       (and (variant? (type (Maybe type/0)) 0 #1 term/0)
+                            (not (variant? (type (Maybe type/0)) 0 #1 term/1)))
+
+                       only_bottom_conforms_to_tags_outside_of_range!
+                       (`` (and (~~ (template [<verdict> <term>]
+                                      [(bit#= <verdict> (variant? variantT arity arbitrary_right? <term>))]
+
+                                      [#0 term/0]
+                                      [#1 (` ("lux io error" ""))]))))
+
+                       can_handle_universal_quantification!
+                       (and (variant?' (type (All (_ a) (Maybe a)))
+                                       {.#Some Maybe}
+                                       0 #0 (' []))
+                            (variant?' (type (All (_ a) (Maybe a)))
+                                       {.#Some (type (Maybe type/0))}
+                                       0 #1 term/0)
+                            (not (variant?' (type (All (_ a) (Maybe a)))
+                                            {.#Some Maybe}
+                                            0 #1 term/0)))
+
+                       existential_types_do_not_affect_independent_cases!
+                       (variant?' (type (Ex (_ a) (Maybe a)))
+                                  {.#None}
+                                  0 #0 (' []))
+
+                       existential_types_affect_dependent_cases!
+                       (`` (and (~~ (template [<verdict> <term>]
+                                      [(bit#= <verdict> (variant?' (type (Ex (_ a) (Maybe a))) {.#None} 0 #1 <term>))]
+
+                                      [#0 term/0]
+                                      [#1 (` ("lux io error" ""))]))))]
+                   (and can_match_case!
+                        names_do_not_matter!
+
+                        cases_independent_of_parameters_conform_to_anything!
+                        cases_dependent_on_parameters_are_tettered_to_those_parameters!
+
+                        only_bottom_conforms_to_tags_outside_of_range!
+
+                        can_handle_universal_quantification!
+
+                        existential_types_do_not_affect_independent_cases!
+                        existential_types_affect_dependent_cases!
+                        )))
+        (_.cover [/.not_a_variant]
+                 (let [[tagT tagC] (|> types/*,terms,*
+                                       (list.item tag)
+                                       (maybe.else [Any (' [])]))]
+                   (|> (/.variant lefts right? tagT)
+                       (/phase.result state)
+                       (..fails? /.not_a_variant))))
+        )))
+
+(def: test|record
+  Test
+  (do [! random.monad]
+    [lux ..random_state
+     .let [state [/extension.#bundle (/extension/analysis.bundle ..eval)
+                  /extension.#state lux]]
+     name ($symbol.random 1 1)
+     arity (# ! each (|>> (n.% 5) (n.+ 2)) random.nat)
+     [type/0 term/0] ..simple_parameter
+     [type/1 term/1] (random.only (|>> product.left (same? type/0) not)
+                                  ..simple_parameter)
+     types/*,terms,* (random.list arity ..simple_parameter)
+     .let [record? (: (-> Type (Maybe Type) Nat (List Code) Bit)
+                      (function (_ record expected arity terms)
+                        (|> (do /phase.monad
+                              [inference (/.record arity record)
+                               [_ [it _]] (|> (/.general archive.empty ..analysis inference terms)
+                                              //type.inferring)]
+                              (case expected
+                                {.#Some expected}
+                                (//type.check
+                                 (do check.monad
+                                   [_ (check.check expected it)
+                                    _ (check.check it expected)]
+                                   (in true)))
+                                
+                                {.#None}
+                                (in true)))
+                            (//module.with_module 0 (product.left name))
+                            (/phase#each product.right)
+                            (/phase.result state)
+                            (try.else false))))
+           record (type.tuple (list#each product.left types/*,terms,*))
+           terms (list#each product.right types/*,terms,*)]]
+    ($_ _.and
+        (_.cover [/.record]
+                 (let [can_infer_record!
+                       (record? record {.#None} arity terms)
+
+                       names_do_not_matter!
+                       (record? {.#Named name record} {.#None} arity terms)
+
+                       can_handle_universal_quantification!
+                       (and (record? (All (_ a) (Tuple type/0 a))
+                                     {.#Some (Tuple type/0 type/1)}
+                                     2 (list term/0 term/1))
+                            (record? (All (_ a) (Tuple a type/0))
+                                     {.#Some (Tuple type/1 type/0)}
+                                     2 (list term/1 term/0)))
+
+                       can_handle_existential_quantification!
+                       (and (not (record? (Ex (_ a) (Tuple type/0 a))
+                                          {.#Some (Tuple type/0 type/1)}
+                                          2 (list term/0 term/1)))
+                            (record? (Ex (_ a) (Tuple type/0 a))
+                                     {.#None}
+                                     2 (list term/0 (` ("lux io error" ""))))
+                            (not (record? (Ex (_ a) (Tuple a type/0))
+                                          {.#Some (Tuple type/1 type/0)}
+                                          2 (list term/1 term/0)))
+                            (record? (Ex (_ a) (Tuple a type/0))
+                                     {.#None}
+                                     2 (list (` ("lux io error" "")) term/0)))]
+                   (and can_infer_record!
+                        names_do_not_matter!
+                        can_handle_universal_quantification!
+                        can_handle_existential_quantification!
+                        )))
+        (_.cover [/.not_a_record]
+                 (|> (/.record arity type/0)
+                     (/phase.result state)
+                     (..fails? /.not_a_record)))
+        )))
+
+(def: .public test
+  Test
+  (<| (_.covering /._)
+      (do [! random.monad]
+        [lux ..random_state
+         .let [state [/extension.#bundle (/extension/analysis.bundle ..eval)
+                      /extension.#state lux]]
+         [type/0 term/0] ..simple_parameter
+         [type/1 term/1] (random.only (|>> product.left (same? type/0) not)
+                                      ..simple_parameter)
+         lefts (# ! each (n.% 10) random.nat)
+         right? random.bit]
+        ($_ _.and
+            ..test|general
+            ..test|variant
+            ..test|record
+            (_.cover [/.invalid_type_application]
+                     (and (|> (/.general archive.empty ..analysis (type (type/0 type/1)) (list term/0))
+                              (/phase.result state)
+                              (..fails? /.invalid_type_application))
+                          (|> (/.variant lefts right? (type (type/0 type/1)))
+                              (/phase.result state)
+                              (..fails? /.invalid_type_application))
+                          (|> (/.record lefts (type (type/0 type/1)))
+                              (/phase.result state)
+                              (..fails? /.invalid_type_application))))
+            ))))
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/type.lux b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/type.lux
index 66876be3c..781a7f38f 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/type.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/type.lux
@@ -2,35 +2,17 @@
  [library
   [lux "*"
    ["_" test {"+" Test}]
-   ["[0]" meta]
    [abstract
-    [monad {"+" do}]
-    [\\specification
-     ["$[0]" equivalence]]]
+    [monad {"+" do}]]
    [control
     [pipe {"+" case>}]
-    ["[0]" maybe ("[1]#[0]" functor)]
-    ["[0]" try ("[1]#[0]" functor)]
-    ["[0]" exception]]
+    ["[0]" try ("[1]#[0]" functor)]]
    [data
-    ["[0]" product]
-    ["[0]" bit ("[1]#[0]" equivalence)]
-    ["[0]" text ("[1]#[0]" equivalence)]
-    [collection
-     ["[0]" list ("[1]#[0]" monad)]]]
-   [macro
-    ["[0]" code ("[1]#[0]" equivalence)]]
+    ["[0]" product]]
    [math
-    ["[0]" random {"+" Random} ("[1]#[0]" monad)]
-    [number
-     ["n" nat]]]
+    ["[0]" random {"+" Random}]]
    ["[0]" type ("[1]#[0]" equivalence)
     ["[0]" check]]]]
- ["$" /////// "_"
-  [macro
-   ["[1][0]" code]]
-  [meta
-   ["[1][0]" symbol]]]
  [\\library
   ["[0]" /
    ["/[1]" //
diff --git a/stdlib/source/test/lux/world.lux b/stdlib/source/test/lux/world.lux
index f705e6269..e57811f1a 100644
--- a/stdlib/source/test/lux/world.lux
+++ b/stdlib/source/test/lux/world.lux
@@ -1,21 +1,21 @@
 (.using
-  [library
-   [lux "*"
-    ["_" test {"+" Test}]]]
-  ["[0]" / "_"
-   ["[1][0]" file]
-   ["[1][0]" shell]
-   ["[1][0]" console]
-   ["[1][0]" program]
-   ["[1][0]" input "_"
-    ["[1]/[0]" keyboard]]
-   ["[1][0]" output "_"
-    ["[1]/[0]" video "_"
-     ["[1]/[0]" resolution]]]
-   ["[1][0]" net "_"
-    ["[1]/[0]" http "_"
-     ["[1]/[0]" client]
-     ["[1]/[0]" status]]]])
+ [library
+  [lux "*"
+   ["_" test {"+" Test}]]]
+ ["[0]" / "_"
+  ["[1][0]" file]
+  ["[1][0]" shell]
+  ["[1][0]" console]
+  ["[1][0]" program]
+  ["[1][0]" input "_"
+   ["[1]/[0]" keyboard]]
+  ["[1][0]" output "_"
+   ["[1]/[0]" video "_"
+    ["[1]/[0]" resolution]]]
+  ["[1][0]" net "_"
+   ["[1]/[0]" http "_"
+    ["[1]/[0]" client]
+    ["[1]/[0]" status]]]])
 
 (def: .public test
   Test
diff --git a/stdlib/source/test/lux/world/file/watch.lux b/stdlib/source/test/lux/world/file/watch.lux
index 0a9a742fb..cd7c95c46 100644
--- a/stdlib/source/test/lux/world/file/watch.lux
+++ b/stdlib/source/test/lux/world/file/watch.lux
@@ -1,29 +1,29 @@
 (.using
-  [library
-   [lux "*"
-    ["_" test {"+" Test}]
-    [abstract
-     [predicate {"+" Predicate}]
-     [monad {"+" do}]]
-    [control
-     ["[0]" try {"+" Try}]
-     ["[0]" exception]
-     [concurrency
-      ["[0]" async {"+" Async}]]]
-    [data
-     ["[0]" binary {"+" Binary} ("[1]#[0]" equivalence)]
-     ["[0]" text ("[1]#[0]" equivalence)
-      ["%" format {"+" format}]]
-     [collection
-      ["[0]" list]]]
-    [math
-     ["[0]" random {"+" Random} ("[1]#[0]" monad)]]]]
-  [\\library
-   ["[0]" /
-    ["/[1]" //]]]
-  [////
+ [library
+  [lux "*"
+   ["_" test {"+" Test}]
+   [abstract
+    [predicate {"+" Predicate}]
+    [monad {"+" do}]]
+   [control
+    ["[0]" try {"+" Try}]
+    ["[0]" exception]
+    [concurrency
+     ["[0]" async {"+" Async}]]]
    [data
-    ["$[0]" binary]]])
+    ["[0]" binary {"+" Binary} ("[1]#[0]" equivalence)]
+    ["[0]" text ("[1]#[0]" equivalence)
+     ["%" format {"+" format}]]
+    [collection
+     ["[0]" list]]]
+   [math
+    ["[0]" random {"+" Random} ("[1]#[0]" monad)]]]]
+ [\\library
+  ["[0]" /
+   ["/[1]" //]]]
+ [////
+  [data
+   ["$[0]" binary]]])
 
 (def: concern
   (Random [/.Concern (Predicate /.Concern)])
@@ -35,35 +35,34 @@
 
 (def: concern##test
   Test
-  (<| (_.for [/.Concern])
-      ($_ _.and
-          (_.cover [/.creation /.creation?]
-                   (and (/.creation? /.creation)
-                        (not (/.creation? /.modification))
-                        (not (/.creation? /.deletion))))
-          (_.cover [/.modification /.modification?]
-                   (and (not (/.modification? /.creation))
-                        (/.modification? /.modification)
-                        (not (/.modification? /.deletion))))
-          (_.cover [/.deletion /.deletion?]
-                   (and (not (/.deletion? /.creation))
-                        (not (/.deletion? /.modification))
-                        (/.deletion? /.deletion)))
-          (do random.monad
-            [left ..concern
-             right (random.only (|>> (same? left) not)
-                                ..concern)
-             .let [[left left?] left
-                   [right right?] right]]
-            (_.cover [/.also]
-                     (let [composition (/.also left right)]
-                       (and (left? composition)
-                            (right? composition)))))
-          (_.cover [/.all]
-                   (and (/.creation? /.all)
-                        (/.modification? /.all)
-                        (/.deletion? /.all)))
-          )))
+  ($_ _.and
+      (_.cover [/.creation /.creation?]
+               (and (/.creation? /.creation)
+                    (not (/.creation? /.modification))
+                    (not (/.creation? /.deletion))))
+      (_.cover [/.modification /.modification?]
+               (and (not (/.modification? /.creation))
+                    (/.modification? /.modification)
+                    (not (/.modification? /.deletion))))
+      (_.cover [/.deletion /.deletion?]
+               (and (not (/.deletion? /.creation))
+                    (not (/.deletion? /.modification))
+                    (/.deletion? /.deletion)))
+      (do random.monad
+        [left ..concern
+         right (random.only (|>> (same? left) not)
+                            ..concern)
+         .let [[left left?] left
+               [right right?] right]]
+        (_.cover [/.also]
+                 (let [composition (/.also left right)]
+                   (and (left? composition)
+                        (right? composition)))))
+      (_.cover [/.all]
+               (and (/.creation? /.all)
+                    (/.modification? /.all)
+                    (/.deletion? /.all)))
+      ))
 
 (def: exception
   Test
@@ -154,7 +153,8 @@
   (<| (_.covering /._)
       (_.for [/.Watcher])
       ($_ _.and
-          ..concern##test
+          (_.for [/.Concern]
+                 ..concern##test)
           ..exception
 
           (do [! random.monad]