Finishing the meta-compiler [Part 2]

15 files changed, 647 insertions, 263 deletions

diff --git a/stdlib/source/experiment/compiler.lux b/stdlib/source/experiment/compiler.lux
new file mode 100644
index 000000000..f17f6c499
--- /dev/null
+++ b/stdlib/source/experiment/compiler.lux
@@ -0,0 +1,15 @@
+(.using
+ [library
+  [lux "*"
+   [control
+    ["[0]" try]]
+   [tool
+    ["[0]" compiler {"+" Custom}]]]])
+
+(def: .public (dummy parameters)
+  (Custom Nat [] [])
+  {try.#Success
+   [0 (function (_ input)
+        [compiler.#dependencies (list)
+         compiler.#process (function (_ state archive)
+                             {try.#Failure "YOLO"})])]})
diff --git a/stdlib/source/library/lux.lux b/stdlib/source/library/lux.lux
index e6a3e5e6f..7ddfa427f 100644
--- a/stdlib/source/library/lux.lux
+++ b/stdlib/source/library/lux.lux
@@ -5128,10 +5128,10 @@
 
 (def: (recursive_type g!self g!dummy name body)
   (-> Code Code Text Code Code)
-  (` ((.All ((~ g!self) (~ g!dummy))
-        (~ (let$ (local_symbol$ name) (` {.#Apply (..Primitive "") (~ g!self)})
-                 body)))
-      (..Primitive ""))))
+  (` {.#Apply (..Primitive "")
+              (.All ((~ g!self) (~ g!dummy))
+                (~ (let$ (local_symbol$ name) (` {.#Apply (..Primitive "") (~ g!self)})
+                         body)))}))
 
 (macro: .public (Rec tokens)
   (case tokens
diff --git a/stdlib/source/library/lux/tool/compiler.lux b/stdlib/source/library/lux/tool/compiler.lux
index 138f2ccf9..f2210209a 100644
--- a/stdlib/source/library/lux/tool/compiler.lux
+++ b/stdlib/source/library/lux/tool/compiler.lux
@@ -40,6 +40,10 @@
 (type: .public (Compiler s d o)
   (-> Input (Compilation s d o)))
 
+(type: .public Custom
+  (Ex (_ state document object)
+    (-> (List Text) (Try [state (Compiler state document object)]))))
+
 (type: .public (Instancer s d o)
   (-> (Key d) (List Parameter) (Compiler s d o)))
 
diff --git a/stdlib/source/library/lux/tool/compiler/default/platform.lux b/stdlib/source/library/lux/tool/compiler/default/platform.lux
index 42d8b9958..ef79450e9 100644
--- a/stdlib/source/library/lux/tool/compiler/default/platform.lux
+++ b/stdlib/source/library/lux/tool/compiler/default/platform.lux
@@ -1,9 +1,9 @@
 (.using
  [library
   [lux "*"
-   [type {"+" :sharing}]
    ["@" target]
    ["[0]" debug]
+   ["[0]" meta]
    [abstract
     ["[0]" monad {"+" Monad do}]]
    [control
@@ -27,6 +27,8 @@
      ["[0]" list ("[1]#[0]" monoid functor mix)]]
     [format
      ["_" binary {"+" Writer}]]]
+   [type {"+" :sharing}
+    ["[0]" check]]
    [world
     ["[0]" file {"+" Path}]
     ["[0]" console]]]]
@@ -49,7 +51,8 @@
      [phase
       ["[0]" extension {"+" Extender}]]]]
    [meta
-    [cli {"+" Compilation Library}]
+    [cli {"+" Compilation Library}
+     ["[0]" compiler {"+" Compiler}]]
     ["[0]" archive {"+" Output Archive}
      ["[0]" registry {"+" Registry}]
      ["[0]" artifact]
@@ -716,6 +719,13 @@
                     [_ (ioW.freeze (value@ #&file_system platform) static archive)]
                     (async#in {try.#Failure error}))))))))
 
+      (exception: .public (invalid_custom_compiler [definition Symbol
+                                                    type Type])
+        (exception.report
+         ["Definition" (%.symbol definition)]
+         ["Expected Type" (%.type ///.Custom)]
+         ["Actual Type" (%.type type)]))
+
       (def: .public (compile phase_wrapper import static expander platform compilation context)
         (All (_ <type_vars>)
           (-> ///phase.Wrapper Import Static Expander <Platform> Compilation <Context> <Return>))
@@ -723,5 +733,28 @@
               compiler (|> (..compiler phase_wrapper expander platform)
                            (serial_compiler import static platform sources)
                            (..parallel context))]
-          (compiler descriptor.runtime module)))
+          (do [! ..monad]
+            [customs (|> compilers
+                         (list#each (function (_ it)
+                                      (let [/#definition (value@ compiler.#definition it)
+                                            [/#module /#name] /#definition
+                                            /#parameters (value@ compiler.#parameters it)]
+                                        (do !
+                                          [[archive state] (compiler descriptor.runtime /#module)
+                                           .let [meta_state (value@ [extension.#state
+                                                                     ///directive.#analysis
+                                                                     ///directive.#state
+                                                                     extension.#state]
+                                                                    state)]
+                                           [_ /#type /#value] (|> /#definition
+                                                                  meta.export
+                                                                  (meta.result meta_state)
+                                                                  async#in)]
+                                          (async#in (if (check.subsumes? ///.Custom /#type)
+                                                      (|> /#value
+                                                          (:as ///.Custom)
+                                                          (function.on /#parameters))
+                                                      (exception.except ..invalid_custom_compiler [/#definition /#type])))))))
+                         (monad.all !))]
+            (compiler descriptor.runtime module))))
       )))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
index 893f9df5a..1b693629a 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/inference.lux
@@ -7,6 +7,7 @@
    [control
     [pipe {"+" case>}]
     ["[0]" maybe]
+    ["[0]" try]
     ["[0]" exception {"+" exception:}]]
    [data
     ["[0]" text
@@ -71,6 +72,38 @@
      [id _] (/type.check check.existential)]
     (in {.#Primitive (format ..prefix module "#" (%.nat id)) (list)})))
 
+(def: .public (quantified @var @parameter :it:)
+  (-> check.Var Nat Type Type)
+  (case :it:
+    {.#Primitive name co_variant}
+    {.#Primitive name (list#each (quantified @var @parameter) co_variant)}
+
+    (^template [<tag>]
+      [{<tag> left right}
+       {<tag> (quantified @var @parameter left)
+              (quantified @var @parameter right)}])
+    ([.#Sum]
+     [.#Product]
+     [.#Function]
+     [.#Apply])
+    
+    {.#Var @}
+    (if (n.= @var @)
+      {.#Parameter @parameter}
+      :it:)
+
+    (^template [<tag>]
+      [{<tag> env body}
+       {<tag> (list#each (quantified @var @parameter) env)
+              (quantified @var (n.+ 2 @parameter) body)}])
+    ([.#UnivQ]
+     [.#ExQ])
+
+    (^or {.#Parameter @}
+         {.#Ex @}
+         {.#Named name anonymous})
+    :it:))
+
 ... 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
@@ -93,13 +126,13 @@
 
       {.#UnivQ _}
       (do phase.monad
-        [[var_id varT] (/type.check check.var)]
-        (general archive analyse (maybe.trusted (type.applied (list varT) inferT)) args))
+        [[@var :var:] (/type.check check.var)]
+        (general archive analyse (maybe.trusted (type.applied (list :var:) inferT)) args))
 
       {.#ExQ _}
-      (do [! phase.monad]
-        [exT ..existential]
-        (general archive analyse (maybe.trusted (type.applied (list exT) inferT)) args))
+      (do phase.monad
+        [:ex: ..existential]
+        (general archive analyse (maybe.trusted (type.applied (list :ex:) inferT)) args))
 
       {.#Apply inputT transT}
       (case (type.applied (list inputT) transT)
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
index 7e06dc71a..c066115ec 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/analysis/type.lux
@@ -43,10 +43,20 @@
     [expectedT (extension.lifted meta.expected_type)]
     (..check (check.check expectedT actualT))))
 
+(def: .public (with_var it)
+  (All (_ a) (-> (-> [check.Var Type] (Operation a))
+                 (Operation a)))
+  (do phase.monad
+    [var (..check check.var)
+     .let [[@it :it:] var]
+     it (it var)
+     _ (..check (check.forget! @it))]
+    (in it)))
+
 (def: .public (inferring action)
   (All (_ a) (-> (Operation a) (Operation [Type a])))
   (do phase.monad
-    [[_ varT] (..check check.var)
-     output (..expecting varT action)
-     knownT (..check (check.clean varT))]
-    (in [knownT output])))
+    [[@it :it:] (..check check.var)
+     it (..expecting :it: action)
+     :it: (..check (check.clean :it:))]
+    (in [:it: it])))
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 347604a35..b91550f39 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
@@ -6,12 +6,16 @@
     monad]
    [control
     ["[0]" maybe]
-    ["ex" exception {"+" exception:}]]
+    ["[0]" try]
+    ["[0]" exception {"+" exception:}]]
    [data
     ["[0]" text
      ["%" format {"+" format}]]
     [collection
      ["[0]" list ("[1]#[0]" monoid monad)]]]
+   [math
+    [number
+     ["n" nat]]]
    ["[0]" type
     ["[0]" check]]]]
  ["[0]" /// "_"
@@ -30,29 +34,44 @@
                                      function Text
                                      argument Text
                                      body Code])
-  (ex.report ["Type" (%.type expected)]
-             ["Function" function]
-             ["Argument" argument]
-             ["Body" (%.code body)]))
+  (exception.report
+   ["Type" (%.type expected)]
+   ["Function" function]
+   ["Argument" argument]
+   ["Body" (%.code body)]))
 
-(exception: .public (cannot_apply [functionT Type
+(exception: .public (cannot_apply [:function: Type
                                    functionC Code
                                    arguments (List Code)])
-  (ex.report ["Function type" (%.type functionT)]
-             ["Function" (%.code functionC)]
-             ["Arguments" (|> arguments
-                              list.enumeration
-                              (list#each (.function (_ [idx argC])
-                                           (format (%.nat idx) " " (%.code argC))))
-                              (text.interposed text.new_line))]))
+  (exception.report
+   ["Function type" (%.type :function:)]
+   ["Function" (%.code functionC)]
+   ["Arguments" (|> arguments
+                    list.enumeration
+                    (list#each (.function (_ [idx argC])
+                                 (format (%.nat idx) " " (%.code argC))))
+                    (text.interposed text.new_line))]))
 
 (def: .public (function analyse function_name arg_name archive body)
   (-> Phase Text Text Phase)
   (do [! ///.monad]
-    [functionT (///extension.lifted meta.expected_type)]
-    (loop [expectedT functionT]
+    [:function: (///extension.lifted meta.expected_type)]
+    (loop [expectedT :function:]
       (/.with_exception ..cannot_analyse [expectedT function_name arg_name body]
         (case expectedT
+          {.#Function :input: :output:}
+          (<| (# ! each (.function (_ [scope bodyA])
+                          {/.#Function (list#each (|>> /.variable)
+                                                  (/scope.environment scope))
+                                       bodyA}))
+              /scope.with
+              ... Functions have access not only to their argument, but
+              ... also to themselves, through a local variable.
+              (/scope.with_local [function_name expectedT])
+              (/scope.with_local [arg_name :input:])
+              (/type.expecting :output:)
+              (analyse archive body))
+          
           {.#Named name unnamedT}
           (again unnamedT)
 
@@ -62,7 +81,7 @@
             (again value)
 
             {.#None}
-            (/.failure (ex.error cannot_analyse [expectedT function_name arg_name body])))
+            (/.failure (exception.error ..cannot_analyse [expectedT function_name arg_name body])))
 
           (^template [<tag> <instancer>]
             [{<tag> _}
@@ -82,33 +101,34 @@
               ... Inference
               _
               (do !
-                [[input_id inputT] (/type.check check.var)
-                 [output_id outputT] (/type.check check.var)
-                 .let [functionT {.#Function inputT outputT}]
-                 functionA (again functionT)
-                 _ (/type.check (check.check expectedT functionT))]
+                [[@input :input:] (/type.check check.var)
+                 [@output :output:] (/type.check check.var)
+                 .let [:function: {.#Function :input: :output:}]
+                 functionA (again :function:)
+                 specialization (/type.check (check.try (check.identity (list @output) @input)))
+                 :function: (case specialization
+                              {try.#Success :input:'}
+                              (in :function:)
+
+                              {try.#Failure _}
+                              (/type.check
+                               (do [! check.monad]
+                                 [? (check.linked? @input @output)]
+                                 (# ! each
+                                    (|>> {.#Function :input:} (/inference.quantified @input 1) {.#UnivQ (list)})
+                                    (if ?
+                                      (in :input:)
+                                      (check.identity (list @input) @output))))))
+                 _ (/type.check (check.check expectedT :function:))]
                 (in functionA))))
 
-          {.#Function inputT outputT}
-          (<| (# ! each (.function (_ [scope bodyA])
-                          {/.#Function (list#each (|>> /.variable)
-                                                  (/scope.environment scope))
-                                       bodyA}))
-              /scope.with
-              ... Functions have access not only to their argument, but
-              ... also to themselves, through a local variable.
-              (/scope.with_local [function_name expectedT])
-              (/scope.with_local [arg_name inputT])
-              (/type.expecting outputT)
-              (analyse archive body))
-          
           _
           (/.failure "")
           )))))
 
-(def: .public (apply analyse argsC+ functionT functionA archive functionC)
+(def: .public (apply analyse argsC+ :function: functionA archive functionC)
   (-> Phase (List Code) Type Analysis Phase)
-  (<| (/.with_exception ..cannot_apply [functionT functionC argsC+])
+  (<| (/.with_exception ..cannot_apply [:function: functionC argsC+])
       (do ///.monad
-        [[applyT argsA+] (/inference.general archive analyse functionT argsC+)])
+        [[applyT argsA+] (/inference.general archive analyse :function: argsC+)])
       (in (/.reified [functionA argsA+]))))
diff --git a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux
index 4632aa193..d747ff070 100644
--- a/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux
+++ b/stdlib/source/library/lux/tool/compiler/language/lux/phase/extension/analysis/lux.lux
@@ -124,10 +124,10 @@
 (def: lux::is
   Handler
   (function (_ extension_name analyse archive args)
-    (do ////.monad
-      [[var_id varT] (typeA.check check.var)]
-      ((binary varT varT Bit extension_name)
-       analyse archive args))))
+    (<| typeA.with_var
+        (function (_ [@var :var:]))
+        ((binary :var: :var: Bit extension_name)
+         analyse archive args))))
 
 ... "lux try" provides a simple way to interact with the host platform's
 ... error_handling facilities.
diff --git a/stdlib/source/library/lux/type.lux b/stdlib/source/library/lux/type.lux
index 380331c40..ac81fe26b 100644
--- a/stdlib/source/library/lux/type.lux
+++ b/stdlib/source/library/lux/type.lux
@@ -1,31 +1,31 @@
 (.using
-  [library
-   [lux {"-" function :as}
-    ["@" target]
-    [abstract
-     [equivalence {"+" Equivalence}]
-     [monad {"+" Monad do}]]
-    [control
-     ["[0]" function]
-     ["[0]" maybe]
-     ["[0]" exception {"+" exception:}]
-     ["<>" parser
-      ["<[0]>" code {"+" Parser}]]]
-    [data
-     ["[0]" product]
-     ["[0]" text ("[1]#[0]" monoid equivalence)]
-     [collection
-      ["[0]" array]
-      ["[0]" list ("[1]#[0]" functor monoid mix)]]]
-    ["[0]" macro
-     [syntax {"+" syntax:}]
-     ["[0]" code]]
-    [math
-     [number
-      ["n" nat ("[1]#[0]" decimal)]]]
-    ["[0]" meta
-     ["[0]" location]
-     ["[0]" symbol ("[1]#[0]" equivalence codec)]]]])
+ [library
+  [lux {"-" function :as}
+   ["@" target]
+   [abstract
+    [equivalence {"+" Equivalence}]
+    [monad {"+" Monad do}]]
+   [control
+    ["[0]" function]
+    ["[0]" maybe]
+    ["[0]" exception {"+" exception:}]
+    ["<>" parser
+     ["<[0]>" code {"+" Parser}]]]
+   [data
+    ["[0]" product]
+    ["[0]" text ("[1]#[0]" monoid equivalence)]
+    [collection
+     ["[0]" array]
+     ["[0]" list ("[1]#[0]" functor monoid mix)]]]
+   ["[0]" macro
+    [syntax {"+" syntax:}]
+    ["[0]" code]]
+   [math
+    [number
+     ["n" nat ("[1]#[0]" decimal)]]]
+   ["[0]" meta
+    ["[0]" location]
+    ["[0]" symbol ("[1]#[0]" equivalence codec)]]]])
 
 (template [<name> <tag>]
   [(def: .public (<name> type)
@@ -466,3 +466,32 @@
                      (~ extraction)
                      ... The value of this expression will never be relevant, so it doesn't matter what it is.
                      (.:as .Nothing [])))))))
+
+(def: .public (replaced before after)
+  (-> Type Type Type Type)
+  (.function (again it)
+    (if (# ..equivalence = before it)
+      after
+      (case it
+        {.#Primitive name co_variant}
+        {.#Primitive name (list#each again co_variant)}
+
+        (^template [<tag>]
+          [{<tag> left right}
+           {<tag> (again left) (again right)}])
+        ([.#Sum]
+         [.#Product]
+         [.#Function]
+         [.#Apply])
+
+        (^template [<tag>]
+          [{<tag> env body}
+           {<tag> (list#each again env) (again body)}])
+        ([.#UnivQ]
+         [.#ExQ])
+        
+        (^or {.#Parameter _}
+             {.#Var _}
+             {.#Ex _}
+             {.#Named _})
+        it))))
diff --git a/stdlib/source/library/lux/type/check.lux b/stdlib/source/library/lux/type/check.lux
index 90e94478b..31ec9da05 100644
--- a/stdlib/source/library/lux/type/check.lux
+++ b/stdlib/source/library/lux/type/check.lux
@@ -1,25 +1,25 @@
 (.using
-  [library
-   [lux "*"
-    ["@" target]
-    [abstract
-     [functor {"+" Functor}]
-     [apply {"+" Apply}]
-     ["[0]" monad {"+" Monad do}]]
-    [control
-     ["[0]" maybe]
-     ["[0]" try {"+" Try}]
-     ["[0]" exception {"+" Exception exception:}]]
-    [data
-     ["[0]" product]
-     ["[0]" text ("[1]#[0]" monoid equivalence)]
-     [collection
-      ["[0]" list]
-      ["[0]" set {"+" Set}]]]
-    [math
-     [number
-      ["n" nat ("[1]#[0]" decimal)]]]]]
-  ["[0]" // ("[1]#[0]" equivalence)])
+ [library
+  [lux {"-" try}
+   ["@" target]
+   [abstract
+    [functor {"+" Functor}]
+    [apply {"+" Apply}]
+    ["[0]" monad {"+" Monad do}]]
+   [control
+    ["[0]" maybe]
+    ["[0]" try {"+" Try}]
+    ["[0]" exception {"+" Exception exception:}]]
+   [data
+    ["[0]" product]
+    ["[0]" text ("[1]#[0]" monoid equivalence)]
+    [collection
+     ["[0]" list ("[1]#[0]" mix)]
+     ["[0]" set {"+" Set}]]]
+   [math
+    [number
+     ["n" nat ("[1]#[0]" decimal)]]]]]
+ ["[0]" // ("[1]#[0]" equivalence)])
 
 (template: (!n#= reference subject)
   [("lux i64 =" reference subject)])
@@ -249,17 +249,21 @@
       _
       (exception.except ..unknown_type_var id))))
 
-(def: (re_bind type id)
-  (-> Type Var (Check Any))
+(def: (re_bind' ?type id)
+  (-> (Maybe Type) Var (Check Any))
   (function (_ context)
     (case (|> context (value@ .#var_bindings) (var::get id))
       {.#Some _}
-      {try.#Success [(revised@ .#var_bindings (var::put id {.#Some type}) context)
+      {try.#Success [(revised@ .#var_bindings (var::put id ?type) context)
                      []]}
       
       _
       (exception.except ..unknown_type_var id))))
 
+(def: (re_bind type id)
+  (-> Type Var (Check Any))
+  (re_bind' {.#Some type} id))
+
 (def: .public var
   (Check [Var Type])
   (function (_ context)
@@ -298,26 +302,21 @@
 (type: Ring
   (Set Var))
 
-(def: empty_ring
-  Ring
-  (set.empty n.hash))
-
-... TODO: Optimize this by not using sets anymore.
-(def: (ring start)
-  (-> Var (Check Ring))
+(def: (ring' start)
+  (-> Var (Check (List Var)))
   (function (_ context)
     (loop [current start
-           output (set.has start empty_ring)]
+           output (list start)]
       (case (|> context (value@ .#var_bindings) (var::get current))
         {.#Some {.#Some type}}
         (case type
-          {.#Var post}
-          (if (!n#= start post)
+          {.#Var next}
+          (if (!n#= start next)
             {try.#Success [context output]}
-            (again post (set.has post output)))
+            (again next (list& next output)))
           
           _
-          {try.#Success [context empty_ring]})
+          {try.#Success [context (list)]})
 
         {.#Some {.#None}}
         {try.#Success [context output]}
@@ -325,22 +324,114 @@
         {.#None}
         (exception.except ..unknown_type_var current)))))
 
+... TODO: Optimize this by not using sets anymore.
+(def: ring
+  (-> Var (Check Ring))
+  (|>> ..ring'
+       (check#each (set.of_list n.hash))))
+
+(def: .public (linked? @0 @1)
+  (-> Var Var (Check Bit))
+  (check#each (function (_ it)
+                (set.member? it @1))
+              (..ring @0)))
+
+(exception: (invalid_alias [var Var
+                            expected (List Var)
+                            actual (List Var)])
+  (exception.report
+   ["Var" (n#encoded var)]
+   ["Expected" (exception.listing n#encoded expected)]
+   ["Actual" (exception.listing n#encoded actual)]))
+
+(exception: (cannot_identify [var Var])
+  (exception.report
+   ["Var" (n#encoded var)]))
+
+(def: .public (identity aliases @)
+  (-> (List Var) Var (Check Type))
+  (do [! ..monad]
+    [:bound: (..peek @)]
+    (case :bound:
+      {.#Some :bound:}
+      (in :bound:)
+
+      {.#None}
+      (do !
+        [existing_aliases (..ring @)
+         _ (if (list.every? (set.member? existing_aliases) aliases)
+             (in [])
+             (..except ..invalid_alias [@ aliases (set.list existing_aliases)]))
+         .let [forbidden_aliases (set.of_list n.hash (list& @ aliases))
+               allowed_aliases (set.difference forbidden_aliases existing_aliases)]]
+        (case (set.list allowed_aliases)
+          {.#Item identity _}
+          (in {.#Var identity})
+          
+          {.#None}
+          (..except ..cannot_identify [@]))))))
+
+(def: (erase! @)
+  (-> Var (Check Any))
+  (function (_ context)
+    {try.#Success [(revised@ .#var_bindings
+                             (list#mix (: (:let [binding [Nat (Maybe Type)]]
+                                            (-> binding
+                                                (List binding)
+                                                (List binding)))
+                                          (function (_ in out)
+                                            (let [[@var :var:] in]
+                                              (if (n.= @ @var)
+                                                out
+                                                (list& in out)))))
+                                       (: (List [Nat (Maybe Type)])
+                                          (list)))
+                             context)
+                   []]}))
+
+(def: .public (forget! @)
+  (-> Var (Check Any))
+  (do [! ..monad]
+    [ring (..ring' @)]
+    (case ring
+      (^ (list))
+      (in [])
+      
+      (^ (list @me))
+      (erase! @me)
+      
+      (^ (list @other @me))
+      (do !
+        [_ (re_bind' {.#None} @other)]
+        (erase! @me))
+      
+      (^ (list& @prev _))
+      (case (list.reversed ring)
+        (^ (list& @me @next _))
+        (do !
+          [_ (re_bind {.#Var @next} @prev)
+           _ (re_bind {.#Var @prev} @next)]
+          (erase! @me))
+
+        _
+        (undefined)))))
+
+(def: .public (try it)
+  (All (_ a) (-> (Check a) (Check (Try a))))
+  (function (_ context)
+    (case (it context)
+      {try.#Success [context' output]}
+      {try.#Success [context' {try.#Success output}]}
+
+      {try.#Failure error}
+      {try.#Success [context {try.#Failure error}]})))
+
 (def: .public fresh_context
   Type_Context
   [.#var_counter 0
    .#ex_counter 0
    .#var_bindings (list)])
 
-(def: (attempt op)
-  (All (_ a) (-> (Check a) (Check (Maybe a))))
-  (function (_ context)
-    (case (op context)
-      {try.#Success [context' output]}
-      {try.#Success [context' {.#Some output}]}
-
-      {try.#Failure _}
-      {try.#Success [context {.#None}]})))
-
 (def: (either left right)
   (All (_ a) (-> (Check a) (Check a) (Check a)))
   (function (_ context)
@@ -396,17 +487,17 @@
   (if (!n#= idE idA)
     (check#in assumptions)
     (do [! ..monad]
-      [ebound (attempt (..bound idE))
-       abound (attempt (..bound idA))]
+      [ebound (..try (..bound idE))
+       abound (..try (..bound idA))]
       (case [ebound abound]
         ... Link the 2 variables circularly
-        [{.#None} {.#None}]
+        [{try.#Failure _} {try.#Failure _}]
         (do !
           [_ (link/2 idE idA)]
           (in assumptions))
 
         ... Interpose new variable between 2 existing links
-        [{.#Some etype} {.#None}]
+        [{try.#Success etype} {try.#Failure _}]
         (case etype
           {.#Var targetE}
           (do !
@@ -417,7 +508,7 @@
           (check' assumptions etype {.#Var idA}))
 
         ... Interpose new variable between 2 existing links
-        [{.#None} {.#Some atype}]
+        [{try.#Failure _} {try.#Success atype}]
         (case atype
           {.#Var targetA}
           (do !
@@ -427,7 +518,7 @@
           _
           (check' assumptions {.#Var idE} atype))
 
-        [{.#Some etype} {.#Some atype}]
+        [{try.#Success etype} {try.#Success atype}]
         (case [etype atype]
           [{.#Var targetE} {.#Var targetA}]
           (do !
@@ -702,9 +793,9 @@
              (check#each (|>> {<tag> leftT'}))))])
     ([.#Sum] [.#Product] [.#Function] [.#Apply])
 
-    {.#Var id}
+    {.#Var @}
     (do ..monad
-      [?actualT (peek id)]
+      [?actualT (peek @)]
       (case ?actualT
         {.#Some actualT}
         (clean actualT)
@@ -715,7 +806,8 @@
     (^template [<tag>]
       [{<tag> envT+ unquantifiedT}
        (do [! ..monad]
-         [envT+' (monad.each ! clean envT+)]
-         (in {<tag> envT+' unquantifiedT}))])
+         [envT+' (monad.each ! clean envT+)
+          unquantifiedT' (clean unquantifiedT)]
+         (in {<tag> envT+' unquantifiedT'}))])
     ([.#UnivQ] [.#ExQ])
     ))
diff --git a/stdlib/source/test/lux/target/python.lux b/stdlib/source/test/lux/target/python.lux
index 39c51b2a7..6eed5ecab 100644
--- a/stdlib/source/test/lux/target/python.lux
+++ b/stdlib/source/test/lux/target/python.lux
@@ -324,6 +324,31 @@
                                         (list (/.float float/0) (/.float float/1) (/.float float/2)))))
         )))
 
+(def: test|var
+  Test
+  (do [! random.monad]
+    [expected/0 random.safe_frac
+     expected/1 random.safe_frac
+     choice (# ! each (n.% 2) random.nat)
+     .let [expected/? (case choice
+                        0 expected/0
+                        _ expected/1)]
+     $var (# ! each (|>> %.nat (format "v") /.var) random.nat)
+     $choice (# ! each (|>> %.nat (format "c") /.var) random.nat)]
+    ($_ _.and
+        (_.cover [/.Single /.SVar /.var]
+                 (expression (|>> (:as Frac) (f.= expected/0))
+                             (/.apply/* (/.lambda (list $var) $var)
+                                        (list (/.float expected/0)))))
+        (_.cover [/.Poly /.PVar /.poly]
+                 (expression (|>> (:as Frac) (f.= expected/?))
+                             (/.apply/* (/.lambda (list $choice (/.poly $var))
+                                                  (/.item $choice $var))
+                                        (list (/.int (.int choice))
+                                              (/.float expected/0)
+                                              (/.float expected/1)))))
+        )))
+
 (def: test|expression
   Test
   (do [! random.monad]
@@ -335,6 +360,8 @@
             (_.for [/.Computation]
                    ..test|computation)
             ..test|function
+            (_.for [/.Var]
+                   ..test|var)
             ))))
 
 (def: .public test
diff --git a/stdlib/source/test/lux/tool.lux b/stdlib/source/test/lux/tool.lux
index 0f42f81db..c9a5cfb7c 100644
--- a/stdlib/source/test/lux/tool.lux
+++ b/stdlib/source/test/lux/tool.lux
@@ -17,7 +17,8 @@
       ["[1]/[0]" analysis "_"
        ["[1]/[0]" simple]
        ["[1]/[0]" complex]
-       ["[1]/[0]" reference]]
+       ["[1]/[0]" reference]
+       ["[1]/[0]" function]]
       ... ["[1]/[0]" synthesis]
       ]]]
    ["[1][0]" meta "_"
@@ -41,6 +42,7 @@
       /phase/analysis/simple.test
       /phase/analysis/complex.test
       /phase/analysis/reference.test
+      /phase/analysis/function.test
       ... /syntax.test
       ... /synthesis.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
index fa3df9c67..97bdb7a54 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
@@ -78,7 +78,7 @@
     {try.#Failure error}
     (text.contains? (value@ exception.#label exception) error)))
 
-(def: simple_parameter
+(def: .public simple_parameter
   (Random [Type Code])
   (`` ($_ random.either
           (~~ (template [<type> <random> <code>]
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
index f559e98c4..ed111c5e4 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
@@ -230,7 +230,6 @@
                    (list.item tag)
                    (maybe.else ""))]]
     ($_ _.and
-        ..test|sum
         (_.cover [/.variant]
                  (let [expected_variant? (: (-> Symbol Bit)
                                             (function (_ tag)
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
index 815b488fe..50fbc1c50 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
@@ -1,133 +1,253 @@
 (.using
+ [library
   [lux "*"
-   [abstract
-    ["[0]" monad {"+" do}]]
-   [data
-    ["%" text/format {"+" format}]]
-   ["r" math/random {"+" Random}]
    ["_" test {"+" Test}]
+   [abstract
+    [monad {"+" do}]]
    [control
-    pipe
-    ["[0]" maybe]
-    ["[0]" try]]
+    [pipe {"+" case>}]
+    ["[0]" function]
+    ["[0]" try ("[1]#[0]" functor)]
+    ["[0]" exception]]
    [data
     ["[0]" product]
-    ["[0]" text ("[1]#[0]" equivalence)]
-    [number
-     ["n" nat]]
+    ["[0]" text
+     ["%" format]]
     [collection
-     ["[0]" list ("[1]#[0]" functor)]]]
-   ["[0]" type]
-   ["[0]" macro
+     ["[0]" list]]]
+   [macro
     ["[0]" code]]
+   [math
+    ["[0]" random]
+    [number
+     ["n" nat]]]
    [meta
-    ["[0]" symbol]]]
-  [//
-   ["_[0]" primitive]
-   ["_[0]" structure]]
-  [\\
-   ["[0]" /
-    ["/[1]" //
-     ["[1][0]" module]
-     ["[1][0]" type]
-     ["/[1]" // "_"
-      ["/[1]" //
-       ["[1][0]" analysis {"+" Analysis Operation}]
-       [///
-        ["[1][0]" reference]
-        ["[0]" phase]
-        [meta
-         ["[0]" archive]]]]]]]])
-
-(def: (check_apply expectedT num_args analysis)
-  (-> Type Nat (Operation Analysis) Bit)
-  (|> analysis
-      (//type.with_type expectedT)
-      (phase.result _primitive.state)
-      (case> {try.#Success applyA}
-             (let [[funcA argsA] (////analysis.application applyA)]
-               (n.= num_args (list.size argsA)))
-
-             {try.#Failure _}
-             false)))
-
-(def: abstraction
-  (do r.monad
-    [func_name (r.unicode 5)
-     arg_name (|> (r.unicode 5) (r.only (|>> (text#= func_name) not)))
-     [outputT outputC] _primitive.primitive
-     [inputT _] _primitive.primitive
-     .let [g!arg (code.local_symbol arg_name)]]
-    (<| (_.context (%.symbol (symbol /.function)))
-        ($_ _.and
-            (_.test "Can analyse function."
-                    (and (|> (//type.with_type (All (_ a) (-> a outputT))
-                               (/.function _primitive.phase func_name arg_name archive.empty outputC))
-                             _structure.check_succeeds)
-                         (|> (//type.with_type (All (_ a) (-> a a))
-                               (/.function _primitive.phase func_name arg_name archive.empty g!arg))
-                             _structure.check_succeeds)))
-            (_.test "Generic functions can always be specialized."
-                    (and (|> (//type.with_type (-> inputT outputT)
-                               (/.function _primitive.phase func_name arg_name archive.empty outputC))
-                             _structure.check_succeeds)
-                         (|> (//type.with_type (-> inputT inputT)
-                               (/.function _primitive.phase func_name arg_name archive.empty g!arg))
-                             _structure.check_succeeds)))
-            (_.test "The function's name is bound to the function's type."
-                    (|> (//type.with_type (Rec self (-> inputT self))
-                          (/.function _primitive.phase func_name arg_name archive.empty (code.local_symbol func_name)))
-                        _structure.check_succeeds))
-            ))))
+    ["[0]" symbol "_"
+     ["$[1]" \\test]]]
+   ["[0]" type ("[1]#[0]" equivalence)
+    ["$[1]" \\test]
+    ["[0]" check]]]]
+ [\\library
+  ["[0]" /
+   ["/[1]" //
+    [//
+     ["[1][0]" extension
+      ["[1]/[0]" analysis "_"
+       ["[1]" lux]]]
+     [//
+      ["[1][0]" analysis {"+" Analysis}
+       [evaluation {"+" Eval}]
+       ["[2][0]" macro]
+       ["[2][0]" scope]
+       ["[2][0]" module]
+       ["[2][0]" type
+        ["$[1]" \\test]]
+       ["[2][0]" inference "_"
+        ["$[1]" \\test]]]
+      [///
+       ["[1][0]" phase ("[1]#[0]" monad)]
+       [meta
+        ["[0]" archive]]]]]]]])
 
-(def: apply
-  (do [! r.monad]
-    [full_args (|> r.nat (# ! each (|>> (n.% 10) (n.max 2))))
-     partial_args (|> r.nat (# ! each (n.% full_args)))
-     var_idx (|> r.nat (# ! each (|>> (n.% full_args) (n.max 1))))
-     inputsTC (r.list full_args _primitive.primitive)
-     .let [inputsT (list#each product.left inputsTC)
-           inputsC (list#each product.right inputsTC)]
-     [outputT outputC] _primitive.primitive
-     .let [funcT (type.function inputsT outputT)
-           partialT (type.function (list.after partial_args inputsT) outputT)
-           varT {.#Parameter 1}
-           polyT (<| (type.univ_q 1)
-                     (type.function (list.together (list (list.first var_idx inputsT)
-                                                         (list varT)
-                                                         (list.after (++ var_idx) inputsT))))
-                     varT)
-           poly_inputT (maybe.trusted (list.item var_idx inputsT))
-           partial_poly_inputsT (list.after (++ var_idx) inputsT)
-           partial_polyT1 (<| (type.function partial_poly_inputsT)
-                              poly_inputT)
-           partial_polyT2 (<| (type.univ_q 1)
-                              (type.function {.#Item varT partial_poly_inputsT})
-                              varT)
-           dummy_function {////analysis.#Function (list) {////analysis.#Reference (////reference.local 1)}}]]
-    (<| (_.context (%.symbol (symbol /.apply)))
-        ($_ _.and
-            (_.test "Can analyse monomorphic type application."
-                    (|> (/.apply _primitive.phase inputsC funcT dummy_function archive.empty (' []))
-                        (check_apply outputT full_args)))
-            (_.test "Can partially apply functions."
-                    (|> (/.apply _primitive.phase (list.first partial_args inputsC) funcT dummy_function archive.empty (' []))
-                        (check_apply partialT partial_args)))
-            (_.test "Can apply polymorphic functions."
-                    (|> (/.apply _primitive.phase inputsC polyT dummy_function archive.empty (' []))
-                        (check_apply poly_inputT full_args)))
-            (_.test "Polymorphic partial application propagates found type-vars."
-                    (|> (/.apply _primitive.phase (list.first (++ var_idx) inputsC) polyT dummy_function archive.empty (' []))
-                        (check_apply partial_polyT1 (++ var_idx))))
-            (_.test "Polymorphic partial application preserves quantification for type-vars."
-                    (|> (/.apply _primitive.phase (list.first var_idx inputsC) polyT dummy_function archive.empty (' []))
-                        (check_apply partial_polyT2 var_idx)))
-            ))))
+(def: (eval archive type term)
+  Eval
+  (//phase#in []))
+
+(def: (expander macro inputs state)
+  //macro.Expander
+  {try.#Success ((.macro macro) inputs state)})
+
+(def: analysis
+  //analysis.Phase
+  (//.phase ..expander))
+
+(def: test|function
+  Test
+  (do [! random.monad]
+    [lux $//type.random_state
+     .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+                  //extension.#state lux]]
+     input/0 ($type.random 0)
+     input/1 ($type.random 0)
+     function/0 (random.ascii/lower 1)
+     function/1 (random.ascii/lower 2)
+     argument/0 (random.ascii/lower 3)
+     argument/1 (random.ascii/lower 4)
+     module/0 (random.ascii/lower 5)
+     [output/0 term/0] $//inference.simple_parameter
+     [output/1 term/1] (random.only (|>> product.left (same? output/0) not)
+                                    $//inference.simple_parameter)
+     name/0 ($symbol.random 1 1)
+     .let [$function/0 (code.local_symbol function/0)
+           $function/1 (code.local_symbol function/1)
+           $argument/0 (code.local_symbol argument/0)
+           $argument/1 (code.local_symbol argument/1)]]
+    ($_ _.and
+        (_.cover [/.function]
+                 (let [function?' (: (-> Type Code (-> [(List Analysis) Analysis] Bit) Bit)
+                                     (function (_ function_type output_term ?)
+                                       (|> (do //phase.monad
+                                             [analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+                                                             output_term)
+                                                           (//type.expecting function_type))]
+                                             (in (case analysis
+                                                   {//analysis.#Function it}
+                                                   (? it)
+
+                                                   _
+                                                   false)))
+                                           (//module.with 0 module/0)
+                                           (//phase#each product.right)
+                                           (//phase.result state)
+                                           (try.else false))))
+                       function? (: (-> Type Code Bit)
+                                    (function (_ function_type output_term)
+                                      (function?' function_type output_term (function.constant true))))
+                       inferring? (: (-> Type Code Bit)
+                                     (function (_ :expected: term)
+                                       (|> (do //phase.monad
+                                             [[:actual: analysis] (|> (/.function ..analysis function/0 argument/0 archive.empty
+                                                                        term)
+                                                                      //type.inferring)]
+                                             (in (case analysis
+                                                   {//analysis.#Function [actual_env actual_body]}
+                                                   (type#= :expected: :actual:)
+
+                                                   _
+                                                   false)))
+                                           (//module.with 0 module/0)
+                                           (//phase#each product.right)
+                                           (//phase.result state)
+                                           (try.else false))))]
+                   (and (function? (-> input/0 output/0) term/0)
+                        (function? (-> input/0 input/0) $argument/0)
+
+                        (function? {.#Named name/0 (-> input/0 output/0)} term/0)
+                        
+                        (function? (All (_ a) (-> a a)) $argument/0)
+                        (function? (Ex (_ a) (-> a a)) $argument/0)
+                        (function? (Ex (_ a) (-> input/0 a)) term/0)
+                        (function? (Ex (_ a) (-> a a)) term/0)
+                        (function? (Rec self (-> input/0 self)) $function/0)
+
+                        (function? (type ((All (_ a) (-> a a)) output/0)) term/0)
+                        (not (function? (type ((All (_ a) (-> a a)) output/1)) term/0))
+
+                        (function? (type ((Ex (_ a) (-> a a)) output/0)) term/0)
+                        (not (function? (type ((Ex (_ a) (-> a a)) output/1)) term/0))
+
+                        (function?' (-> input/0 input/1 input/0) (` ([(~ $function/1) (~ $argument/1)] (~ $argument/0)))
+                                    (function (_ [outer body])
+                                      (and (list.empty? outer)
+                                           (case body
+                                             {//analysis.#Function [inner body]}
+                                             (n.= 1 (list.size inner))
+
+                                             _
+                                             false))))
+                        (function?' (-> input/0 input/1 input/1) (` ([(~ $function/1) (~ $argument/1)] (~ $argument/1)))
+                                    (function (_ [outer body])
+                                      (and (list.empty? outer)
+                                           (case body
+                                             {//analysis.#Function [inner body]}
+                                             (n.= 0 (list.size inner))
+
+                                             _
+                                             false))))
+
+                        (|> (do //phase.monad
+                              [[@var :var:] (//type.check check.var)
+                               _ (//type.check (check.check :var: (-> input/0 output/0)))
+                               analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+                                              term/0)
+                                            (//type.expecting :var:))]
+                              (in (case analysis
+                                    {//analysis.#Function [actual_env actual_body]}
+                                    true
+
+                                    _
+                                    false)))
+                            (//module.with 0 module/0)
+                            (//phase#each product.right)
+                            (//phase.result state)
+                            (try.else false))
+                        
+                        (inferring? (All (_ a) (-> a output/0)) term/0)
+                        (inferring? (All (_ a) (-> a a)) $argument/0)
+                        (inferring? (All (_ @0) (-> @0 @0 (And .Bit @0)))
+                                    (` ([(~ $function/1) (~ $argument/1)]
+                                        [("lux is" (~ $argument/0) (~ $argument/1))
+                                         (~ $argument/1)]))))))
+        (_.cover [/.cannot_analyse]
+                 (|> (do //phase.monad
+                       [analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+                                       term/1)
+                                     (//type.expecting (-> input/0 output/0)))]
+                       (in (case analysis
+                             {//analysis.#Function [actual_env actual_body]}
+                             true
+
+                             _
+                             false)))
+                     (//module.with 0 module/0)
+                     (//phase#each product.right)
+                     (//phase.result state)
+                     (exception.otherwise (text.contains? (value@ exception.#label /.cannot_analyse)))))
+        )))
 
 (def: .public test
   Test
-  (<| (_.context (symbol.module (symbol /._)))
-      ($_ _.and
-          ..abstraction
-          ..apply
-          )))
+  (<| (_.covering /._)
+      (do [! random.monad]
+        [lux $//type.random_state
+         .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+                      //extension.#state lux]]
+         [input/0 term/0] $//inference.simple_parameter
+         [input/1 term/1] $//inference.simple_parameter
+         output/0 ($type.random 0)
+         module/0 (random.ascii/lower 1)]
+        ($_ _.and
+            ..test|function
+            (_.cover [/.apply]
+                     (let [reification? (: (-> Type (List Code) Type Bit)
+                                           (function (_ :abstraction: terms :expected:)
+                                             (|> (do //phase.monad
+                                                   [[:actual: analysis] (|> (/.apply ..analysis terms
+                                                                                     :abstraction:
+                                                                                     (//analysis.unit)
+                                                                                     archive.empty
+                                                                                     (' []))
+                                                                            //type.inferring)]
+                                                   (in (and (check.subsumes? :expected: :actual:)
+                                                            (case analysis
+                                                              {//analysis.#Apply _}
+                                                              true
+
+                                                              _
+                                                              false))))
+                                                 (//module.with 0 module/0)
+                                                 (//phase#each product.right)
+                                                 (//phase.result state)
+                                                 (try.else false))))]
+                       (and (reification? (-> input/0 input/1 output/0) (list term/0 term/1) output/0)
+                            (reification? (-> input/0 input/1 output/0) (list term/0) (-> input/1 output/0))
+                            (reification? (All (_ a) (-> a a)) (list term/0) input/0)
+                            (reification? (All (_ a) (-> a a a)) (list term/0) (-> input/0 input/0))
+                            (reification? (All (_ a) (-> input/0 a)) (list term/0) .Nothing)
+                            (reification? (All (_ a b) (-> a b a)) (list term/0) (All (_ b) (-> b input/0)))
+                            (reification? (Ex (_ a) (-> a input/0)) (list (` ("lux io error" ""))) input/0)
+                            (reification? (Ex (_ a) (-> input/0 a)) (list term/0) .Any))))
+            (_.cover [/.cannot_apply]
+                     (|> (do //phase.monad
+                           [_ (|> (/.apply ..analysis (list term/1 term/0)
+                                           (-> input/0 input/1 output/0)
+                                           (//analysis.unit)
+                                           archive.empty
+                                           (' []))
+                                  (//type.expecting output/0))]
+                           (in false))
+                         (//module.with 0 module/0)
+                         (//phase#each product.right)
+                         (//phase.result state)
+                         (exception.otherwise (text.contains? (value@ exception.#label /.cannot_apply)))))
+            ))))