From 2308e87dda7dc03190394f20a5a4916a5fb01027 Mon Sep 17 00:00:00 2001
From: Eduardo Julian <eduardoejp@gmail.com>
Date: Sun, 12 May 2024 01:50:48 -0400
Subject: [PATCH] New type for `Type` (part 9).

---
 stdlib/source/library/lux/control/pattern.lux |   3 +-
 stdlib/source/library/lux/documentation.lux   |  92 +++++----
 stdlib/source/library/lux/ffi/export.jvm.lux  |   3 +-
 stdlib/source/library/lux/time/solar.lux      |   2 +-
 stdlib/source/library/lux/type/implicit.lux   |  10 +-
 stdlib/source/library/lux/type/poly.lux       |  32 ++--
 stdlib/source/library/lux/type/record.lux     |   2 +-
 stdlib/source/library/lux/type/row.lux        |   2 +-
 stdlib/source/library/lux/web/html.lux        |   2 +-
 .../source/polytypic/lux/abstract/functor.lux |   6 +-
 stdlib/source/projection/lux/type.lux         |  95 +++++-----
 stdlib/source/test/lux.lux                    |   9 +-
 .../source/test/lux/data/collection/array.lux |   8 +-
 stdlib/source/test/lux/meta.lux               |   8 +-
 stdlib/source/test/lux/meta/binding.lux       |   6 +-
 stdlib/source/test/lux/meta/binding/local.lux |  10 +-
 stdlib/source/test/lux/meta/label.lux         |  19 +-
 stdlib/source/test/lux/meta/module.lux        |   2 +-
 stdlib/source/test/lux/meta/module/import.lux |   2 +-
 stdlib/source/test/lux/type.lux               |  71 +++----
 stdlib/source/test/lux/type/check.lux         | 175 ++++++++++--------
 21 files changed, 294 insertions(+), 265 deletions(-)

diff --git a/stdlib/source/library/lux/control/pattern.lux b/stdlib/source/library/lux/control/pattern.lux
index c650b09caa..10d4e28776 100644
--- a/stdlib/source/library/lux/control/pattern.lux
+++ b/stdlib/source/library/lux/control/pattern.lux
@@ -9,7 +9,8 @@
                 or and
                 is has
                 try with when
-                match?)
+                match?
+                abstraction)
    [abstract
     [equivalence (.only Equivalence)]]
    [control
diff --git a/stdlib/source/library/lux/documentation.lux b/stdlib/source/library/lux/documentation.lux
index 632c4af726..19f199c0dc 100644
--- a/stdlib/source/library/lux/documentation.lux
+++ b/stdlib/source/library/lux/documentation.lux
@@ -58,7 +58,7 @@
 
 (the |recursion_dummy|
   (template.macro (_)
-    [{.#Nominal "" {.#Empty}}]))
+    [{.#Nominal "" (list)}]))
 
 (.every Fragment
   (Variant
@@ -264,30 +264,21 @@
   (-> Natural Text Bit Text Type
       Text)
   (`` (when type
-        {.#Nominal name params}
-        (|> params
-            (stack#each (|>> (%type' level type_function_name false module)
-                             (text " ")))
-            {.#Top (%.text name)}
-            list.of_stack
-            text.together
-            (text.enclosed ["(Nominal " ")"]))
-
-        {.#Sum _}
+        (type.Sum left right)
         (|> type
             type.flat_variant
             (list#each (%type' level type_function_name false module))
             (text.interposed " ")
             (text.enclosed ["(Or " ")"]))
 
-        {.#Product _}
+        (type.Product left right)
         (|> type
             type.flat_tuple
             (list#each (%type' level type_function_name false module))
             (text.interposed " ")
             (text.enclosed ["[" "]"]))
 
-        {.#Function input output}
+        (type.Function input output)
         (let [[ins out] (type.flat_function type)]
           (text  "(-> "
                  (|> ins
@@ -297,7 +288,15 @@
                  (%type' level type_function_name false module out)
                  ")"))
 
-        {.#Parameter idx}
+        {.#Nominal name params}
+        (|> params
+            (list#each (function (_ [polarity it])
+                         (%type' level type_function_name false module it)))
+            (text.interposed " ")
+            (text (%.text name) " ")
+            (text.enclosed ["(Nominal " ")"]))
+
+        {.#Parameter parameter idx}
         (parameter_name [type_function_name (stack)] level idx)
 
         (,, (template.with [<tag>]
@@ -308,7 +307,7 @@
               [.#Opaque]))
 
         (,, (template.with [<tag> <name> <flat>]
-              [{<tag> _}
+              [{.#Quantification <tag> _}
                (let [[level' body] (<flat> type)
                      args (level_parameters level level')
                      body_doc (%type' (n.+ level level') type_function_name nestable? module body)]
@@ -318,13 +317,13 @@
                            (text " " body_doc))
                        ")"))]
 
-              [.#Universal "All" type.flat_univ_q]
-              [.#Existential "Ex" type.flat_ex_q]))
+              [.universal "All" type.flat_univ_q]
+              [.existential "Ex" type.flat_ex_q]))
 
-        {.#Reification (|recursion_dummy|) {.#Parameter 0}}
+        {.#Reification (|recursion_dummy|) {.#Parameter .abstraction 0}}
         type_function_name
 
-        {.#Reification (|recursion_dummy|) {.#Universal _ body}}
+        {.#Reification (|recursion_dummy|) {.#Quantification .universal _ body}}
         (text "(Rec " type_function_name
               \n (nested " " (%type' level type_function_name nestable? module body))
               ")")
@@ -352,7 +351,7 @@
   (when arity
     0 {.#Some type}
     _ (when type
-        {.#Universal _env _type}
+        {.#Quantification .universal _env _type}
         (parameterized_type (-- arity) _type)
 
         _
@@ -368,22 +367,7 @@
 
         _
         (when type
-          {.#Nominal name params}
-          (when params
-            {.#Empty}
-            (text "(Nominal " (%.text name) ")")
-
-            _
-            (text "(Nominal "
-                  (%.text name)
-                  " "
-                  (|> params
-                      list.of_stack
-                      (list#each (type_definition' false level arity type_function_info {.#None} module))
-                      (text.interposed " "))
-                  ")"))
-
-          {.#Sum _}
+          (type.Sum _ _)
           (let [members (type.flat_variant type)]
             (when tags
               {.#Empty}
@@ -398,7 +382,7 @@
                   (list.zipped_2 (list.of_stack tags))
                   (list#each (function (_ [t_name type])
                                (when type
-                                 {.#Product _}
+                                 (type.Product _ _)
                                  (let [types (type.flat_tuple type)]
                                    (text " {" t_name " "
                                          (|> types
@@ -411,7 +395,7 @@
                   (text.interposed \n)
                   (text.enclosed [(text "(Variant" \n) ")"]))))
 
-          {.#Product _}
+          (type.Product _ _)
           (let [members (type.flat_tuple type)]
             (when tags
               {.#Empty}
@@ -430,7 +414,7 @@
                   (text.enclosed [" [" "]"])
                   (text.enclosed [(text "(Record" \n) ")"]))))
 
-          {.#Function input output}
+          (type.Function input output)
           (let [[ins out] (type.flat_function type)]
             (text  "(-> "
                    (|> ins
@@ -440,7 +424,20 @@
                    (type_definition' false level arity type_function_info {.#None} module out)
                    ")"))
 
-          {.#Parameter idx}
+          {.#Nominal name params}
+          (|> (when params
+                (list)
+                (%.text name)
+
+                _
+                (|> params
+                    (list#each (function (_ [polarity it])
+                                 (type_definition' false level arity type_function_info {.#None} module it)))
+                    (text.interposed " ")
+                    (text (%.text name) " ")))
+              (text.enclosed ["(Nominal " ")"]))
+
+          {.#Parameter parameter idx}
           (parameter_name type_function_info level idx)
 
           (,, (template.with [<pre> <tag>]
@@ -451,7 +448,7 @@
                 ["+" .#Opaque]))
 
           (,, (template.with [<tag> <name> <flat>]
-                [{<tag> _}
+                [{.#Quantification <tag> _}
                  (let [[level' body] (<flat> type)
                        args (level_parameters (n.- arity level) level')
                        body_doc (type_definition' nestable? (n.+ level level') arity type_function_info tags module body)
@@ -464,14 +461,14 @@
                              (text " " body_doc))
                          ")"))]
 
-                [.#Universal "All" type.flat_univ_q]
-                [.#Existential "Ex" type.flat_ex_q]))
+                [.universal "All" type.flat_univ_q]
+                [.existential "Ex" type.flat_ex_q]))
 
           ... Recursive call
-          {.#Reification (|recursion_dummy|) {.#Parameter 0}}
+          {.#Reification (|recursion_dummy|) {.#Parameter .abstraction 0}}
           (product.left type_function_info)
 
-          {.#Reification (|recursion_dummy|) {.#Universal _ body}}
+          {.#Reification (|recursion_dummy|) {.#Quantification .universal _ body}}
           (|> (type_definition' nestable? level arity type_function_info tags module body)
               (text.all_split_by \n)
               (list#each (text.prefix " "))
@@ -566,9 +563,8 @@
                                            (, 'module)
                                            [(, (code.text (product.right name))) (stack (,* (list#each code.text parameters)))]
                                            (.stack (,* (|> tags
-                                                           (try.else (stack))
-                                                           (stack#each (|>> name.proper code.text))
-                                                           list.of_stack))))
+                                                           (try.else (list))
+                                                           (list#each (|>> name.proper code.text))))))
                                           (text "... " ((debug.private ..type_documentation) (, 'module) (, 'type)) text.\n)
                                           md.raw_code))
                                    (` (md.raw_code ((debug.private ..type_documentation) (, 'module) (, 'type))))))))
diff --git a/stdlib/source/library/lux/ffi/export.jvm.lux b/stdlib/source/library/lux/ffi/export.jvm.lux
index 356efcf5bf..29ed51aaa4 100644
--- a/stdlib/source/library/lux/ffi/export.jvm.lux
+++ b/stdlib/source/library/lux/ffi/export.jvm.lux
@@ -3,8 +3,7 @@
 
 (.using
  [library
-  [lux (.except #Function
-                function)
+  [lux (.except function)
    [abstract
     ["<>" projection]]
    [data
diff --git a/stdlib/source/library/lux/time/solar.lux b/stdlib/source/library/lux/time/solar.lux
index 705557ae8d..50159e67ca 100644
--- a/stdlib/source/library/lux/time/solar.lux
+++ b/stdlib/source/library/lux/time/solar.lux
@@ -3,7 +3,7 @@
 
 (.using
  [library
-  [lux (.except)
+  [lux (.except universal)
    ["[0]" ffi]
    [abstract
     [monad (.only do)]]
diff --git a/stdlib/source/library/lux/type/implicit.lux b/stdlib/source/library/lux/type/implicit.lux
index 610d6c1bfd..a17aa78a73 100644
--- a/stdlib/source/library/lux/type/implicit.lux
+++ b/stdlib/source/library/lux/type/implicit.lux
@@ -89,7 +89,7 @@
       {.#Some sig_type'}
       (member_type idx sig_type'))
 
-    {.#Product left right}
+    (//.Product left right)
     (if (n.= 0 idx)
         (by check.monad in left)
         (member_type (-- idx) right))
@@ -112,7 +112,11 @@
                    [[this_module_name _] module.current
                     imp_mods (import.all this_module_name)
                     tag_stacks (list.each' ! label.tag_stacks imp_mods)
-                    .let [tag_stacks (|> tag_stacks list.as_stack stack#conjoint (stack#each product.left) stack#conjoint)
+                    .let [tag_stacks (|> tag_stacks
+                                         list.as_stack
+                                         stack#conjoint
+                                         (stack#each (|>> product.left list.as_stack))
+                                         stack#conjoint)
                           candidates (stack.only (|>> product.right (text.= simple_name))
                                                  tag_stacks)]]
                    (when candidates
@@ -230,7 +234,7 @@
           maybe.trusted
           (on_argument arg)))
 
-    {.#Function input output}
+    (//.Function input output)
     (do check.monad
       [_ (check.check input arg)]
       (in output))
diff --git a/stdlib/source/library/lux/type/poly.lux b/stdlib/source/library/lux/type/poly.lux
index 924c751f79..f2f9cab7f2 100644
--- a/stdlib/source/library/lux/type/poly.lux
+++ b/stdlib/source/library/lux/type/poly.lux
@@ -72,7 +72,7 @@
 
 (the recursion_parameter
   (template.macro (_)
-    [{.#Nominal "" {.#Empty}}]))
+    [{.#Nominal "" (.list)}]))
 
 (the recursive
   (template.macro (_ ,type)
@@ -82,21 +82,21 @@
 (the recursion
   (template.macro (_)
     [{.#Reification (..recursion_parameter)
-                    {.#Parameter 0}}]))
+                    {.#Parameter .abstraction 0}}]))
 
 (the polymorphic
   (template.macro (_ ,name ,non_quantified)
     [{.#Named ,name {.#Quantification .universal (stack) ,non_quantified}}]))
 
 (every Context
-  (Dictionary Natural Code))
+  (Dictionary Natural [Code Code]))
 
 (the empty
   Context
   (dictionary.empty n.hash))
 
 (the (has solution it)
-  (-> Code
+  (-> [Code Code]
       (-> Context Context))
   (dictionary.has (dictionary.size it) solution it))
 
@@ -105,9 +105,7 @@
       (-> Context Context))
   (let [[_ it] (list#mix (function (_ next [previous it])
                            [(list#composite previous (list next))
-                            (|> it
-                                (has (` ((, successor) (,* previous))))
-                                (has next))])
+                            (has [(` ((, successor) (,* previous))) next] it)])
                          [(is (List Code) (list)) it]
                          predecessors)]
     it))
@@ -184,24 +182,24 @@
 
                      {.#None}
                      (when it
-                       {.#Sum sum}
+                       (//.Sum left right)
                        (when (its #sum poly)
                          {#Nested for_sum}
-                         (for_sum (code arity 'recursive context) sum)
+                         (for_sum (code arity 'recursive context) [left right])
 
                          {#Flat for_variant}
                          (for_variant (code arity 'recursive context) (//.flat_variant it)))
 
-                       {.#Product product}
+                       (//.Product left right)
                        (when (its #product poly)
                          {#Nested for_product}
-                         (for_product (code arity 'recursive context) product)
+                         (for_product (code arity 'recursive context) [left right])
 
                          {#Flat for_record}
                          (for_record (code arity 'recursive context) (//.flat_tuple it)))
 
-                       {.#Function it}
-                       ((its #function poly) (code arity 'recursive context) it)
+                       (//.Function cause effect)
+                       ((its #function poly) (code arity 'recursive context) [cause effect])
 
                        (..recursive it)
                        ((its #recursive poly) (code arity 'recursive context) [(list 'recursive) it])
@@ -211,7 +209,7 @@
 
                        {.#Reification it}
                        (when it
-                         [{.#Parameter 1} {.#Parameter 0}]
+                         [{.#Parameter .argument 0} {.#Parameter .abstraction 0}]
                          (when (its #recursion poly)
                            {.#Some recursion}
                            (recursion (code arity 'recursive context) (list 'recursive))
@@ -226,7 +224,7 @@
                           (code arity 'recursive context)
                           it))
 
-                       {.#Parameter index}
+                       {.#Parameter .argument index}
                        (when (its #parameter poly)
                          {.#Some parameter}
                          (parameter (code arity 'recursive context) [arity index])
@@ -236,8 +234,8 @@
                            {try.#Failure _}
                            (exception.except ..invalid [it])
 
-                           success
-                           success))
+                           {try.#Success [type term]}
+                           {try.#Success term}))
                        
                        (..polymorphic _ _)
                        (let [[arity non_quantified] (//.flat_univ_q (//.anonymous it))
diff --git a/stdlib/source/library/lux/type/record.lux b/stdlib/source/library/lux/type/record.lux
index a8b0f5c1e4..d8c522f7fe 100644
--- a/stdlib/source/library/lux/type/record.lux
+++ b/stdlib/source/library/lux/type/record.lux
@@ -156,7 +156,7 @@
                              (list.any? (n.= index) excluded)))
              included (|> (when (product.left head)
                             {.#Some [index exported? cohort]}
-                            (stack.size cohort)
+                            (list.size cohort)
 
                             {.#None}
                             1)
diff --git a/stdlib/source/library/lux/type/row.lux b/stdlib/source/library/lux/type/row.lux
index 2ebab717e9..1c8440302e 100644
--- a/stdlib/source/library/lux/type/row.lux
+++ b/stdlib/source/library/lux/type/row.lux
@@ -87,7 +87,7 @@
     {.#Named _ it}
     (nesting it)
 
-    {.#Existential (stack) un_quantified}
+    {.#Quantification .existential (stack) un_quantified}
     (when (type.flat_reification un_quantified)
       [{.#Named [..row_module ..row_proper] _} _]
       1
diff --git a/stdlib/source/library/lux/web/html.lux b/stdlib/source/library/lux/web/html.lux
index cd1dcb2a11..81e8154c64 100644
--- a/stdlib/source/library/lux/web/html.lux
+++ b/stdlib/source/library/lux/web/html.lux
@@ -3,7 +3,7 @@
 
 (.using
  [library
-  [lux (.except Meta Source Target
+  [lux (.except Meta Source Target Parameter
                 text comment and open quote ruby)
    [control
     ["[0]" maybe (.use "[1]#[0]" functor)]]
diff --git a/stdlib/source/polytypic/lux/abstract/functor.lux b/stdlib/source/polytypic/lux/abstract/functor.lux
index 805ebc8caa..498507cf36 100644
--- a/stdlib/source/polytypic/lux/abstract/functor.lux
+++ b/stdlib/source/polytypic/lux/abstract/functor.lux
@@ -42,7 +42,7 @@
                                              (, 'it)))))))}
      poly.#parameter {.#Some (function (_ code [arity it])
                                {try.#Success
-                                (if (natural.= 1 it)
-                                  (` /.variable)
-                                  (` /.constant))})}
+                                (when it
+                                  0 (` /.variable)
+                                  _ (` /.constant))})}
      poly.#specializations (list)]))
diff --git a/stdlib/source/projection/lux/type.lux b/stdlib/source/projection/lux/type.lux
index fb4718b886..78bfba354e 100644
--- a/stdlib/source/projection/lux/type.lux
+++ b/stdlib/source/projection/lux/type.lux
@@ -41,7 +41,7 @@
 (the .public recursive_iteration
   (template.macro (_)
     [{.#Reification (..recursion_parameter)
-                    {.#Parameter 0}}]))
+                    {.#Parameter .argument 0}}]))
 
 (template.with [<name>]
   [(exception.the .public (<name> type)
@@ -82,7 +82,8 @@
                       (text.interposed ""))])))
 
 (every .public Env
-  (Dictionary Natural [Type Code]))
+  (Dictionary Natural [[Type Code]
+                       [Type Code]]))
 
 (every .public (Projection it)
   (//.Projection [Env Natural (List Type)]
@@ -161,26 +162,30 @@
     (try#each (|>> [[env items_read pass_through]])
               (value' env poly types))))
 
-(the (label idx)
-  (-> Natural
+(the (label prefix idx)
+  (-> Text Natural
       Code)
-  (code.local (text "label" text.tab (n#as idx))))
+  (code.local (text prefix text.tab (n#as idx))))
 
-(the .public (with_extension type poly)
+(the .public (with_extension [abstraction argument] poly)
   (for_any (_ it)
-    (-> Type (Projection it)
-        (Projection [Code it])))
+    (-> [Type Type] (Projection it)
+        (Projection [[Code Code] it])))
   (.function (_ [env inputs])
     (let [current_id (dictionary.size env)
-          'var (label current_id)]
-      (when (//.value [(dictionary.has current_id [type 'var] env)
+          'abstraction (label "abstraction" current_id)
+          'argument (label "argument" current_id)]
+      (when (//.value [(dictionary.has current_id
+                                       [[abstraction 'abstraction]
+                                        [argument 'argument]]
+                                       env)
                        inputs]
                       poly)
-        {try.#Failure error}
-        {try.#Failure error}
-
         {try.#Success [[_ inputs'] output]}
-        {try.#Success [[env inputs'] ['var output]]}))))
+        {try.#Success [[env inputs'] [['abstraction 'argument] output]]}
+
+        {try.#Failure error}
+        {try.#Failure error}))))
 
 (template.with [<name> <flattener> <exception>]
   [(`` (the .public (<name> poly)
@@ -192,7 +197,7 @@
            (let [members (<flattener> (/.anonymous headT))]
              (if (n.> 1 (list.size members))
                  (local members poly)
-                 (//.failure (exception.error <exception> headT)))))))]
+                 (//.failure (exception.error <exception> [headT])))))))]
 
   [variant /.flat_variant ..not_variant]
   [tuple   /.flat_tuple   ..not_tuple]
@@ -216,29 +221,33 @@
      funcI (by ! each dictionary.size ..env)
      [num_args non_poly] (local (list headT) ..polymorphic')
      env ..env
-     .let [funcL (label funcI)
+     .let [funcL (label "abstraction" funcI)
            [all_varsL env'] (loop (again [current_arg 0
                                           env' env
                                           all_varsL (is (List Code) (list))])
                               (if (n.< num_args current_arg)
                                   (if (n.= 0 current_arg)
-                                      (let [varL (label (++ funcI))]
+                                      (let [varL (label "argument" (++ funcI))]
                                         (again (++ current_arg)
                                                (|> env'
-                                                   (dictionary.has funcI [headT funcL])
-                                                   (dictionary.has (++ funcI) [{.#Parameter (++ funcI)} varL]))
+                                                   (dictionary.has funcI [[headT funcL]
+                                                                          [{.#Parameter .argument funcI} varL]]))
                                                (list#composite (list varL) all_varsL)))
-                                      (let [partialI (|> current_arg (n.* 2) (n.+ funcI))
-                                            partial_varI (++ partialI)
-                                            partial_varL (label partial_varI)
+                                      (let [partial_level (n.+ funcI)
+                                            partial_var (|>> partial_level (label "partial"))
+
+                                            partial_argument (partial_level current_arg)
+                                            'partial_var (partial_var current_arg)
                                             partialC (` ((, funcL) (,* (|> (list.indices num_args)
-                                                                           (list#each (|>> (n.* 2) ++ (n.+ funcI) label))
+                                                                           (list#each partial_var)
                                                                            list.reversed))))]
                                         (again (++ current_arg)
                                                (|> env'
-                                                   (dictionary.has partialI [(recursion_parameter) partialC])
-                                                   (dictionary.has partial_varI [{.#Parameter partial_varI} partial_varL]))
-                                               (list#composite (list partial_varL) all_varsL))))
+                                                   (dictionary.has partial_argument [[(recursion_parameter)
+                                                                                      partialC]
+                                                                                     [{.#Parameter .argument partial_argument}
+                                                                                      'partial_var]]))
+                                               (list#composite (list 'partial_var) all_varsL))))
                                   [all_varsL env']))]]
     (<| (with_env env')
         (local (list non_poly))
@@ -287,10 +296,9 @@
 (the .public (argument env idx)
   (-> Env Natural
       Natural)
-  (let [env_level (n./ 2 (dictionary.size env))
-        parameter_level (n./ 2 idx)
-        parameter_idx (n.% 2 idx)]
-    (|> env_level -- (n.- parameter_level) (n.* 2) (n.+ parameter_idx))))
+  (|> (dictionary.size env)
+      --
+      (n.- idx)))
 
 (the .public parameter
   (Projection Code)
@@ -298,16 +306,19 @@
     [env ..env
      headT any]
     (when headT
-      {.#Parameter idx}
+      {.#Parameter parameter idx}
       (when (dictionary.value (..argument env idx) env)
-        {try.#Success [poly_type poly_code]}
-        (in poly_code)
+        {try.#Success [[abstraction_type abstraction_code]
+                       [argument_type argument_code]]}
+        (in (when parameter
+              .abstraction abstraction_code
+              .argument argument_code))
 
         failure
-        (//.failure (exception.error ..unknown_parameter headT)))
+        (//.failure (exception.error ..unknown_parameter [headT])))
 
       _
-      (//.failure (exception.error ..not_parameter headT)))))
+      (//.failure (exception.error ..not_parameter [headT])))))
 
 (the .public (this_parameter id)
   (-> Natural
@@ -316,10 +327,10 @@
     [env ..env
      headT any]
     (when headT
-      {.#Parameter idx}
+      {.#Parameter .argument idx}
       (if (n.= id (..argument env idx))
           (in [])
-          (//.failure (exception.error ..wrong_parameter [{.#Parameter id} headT])))
+          (//.failure (exception.error ..wrong_parameter [{.#Parameter .argument id} headT])))
 
       _
       (//.failure (exception.error ..not_parameter headT)))))
@@ -355,10 +366,9 @@
     (when (/.anonymous headT)
       (..recursive_definition headT')
       (do !
-        [[recT _ output] (|> poly
-                             (with_extension (recursion_parameter))
-                             (with_extension headT)
-                             (local (list headT')))]
+        [[[recT _] output] (|> poly
+                               (with_extension [headT (recursion_parameter)])
+                               (local (list headT')))]
         (in [recT output]))
 
       _
@@ -371,7 +381,8 @@
      headT any]
     (when (/.anonymous headT)
       (^.multi (..recursive_iteration)
-               [(dictionary.value 0 env) {try.#Success [self_type self_call]}])
+               [(dictionary.value 0 env) {try.#Success [[self_type self_call]
+                                                        [argument_type argument_call]]}])
       (in self_call)
 
       _
diff --git a/stdlib/source/test/lux.lux b/stdlib/source/test/lux.lux
index 5045898876..ab39147d4c 100644
--- a/stdlib/source/test/lux.lux
+++ b/stdlib/source/test/lux.lux
@@ -609,7 +609,9 @@
      expected/0 existential_type
      expected/1 existential_type]
     (<| (_.for [/.Type
-                /.#Nominal /.#Sum /.#Product /.#Function /.#Parameter /.#Variable /.#Opaque /.#Universal /.#Existential /.#Reification /.#Named])
+                /.#Nominal /.#Variable /.#Opaque /.#Reification /.#Named
+                /.#Parameter /.abstraction /.argument
+                /.#Quantification /.universal /.existential])
         (all _.and
              (_.coverage [/.is]
                (|> expected
@@ -629,8 +631,9 @@
              (_.coverage [/.type_of]
                (same? /.Natural (/.type_of expected)))
              (_.coverage [/.Nominal]
-               (when (/.Nominal "foo" [expected/0 expected/1])
-                 {.#Nominal "foo" (stack actual/0 actual/1)}
+               (when (/.Nominal "foo" [[#1 expected/0]
+                                       [#1 expected/1]])
+                 {.#Nominal "foo" (list [#1 actual/0] [#1 actual/1])}
                  (and (same? expected/0 actual/0)
                       (same? expected/1 actual/1))
 
diff --git a/stdlib/source/test/lux/data/collection/array.lux b/stdlib/source/test/lux/data/collection/array.lux
index 532203c3ab..0df15fc25c 100644
--- a/stdlib/source/test/lux/data/collection/array.lux
+++ b/stdlib/source/test/lux/data/collection/array.lux
@@ -173,8 +173,8 @@
                  (_.coverage [\\unsafe.nominal]
                    (when \\unsafe.Array
                      (<| {.#Named (name \\unsafe.Array)}
-                         {.#Universal (stack)}
-                         {.#Nominal \\unsafe.nominal (stack _)})
+                         {.#Quantification .universal (stack)}
+                         {.#Nominal \\unsafe.nominal (list [.co_variant _])})
                      true
 
                      _
@@ -349,8 +349,8 @@
                (when /.Array
                  (<| {.#Named (name /.Array)}
                      {.#Named (name \\unsafe.Array)}
-                     {.#Universal (stack)}
-                     {.#Nominal /.nominal (stack _)})
+                     {.#Quantification .universal (stack)}
+                     {.#Nominal /.nominal (list [.co_variant _])})
                  true
 
                  _
diff --git a/stdlib/source/test/lux/meta.lux b/stdlib/source/test/lux/meta.lux
index 3844bae7b6..b6ee8d1945 100644
--- a/stdlib/source/test/lux/meta.lux
+++ b/stdlib/source/test/lux/meta.lux
@@ -73,7 +73,7 @@
                              .#type_context [.#ex_counter 0
                                              .#var_counter 0
                                              .#var_bindings (list)]
-                             .#expected {.#Some {.#Nominal nominal_type (stack)}}
+                             .#expected {.#Some {.#Nominal nominal_type (list)}}
                              .#seed expected_seed
                              .#eval (as_expected [])])]]
     (all _.and
@@ -130,7 +130,7 @@
                              .#type_context [.#ex_counter 0
                                              .#var_counter 0
                                              .#var_bindings (list)]
-                             .#expected {.#Some {.#Nominal nominal_type (stack)}}
+                             .#expected {.#Some {.#Nominal nominal_type (list)}}
                              .#seed expected_seed
                              .#eval (as_expected [])])]]
     (all _.and
@@ -254,7 +254,7 @@
      source_code (random.upper_cased 1)
      expected_current_module (random.upper_cased 1)
      expected_type (by ! each (function (_ name)
-                                {.#Nominal name (stack)})
+                                {.#Nominal name (list)})
                        (random.upper_cased 1))
      expected_seed random.natural
      expected random.natural
@@ -349,7 +349,7 @@
                       source_code (random.upper_cased 1)
                       expected_current_module (random.upper_cased 1)
                       expected_type (by ! each (function (_ name)
-                                                 {.#Nominal name (stack)})
+                                                 {.#Nominal name (list)})
                                         (random.upper_cased 1))
                       expected_seed random.natural
                       expected random.natural
diff --git a/stdlib/source/test/lux/meta/binding.lux b/stdlib/source/test/lux/meta/binding.lux
index cb24aba9c3..aef4f7d3f2 100644
--- a/stdlib/source/test/lux/meta/binding.lux
+++ b/stdlib/source/test/lux/meta/binding.lux
@@ -90,7 +90,7 @@
                              .#type_context [.#ex_counter 0
                                              .#var_counter 0
                                              .#var_bindings (list)]
-                             .#expected {.#Some {.#Nominal nominal_type (stack)}}
+                             .#expected {.#Some {.#Nominal nominal_type (list)}}
                              .#seed expected_seed
                              .#eval (as_expected [])])]]
     (all _.and
@@ -123,7 +123,7 @@
                                         (random.upper_cased 1))
      expected_proper (random.upper_cased 1)
      expected_type (by ! each (function (_ name)
-                                {.#Nominal name (stack)})
+                                {.#Nominal name (list)})
                        (random.upper_cased 1))
      expected_value (random.either (in .the)
                                    (in .macro))
@@ -244,7 +244,7 @@
                                         (random.upper_cased 1))
      expected_proper (random.upper_cased 1)
      expected_type (by ! each (function (_ name)
-                                {.#Nominal name (stack)})
+                                {.#Nominal name (list)})
                        (random.upper_cased 1))
      expected_value (random.either (in .the)
                                    (in .macro))
diff --git a/stdlib/source/test/lux/meta/binding/local.lux b/stdlib/source/test/lux/meta/binding/local.lux
index 1c9a505fb7..3cdfdbdeeb 100644
--- a/stdlib/source/test/lux/meta/binding/local.lux
+++ b/stdlib/source/test/lux/meta/binding/local.lux
@@ -43,11 +43,11 @@
 
                                                                   _
                                                                   {.#None}))))
-         .let [type_0 {.#Nominal name_0 (stack)}
-               type_1 {.#Nominal name_1 (stack)}
-               type_2 {.#Nominal name_2 (stack)}
-               type_3 {.#Nominal name_3 (stack)}
-               type_4 {.#Nominal name_4 (stack)}
+         .let [type_0 {.#Nominal name_0 (list)}
+               type_1 {.#Nominal name_1 (list)}
+               type_2 {.#Nominal name_2 (list)}
+               type_3 {.#Nominal name_3 (list)}
+               type_4 {.#Nominal name_4 (list)}
 
                globals (is (property.List [Bit .Global])
                            (list [name_4
diff --git a/stdlib/source/test/lux/meta/label.lux b/stdlib/source/test/lux/meta/label.lux
index 1b18d246a2..2efc6d8f2b 100644
--- a/stdlib/source/test/lux/meta/label.lux
+++ b/stdlib/source/test/lux/meta/label.lux
@@ -91,15 +91,13 @@
                     (= (list [this_module (name.proper (name ,tag_0))]
                              [this_module (name.proper (name ,tag_1))])
                        (`` (list (,, (static.expansion
-                                      (//#each (|>> list.of_stack
-                                                    (list#each ..as_name))
+                                      (//#each (list#each ..as_name)
                                                (/.tags (name ,type_0)))))))))
                   (_.coverage [/.slots]
                     (= (list [this_module (name.proper (name ,slot_0))]
                              [this_module (name.proper (name ,slot_1))])
                        (`` (list (,, (static.expansion
-                                      (//#each (|>> list.of_stack
-                                                    (list#each ..as_name))
+                                      (//#each (list#each ..as_name)
                                                (/.slots (name ,type_1)))))))))
                   )))
 
@@ -126,8 +124,8 @@
                                               (random.and (in head))))))]
               tags_0 (random_labels 5)
               tags_1 (random_labels 6)
-              .let [type_0 {.#Named [label_module name_1] {.#Nominal name_0 (stack)}}
-                    type_1 {.#Named [label_module name_1] {.#Nominal name_1 (stack)}}
+              .let [type_0 {.#Named [label_module name_1] {.#Nominal name_0 (list)}}
+                    type_1 {.#Named [label_module name_1] {.#Nominal name_1 (list)}}
 
                     expected_lux
                     (is Lux
@@ -164,7 +162,7 @@
                                                                     stack.enumeration
                                                                     (stack#each (function (_ [index proper])
                                                                                   [proper [true {.#Definition [.Tag
-                                                                                                               (|> [{.#Some [(lefts index) (right? index) cohort]} type_0]
+                                                                                                               (|> [{.#Some [(lefts index) (right? index) (list.of_stack cohort)]} type_0]
                                                                                                                    (is Label)
                                                                                                                    (as .Tag))]}]]))
                                                                     list.of_stack))
@@ -182,7 +180,7 @@
                                                                     stack.enumeration
                                                                     (stack#each (function (_ [index proper])
                                                                                   [proper [true {.#Definition [.Slot
-                                                                                                               (|> [{.#Some [(lefts index) (right? index) cohort]} type_1]
+                                                                                                               (|> [{.#Some [(lefts index) (right? index) (list.of_stack cohort)]} type_1]
                                                                                                                    (is Label)
                                                                                                                    (as .Slot))]}]]))
                                                                     list.of_stack)))
@@ -199,11 +197,12 @@
                   (_.coverage [/.tag_stacks]
                     (let [equivalence (stack.equivalence
                                        (product.equivalence
-                                        (stack.equivalence name.equivalence)
+                                        (list.equivalence name.equivalence)
                                         type.equivalence))]
                       (|> (/.tag_stacks label_module)
                           (//.value expected_lux)
-                          (try#each (by equivalence = (stack [(stack#each (|>> [label_module]) {.#Top tags_1})
+                          (try#each (by equivalence = (stack [(list#each (|>> [label_module])
+                                                                         (list.of_stack {.#Top tags_1}))
                                                               type_1])))
                           (try.else false))))
                   )))
diff --git a/stdlib/source/test/lux/meta/module.lux b/stdlib/source/test/lux/meta/module.lux
index f413aae7c5..ac5df8d961 100644
--- a/stdlib/source/test/lux/meta/module.lux
+++ b/stdlib/source/test/lux/meta/module.lux
@@ -82,7 +82,7 @@
                                       .#type_context [.#ex_counter 0
                                                       .#var_counter 0
                                                       .#var_bindings (list)]
-                                      .#expected {.#Some {.#Nominal nominal_type (stack)}}
+                                      .#expected {.#Some {.#Nominal nominal_type (list)}}
                                       .#seed expected_seed
                                       .#eval (as_expected [])])]]
              (<| (_.for [.Module
diff --git a/stdlib/source/test/lux/meta/module/import.lux b/stdlib/source/test/lux/meta/module/import.lux
index aff87c1ffb..1c34653c83 100644
--- a/stdlib/source/test/lux/meta/module/import.lux
+++ b/stdlib/source/test/lux/meta/module/import.lux
@@ -68,7 +68,7 @@
                                  .#type_context [.#ex_counter 0
                                                  .#var_counter 0
                                                  .#var_bindings (list)]
-                                 .#expected {.#Some {.#Nominal nominal_type (stack)}}
+                                 .#expected {.#Some {.#Nominal nominal_type (list)}}
                                  .#seed expected_seed
                                  .#eval (as_expected [])])]]
         (all _.and
diff --git a/stdlib/source/test/lux/type.lux b/stdlib/source/test/lux/type.lux
index 6d4df940fb..1b49c6b8e4 100644
--- a/stdlib/source/test/lux/type.lux
+++ b/stdlib/source/test/lux/type.lux
@@ -69,7 +69,7 @@
   (Random Type)
   (|> (random.alpha_numeric 1)
       (by random.monad each (function (_ name)
-                              {.#Nominal name (stack)}))))
+                              {.#Nominal name (list)}))))
 
 (the test|matches
   Test
@@ -168,52 +168,46 @@
                (!expect (^.multi {try.#Failure error}
                                  (exception.is? \\projection.not_parameter error)))))
          (_.coverage [\\projection.unknown_parameter]
-           (|> (\\projection.value \\projection.parameter {.#Parameter parameter})
+           (|> (\\projection.value \\projection.parameter {.#Parameter .argument parameter})
                (!expect (^.multi {try.#Failure error}
                                  (exception.is? \\projection.unknown_parameter error)))))
          (_.coverage [\\projection.with_extension]
-           (|> (\\projection.value (<| (\\projection.with_extension quantification)
-                                       (\\projection.with_extension argument)
+           (|> (\\projection.value (<| (\\projection.with_extension [quantification argument])
                                        \\projection.any)
                                    not_parameter)
-               (!expect (^.multi {try.#Success [quantification::binding argument::binding actual]}
+               (!expect (^.multi {try.#Success [[quantification::binding argument::binding] actual]}
                                  (same? not_parameter actual)))))
          (_.coverage [\\projection.parameter]
-           (|> (\\projection.value (<| (\\projection.with_extension quantification)
-                                       (\\projection.with_extension argument)
+           (|> (\\projection.value (<| (\\projection.with_extension [quantification argument])
                                        \\projection.parameter)
-                                   {.#Parameter 0})
-               (!expect {try.#Success [quantification::binding argument::binding _]})))
+                                   {.#Parameter .abstraction 0})
+               (!expect {try.#Success [[quantification::binding argument::binding] _]})))
          (_.coverage [\\projection.argument]
            (let [argument? (is (-> Natural Natural Bit)
                                (function (_ @ expected)
-                                 (|> (\\projection.value (<| (\\projection.with_extension quantification)
-                                                             (\\projection.with_extension argument)
-                                                             (\\projection.with_extension quantification)
-                                                             (\\projection.with_extension argument)
+                                 (|> (\\projection.value (<| (\\projection.with_extension [quantification argument])
+                                                             (\\projection.with_extension [quantification argument])
                                                              (do <>.monad
                                                                [env \\projection.env
                                                                 _ \\projection.any]
                                                                (in (\\projection.argument env @))))
                                                          not_parameter)
-                                     (!expect (^.multi {try.#Success [_ _ _ _ actual]}
+                                     (!expect (^.multi {try.#Success [[_ _] [_ _] actual]}
                                                        (n.= expected actual))))))]
              (and (argument? 0 2)
                   (argument? 1 3)
                   (argument? 2 0))))
          (_.coverage [\\projection.wrong_parameter]
-           (|> (\\projection.value (<| (\\projection.with_extension quantification)
-                                       (\\projection.with_extension argument)
+           (|> (\\projection.value (<| (\\projection.with_extension [quantification argument])
                                        (\\projection.this_parameter 1))
-                                   {.#Parameter 0})
+                                   {.#Parameter .abstraction 0})
                (!expect (^.multi {try.#Failure error}
                                  (exception.is? \\projection.wrong_parameter error)))))
          (_.coverage [\\projection.this_parameter]
-           (|> (\\projection.value (<| (\\projection.with_extension quantification)
-                                       (\\projection.with_extension argument)
+           (|> (\\projection.value (<| (\\projection.with_extension [quantification argument])
                                        (\\projection.this_parameter 0))
-                                   {.#Parameter 0})
-               (!expect {try.#Success [quantification::binding argument::binding _]})))
+                                   {.#Parameter .abstraction 0})
+               (!expect {try.#Success [[quantification::binding argument::binding] _]})))
          )))
 
 (the test|polymorphic
@@ -370,17 +364,23 @@
      (let [pairG (random.and again again)
            un_parameterized (is (Random Type)
                                 (all random.either
-                                     (random#each (|>> {.#Nominal}) (random.and ..proper (random.stack 0 again)))
-                                     (random#each (|>> {.#Nominal}) (random.and ..proper (random.stack 1 again)))
-                                     (random#each (|>> {.#Nominal}) (random.and ..proper (random.stack 2 again)))
-                                     (random#each (|>> {.#Sum}) pairG)
-                                     (random#each (|>> {.#Product}) pairG)
-                                     (random#each (|>> {.#Function}) pairG)
+                                     (random#each (|>> {.#Nominal}) (random.and ..proper (random.list 0 (random.and random.bit again))))
+                                     (random#each (|>> {.#Nominal}) (random.and ..proper (random.list 1 (random.and random.bit again))))
+                                     (random#each (|>> {.#Nominal}) (random.and ..proper (random.list 2 (random.and random.bit again))))
+                                     (random#each (function (_ [left right])
+                                                    (/.Sum left right))
+                                                  pairG)
+                                     (random#each (function (_ [left right])
+                                                    (/.Product left right))
+                                                  pairG)
+                                     (random#each (function (_ [left right])
+                                                    (/.Function left right))
+                                                  pairG)
                                      ))]
        (when parameters
          0 un_parameterized
          _ (|> random.natural
-               (random#each (|>> (n.% parameters) {.#Parameter}))
+               (random#each (|>> (n.% parameters) {.#Parameter .argument}))
                (random.either un_parameterized)))))))
 
 (the .public (random parameters)
@@ -423,7 +423,8 @@
               members (|> (..random 0)
                           (random.only (function (_ type)
                                          (when type
-                                           (^.or {.#Sum _} {.#Product _})
+                                           (^.or (/.Sum left right)
+                                                 (/.Product left right))
                                            false
 
                                            _
@@ -451,7 +452,7 @@
                       (do maybe.monad
                         [partial (/.reified (list Bit) Annotated)
                          full (/.reified (list Integer) partial)]
-                        (in (by /.equivalence = full {.#Product Bit Integer}))))
+                        (in (by /.equivalence = full (/.Product Bit Integer)))))
                   (|> (/.reified (list Bit) Text)
                       (pipe.when
                         {.#None}
@@ -465,7 +466,10 @@
               extra (|> (..random 0)
                         (random.only (function (_ type)
                                        (when type
-                                         (^.or {.#Function _} {.#Reification _})
+                                         (/.Function left right)
+                                         false
+
+                                         {.#Reification _}
                                          false
 
                                          _
@@ -491,7 +495,8 @@
               body_type (|> (..random 0)
                             (random.only (function (_ type)
                                            (when type
-                                             (^.or {.#Universal _} {.#Existential _})
+                                             (^.or {.#Quantification .universal _}
+                                                   {.#Quantification .existential _})
                                              false
 
                                              _
@@ -517,7 +522,7 @@
               element_type (|> (..random 0)
                                (random.only (function (_ type)
                                               (when type
-                                                {.#Nominal name (stack element_type)}
+                                                {.#Nominal name (list [polarity element_type])}
                                                 (not (text.= array.nominal name))
 
                                                 _
diff --git a/stdlib/source/test/lux/type/check.lux b/stdlib/source/test/lux/type/check.lux
index ce37af99b2..b536dfead1 100644
--- a/stdlib/source/test/lux/type/check.lux
+++ b/stdlib/source/test/lux/type/check.lux
@@ -50,20 +50,26 @@
    (function (_ again)
      (let [pairG (random.and again again)
            quantifiedG (random.and (random#in (stack)) (type' (++ num_vars)))
-           random_pair (random.either (random.either (random#each (|>> {.#Sum}) pairG)
-                                                     (random#each (|>> {.#Product}) pairG))
-                                      (random.either (random#each (|>> {.#Function}) pairG)
+           random_pair (random.either (random.either (random#each (function (_ [left right])
+                                                                    (//.Sum left right))
+                                                                  pairG)
+                                                     (random#each (function (_ [left right])
+                                                                    (//.Product left right))
+                                                                  pairG))
+                                      (random.either (random#each (function (_ [left right])
+                                                                    (//.Function left right))
+                                                                  pairG)
                                                      (random#each (|>> {.#Reification}) pairG)))
            random_id (let [random_id (random.either (random#each (|>> {.#Variable}) random.natural)
                                                     (random#each (|>> {.#Opaque}) random.natural))]
                        (when num_vars
                          0 random_id
-                         _ (random.either (random#each (|>> (n.% num_vars) (n.* 2) ++ {.#Parameter}) random.natural)
+                         _ (random.either (random#each (|>> (n.% num_vars) {.#Parameter .argument}) random.natural)
                                           random_id)))
-           random_quantified (random.either (random#each (|>> {.#Universal}) quantifiedG)
-                                            (random#each (|>> {.#Existential}) quantifiedG))]
+           random_quantified (random.either (random#each (|>> {.#Quantification .universal}) quantifiedG)
+                                            (random#each (|>> {.#Quantification .existential}) quantifiedG))]
        (all random.either
-            (random#each (|>> {.#Nominal}) (random.and ..proper (random#in (stack))))
+            (random#each (|>> {.#Nominal}) (random.and ..proper (random#in (list))))
             random_pair
             random_id
             random_quantified
@@ -77,20 +83,22 @@
 (the (valid_type? type)
   (-> Type Bit)
   (`` (when type
-        {.#Nominal name params}
-        (stack.every? valid_type? params)
-        
-        {.#Opaque id}
-        true
-
         (,, (template.with [<tag>]
-              [{<tag> left right}
+              [(<tag> left right)
                (and (valid_type? left)
                     (valid_type? right))]
 
-              [.#Sum]
-              [.#Product]
-              [.#Function]))
+              [//.Sum]
+              [//.Product]
+              [//.Function]))
+
+        {.#Nominal name params}
+        (list.every? (function (_ [polarity it])
+                       (valid_type? it))
+                     params)
+        
+        {.#Opaque id}
+        true
 
         {.#Named name type'}
         (valid_type? type')
@@ -125,7 +133,8 @@
   (-> Natural (Random Type))
   (do random.monad
     [nominal (random.upper_cased 3)
-     parameters (random.stack parameters (nominal_type (-- parameters)))]
+     parameters (random.list parameters (random.and random.bit
+                                                    (nominal_type (-- parameters))))]
     (in {.#Nominal nominal parameters})))
 
 (the clean_type
@@ -257,7 +266,7 @@
   (Random Type)
   (do random.monad
     [name (random.upper_cased 10)]
-    (in {.#Nominal name (stack)})))
+    (in {.#Nominal name (list)})))
 
 (the (non_twins = random)
   (for_any (_ a) (-> (-> a a Bit) (Random a) (Random [a a])))
@@ -275,22 +284,22 @@
 (the (handles_nominal_types! name/0 name/1 parameter/0 parameter/1)
   (-> Text Text Type Type Bit)
   (let [names_matter!
-        (and (..succeeds? (/.check {.#Nominal name/0 (stack)}
-                                   {.#Nominal name/0 (stack)}))
-             (..fails? (/.check {.#Nominal name/0 (stack)}
-                                {.#Nominal name/1 (stack)})))
+        (and (..succeeds? (/.check {.#Nominal name/0 (list)}
+                                   {.#Nominal name/0 (list)}))
+             (..fails? (/.check {.#Nominal name/0 (list)}
+                                {.#Nominal name/1 (list)})))
 
         parameters_matter!
-        (and (..succeeds? (/.check {.#Nominal name/0 (stack parameter/0)}
-                                   {.#Nominal name/0 (stack parameter/0)}))
-             (..fails? (/.check {.#Nominal name/0 (stack parameter/0)}
-                                {.#Nominal name/0 (stack parameter/1)})))
+        (and (..succeeds? (/.check {.#Nominal name/0 (list [.co_variant parameter/0])}
+                                   {.#Nominal name/0 (list [.co_variant parameter/0])}))
+             (..fails? (/.check {.#Nominal name/0 (list [.co_variant parameter/0])}
+                                {.#Nominal name/0 (list [.co_variant parameter/1])})))
 
         covariant_parameters!
-        (and (..succeeds? (/.check {.#Nominal name/0 (stack Super)}
-                                   {.#Nominal name/0 (stack Sub)}))
-             (..fails? (/.check {.#Nominal name/0 (stack Sub)}
-                                {.#Nominal name/0 (stack Super)})))]
+        (and (..succeeds? (/.check {.#Nominal name/0 (list [.co_variant Super])}
+                                   {.#Nominal name/0 (list [.co_variant Sub])}))
+             (..fails? (/.check {.#Nominal name/0 (list [.co_variant Sub])}
+                                {.#Nominal name/0 (list [.co_variant Super])})))]
     (and names_matter!
          parameters_matter!
          covariant_parameters!)))
@@ -298,15 +307,15 @@
 (template.with [<assertion> <combinator>]
   [(the (<assertion> name/0 name/1)
      (-> Text Text Bit)
-     (let [pair/0 {<combinator> {.#Nominal name/0 (stack)} {.#Nominal name/0 (stack)}}
-           pair/1 {<combinator> {.#Nominal name/1 (stack)} {.#Nominal name/1 (stack)}}
+     (let [pair/0 (<combinator> {.#Nominal name/0 (list)} {.#Nominal name/0 (list)})
+           pair/1 (<combinator> {.#Nominal name/1 (list)} {.#Nominal name/1 (list)})
            
            invariant!
            (and (..succeeds? (/.check pair/0 pair/0))
                 (..fails? (/.check pair/0 pair/1)))
 
-           super_pair {<combinator> Super Super}
-           sub_pair {<combinator> Sub Sub}
+           super_pair (<combinator> Super Super)
+           sub_pair (<combinator> Sub Sub)
            
            covariant!
            (and (..succeeds? (/.check super_pair sub_pair))
@@ -314,17 +323,17 @@
        (and invariant!
             covariant!)))]
 
-  [handles_products! .#Product]
-  [handles_sums! .#Sum]
+  [handles_products! //.Product]
+  [handles_sums! //.Sum]
   )
 
 (the (handles_function_variance! nominal)
   (-> Type Bit)
   (let [functions_have_contravariant_inputs!
-        (..succeeds? (/.check {.#Function Sub nominal} {.#Function Super nominal}))
+        (..succeeds? (/.check (//.Function Sub nominal) (//.Function Super nominal)))
         
         functions_have_covariant_outputs!
-        (..succeeds? (/.check {.#Function nominal Super} {.#Function nominal Sub}))]
+        (..succeeds? (/.check (//.Function nominal Super) (//.Function nominal Sub)))]
     (and functions_have_contravariant_inputs!
          functions_have_covariant_outputs!)))
 
@@ -576,29 +585,33 @@
                        [leftT dirty_type
                         rightT dirty_type]
                        (in (function (_ holeT)
-                             {<tag> (leftT holeT) (rightT holeT)})))]
+                             (<tag> (leftT holeT) (rightT holeT)))))]
 
-                    [.#Sum]
-                    [.#Product]
-                    [.#Function]
-                    [.#Reification]
+                    [//.Sum]
+                    [//.Product]
+                    [//.Function]
                     ))
+              (do random.monad
+                [leftT dirty_type
+                 rightT dirty_type]
+                (in (function (_ holeT)
+                      {.#Reification (leftT holeT) (rightT holeT)})))
               (do [! random.monad]
                 [name (random.upper_cased 10)
                  parameterT dirty_type]
                 (in (function (_ holeT)
-                      {.#Nominal name (stack (parameterT holeT))})))
+                      {.#Nominal name (list [.co_variant (parameterT holeT)])})))
               (,, (template.with [<tag>]
                     [(do [! random.monad]
                        [funcT dirty_type
                         argT dirty_type
                         body random.natural]
                        (in (function (_ holeT)
-                             {<tag> (stack (funcT holeT) (argT holeT))
-                                    {.#Parameter body}})))]
+                             {.#Quantification <tag> (stack [(funcT holeT) (argT holeT)])
+                                               {.#Parameter .argument body}})))]
 
-                    [.#Universal]
-                    [.#Existential]
+                    [.universal]
+                    [.existential]
                     ))
               )))))
 
@@ -641,16 +654,16 @@
   (do random.monad
     [nominal (random.upper_cased 10)
      example ..clean_type]
-    (in (and (/.< {.#Nominal nominal (stack)}
-                  {.#Nominal nominal (stack)})
-             (/.< {.#Nominal nominal (stack .Any)}
-                  {.#Nominal nominal (stack example)})
-             (not (/.< {.#Nominal nominal (stack example)}
-                       {.#Nominal nominal (stack .Any)}))
-             (/.< {.#Nominal nominal (stack example)}
-                  {.#Nominal nominal (stack .Nothing)})
-             (not (/.< {.#Nominal nominal (stack .Nothing)}
-                       {.#Nominal nominal (stack example)}))
+    (in (and (/.< {.#Nominal nominal (list)}
+                  {.#Nominal nominal (list)})
+             (/.< {.#Nominal nominal (list [.co_variant .Any])}
+                  {.#Nominal nominal (list [.co_variant example])})
+             (not (/.< {.#Nominal nominal (list [.co_variant example])}
+                       {.#Nominal nominal (list [.co_variant .Any])}))
+             (/.< {.#Nominal nominal (list [.co_variant example])}
+                  {.#Nominal nominal (list [.co_variant .Nothing])})
+             (not (/.< {.#Nominal nominal (list [.co_variant .Nothing])}
+                       {.#Nominal nominal (list [.co_variant example])}))
              ))))
 
 (the for_subsumption|sum
@@ -658,14 +671,14 @@
   (do random.monad
     [left ..clean_type
      right ..clean_type]
-    (in (and (/.< {.#Sum .Any .Any}
-                  {.#Sum left right})
-             (not (/.< {.#Sum left right}
-                       {.#Sum .Any .Any}))
-             (/.< {.#Sum left right}
-                  {.#Sum .Nothing .Nothing})
-             (not (/.< {.#Sum .Nothing .Nothing}
-                       {.#Sum left right}))
+    (in (and (/.< (//.Sum .Any .Any)
+                  (//.Sum left right))
+             (not (/.< (//.Sum left right)
+                       (//.Sum .Any .Any)))
+             (/.< (//.Sum left right)
+                  (//.Sum .Nothing .Nothing))
+             (not (/.< (//.Sum .Nothing .Nothing)
+                       (//.Sum left right)))
              ))))
 
 (the for_subsumption|product
@@ -673,14 +686,14 @@
   (do random.monad
     [left ..clean_type
      right ..clean_type]
-    (in (and (/.< {.#Product .Any .Any}
-                  {.#Product left right})
-             (not (/.< {.#Product left right}
-                       {.#Product .Any .Any}))
-             (/.< {.#Product left right}
-                  {.#Product .Nothing .Nothing})
-             (not (/.< {.#Product .Nothing .Nothing}
-                       {.#Product left right}))
+    (in (and (/.< (//.Product .Any .Any)
+                  (//.Product left right))
+             (not (/.< (//.Product left right)
+                       (//.Product .Any .Any)))
+             (/.< (//.Product left right)
+                  (//.Product .Nothing .Nothing))
+             (not (/.< (//.Product .Nothing .Nothing)
+                       (//.Product left right)))
              ))))
 
 (the for_subsumption|function
@@ -688,12 +701,12 @@
   (do random.monad
     [left ..clean_type
      right ..clean_type]
-    (in (and (/.< {.#Function .Nothing .Any}
-                  {.#Function left right})
-             (not (/.< {.#Function left right}
-                       {.#Function .Nothing .Any}))
-             (not (/.< {.#Function .Any .Nothing}
-                       {.#Function left right}))
+    (in (and (/.< (//.Function .Nothing .Any)
+                  (//.Function left right))
+             (not (/.< (//.Function left right)
+                       (//.Function .Nothing .Any)))
+             (not (/.< (//.Function .Any .Nothing)
+                       (//.Function left right)))
              ))))
 
 (template.with [<tag> <name>]