- Updated the compiler's type-checking context to match it with lux/type/check.

7 files changed, 276 insertions, 200 deletions

diff --git a/luxc/src/lux/base.clj b/luxc/src/lux/base.clj
index 2fe9952ee..bdbffdf35 100644
--- a/luxc/src/lux/base.clj
+++ b/luxc/src/lux/base.clj
@@ -110,6 +110,12 @@
   ["counter"
    "mappings"])
 
+;; Type-Context
+(deftuple
+  ["ex-counter"
+   "var-counter"
+   "var-bindings"])
+
 ;; Env
 (deftuple
   ["name"
@@ -148,7 +154,7 @@
    "cursor"
    "modules"
    "scopes"
-   "type-vars"
+   "type-context"
    "expected"
    "seed"
    "scope-type-vars"
@@ -711,6 +717,14 @@
       ;; "lux;mappings"
       (|table)]))
 
+(def +init-type-context+
+  (T [;; ex-counter
+      0
+      ;; var-counter
+      0
+      ;; var-bindings
+      (|table)]))
+
 (defn env [name old-name]
   (T [;; "lux;name"
       ($Cons name old-name)
@@ -821,8 +835,8 @@
       (|table)
       ;; "lux;scopes"
       $Nil
-      ;; "lux;types"
-      +init-bindings+
+      ;; "lux;type-context"
+      +init-type-context+
       ;; "lux;expected"
       $None
       ;; "lux;seed"
diff --git a/luxc/src/lux/type.clj b/luxc/src/lux/type.clj
index 561d81795..f69542442 100644
--- a/luxc/src/lux/type.clj
+++ b/luxc/src/lux/type.clj
@@ -171,7 +171,7 @@
 
 (defn bound? [id]
   (fn [state]
-    (if-let [type (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
+    (if-let [type (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
       (|case type
         (&/$Some type*)
         (return* state true)
@@ -183,7 +183,7 @@
 
 (defn deref [id]
   (fn [state]
-    (if-let [type* (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
+    (if-let [type* (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
       (|case type*
         (&/$Some type)
         (return* state type)
@@ -205,7 +205,7 @@
 
 (defn set-var [id type]
   (fn [state]
-    (if-let [tvar (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
+    (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
       (|case tvar
         (&/$Some bound)
         (if (type= type bound)
@@ -214,56 +214,63 @@
            state))
         
         (&/$None)
-        (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/$Some type) %)
-                                                            ts))
+        (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id (&/$Some type) %)
+                                                               ts))
                             state)
                  nil))
-      ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) &/|length)))
+      ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length)))
        state))))
 
 (defn reset-var [id type]
   (fn [state]
-    (if-let [tvar (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
-      (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/$Some type) %)
-                                                          ts))
+    (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
+      (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id (&/$Some type) %)
+                                                             ts))
                           state)
                nil)
-      ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) &/|length)))
+      ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length)))
        state))))
 
 (defn unset-var [id]
   (fn [state]
-    (if-let [tvar (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
-      (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id &/$None %)
-                                                          ts))
+    (if-let [tvar (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) (&/|get id))]
+      (return* (&/update$ &/$type-context (fn [ts] (&/update$ &/$var-bindings #(&/|put id &/$None %)
+                                                             ts))
                           state)
                nil)
-      ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) &/|length)))
+      ((&/fail-with-loc (str "[Type Error] Unknown type-var: " id " | " (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings) &/|length)))
        state))))
 
 ;; [Exports]
 ;; Type vars
 (def reset-mappings
   (fn [state]
-    (return* (&/update$ &/$type-vars #(->> %
-                                           ;; (&/set$ &/$counter 0)
-                                           (&/set$ &/$mappings (&/|table)))
+    (return* (&/update$ &/$type-context #(->> %
+                                              ;; (&/set$ &/$var-counter 0)
+                                              (&/set$ &/$var-bindings (&/|table)))
                         state)
              nil)))
 
 (def create-var
   (fn [state]
-    (let [id (->> state (&/get$ &/$type-vars) (&/get$ &/$counter))]
-      (return* (&/update$ &/$type-vars #(->> %
-                                             (&/update$ &/$counter inc)
-                                             (&/update$ &/$mappings (fn [ms] (&/|put id &/$None ms))))
+    (let [id (->> state (&/get$ &/$type-context) (&/get$ &/$var-counter))]
+      (return* (&/update$ &/$type-context #(->> %
+                                                (&/update$ &/$var-counter inc)
+                                                (&/update$ &/$var-bindings (fn [ms] (&/|put id &/$None ms))))
                           state)
                id))))
 
 (def existential
   ;; (Lux Type)
-  (|do [seed &/gen-id]
-    (return (&/$ExT seed))))
+  (fn [compiler]
+    (return* (&/update$ &/$type-context
+                        (fn [context]
+                          (&/update$ &/$ex-counter inc context))
+                        compiler)
+             (->> compiler
+                  (&/get$ &/$type-context)
+                  (&/get$ &/$ex-counter)
+                  &/$ExT))))
 
 (declare clean*)
 (defn delete-var [id]
@@ -292,9 +299,9 @@
                                          (|do [?type** (clean* id ?type*)]
                                            (return (&/T [?id (&/$Some ?type**)]))))
                                        ))))
-                               (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings)))]
+                               (->> state (&/get$ &/$type-context) (&/get$ &/$var-bindings)))]
          (fn [state]
-           (return* (&/update$ &/$type-vars #(&/set$ &/$mappings (&/|remove id mappings*) %)
+           (return* (&/update$ &/$type-context #(&/set$ &/$var-bindings (&/|remove id mappings*) %)
                                state)
                     nil)))
        state))))
diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux
index 8be7f8d26..e1244d970 100644
--- a/stdlib/source/lux.lux
+++ b/stdlib/source/lux.lux
@@ -548,6 +548,26 @@
          (#Cons [["lux" "doc"] (#TextA "All the information contained within a Lux module.")]
                 default-def-meta-exported)))
 
+## (type: Type-Context
+##   {#ex-counter Nat
+##    #var-counter Nat
+##    #var-bindings (List [Nat (Maybe Type)])})
+(_lux_def Type-Context
+  (#NamedT ["lux" "Type-Context"]
+           (#ProdT ## ex-counter
+            Nat
+            (#ProdT ## var-counter
+             Nat
+             ## var-bindings
+             (#AppT List
+                    (#ProdT Nat
+                            (#AppT Maybe Type))))))
+  (#Cons [["lux" "tags"] (#ListA (#Cons (#TextA "ex-counter")
+                                        (#Cons (#TextA "var-counter")
+                                               (#Cons (#TextA "var-bindings")
+                                                      #Nil))))]
+         default-def-meta-exported))
+
 ## (type: Compiler-Mode
 ##   #Release
 ##   #Debug
@@ -592,7 +612,7 @@
 ##    #cursor          Cursor
 ##    #modules         (List [Text Module])
 ##    #scopes          (List Scope)
-##    #type-vars       (Bindings Nat (Maybe Type))
+##    #type-context    Type-Context
 ##    #expected        (Maybe Type)
 ##    #seed            Nat
 ##    #scope-type-vars (List Nat)
@@ -610,8 +630,8 @@
                                    Module))
                (#ProdT ## "lux;scopes"
                 (#AppT List Scope)
-                (#ProdT ## "lux;type-vars"
-                 (#AppT (#AppT Bindings Nat) (#AppT Maybe Type))
+                (#ProdT ## "lux;type-context"
+                 Type-Context
                  (#ProdT ## "lux;expected"
                   (#AppT Maybe Type)
                   (#ProdT ## "lux;seed"
@@ -625,7 +645,7 @@
                                                (#Cons (#TextA "cursor")
                                                       (#Cons (#TextA "modules")
                                                              (#Cons (#TextA "scopes")
-                                                                    (#Cons (#TextA "type-vars")
+                                                                    (#Cons (#TextA "type-context")
                                                                            (#Cons (#TextA "expected")
                                                                                   (#Cons (#TextA "seed")
                                                                                          (#Cons (#TextA "scope-type-vars")
@@ -1695,7 +1715,7 @@
   (-> Ident ($' Lux Ident))
   (let' [[module name] ident
          {#info info #source    source   #modules modules
-          #scopes scopes #type-vars types    #host    host
+          #scopes scopes #type-context types    #host    host
           #seed seed #expected  expected #cursor  cursor
           #scope-type-vars scope-type-vars} state]
         (_lux_case (get module modules)
@@ -1854,7 +1874,7 @@
   ($' Lux Text)
   (_lux_case state
     {#info info #source    source   #modules modules
-     #scopes scopes #type-vars types    #host    host
+     #scopes scopes #type-context types    #host    host
      #seed seed #expected  expected #cursor  cursor
      #scope-type-vars scope-type-vars}
     (_lux_case (reverse scopes)
@@ -2336,7 +2356,7 @@
           (function' [state]
                      (_lux_case state
                        {#info info #source source #modules modules
-                        #scopes   scopes   #type-vars   types   #host           host
+                        #scopes   scopes   #type-context   types   #host           host
                         #seed   seed #expected expected
                         #cursor cursor
                         #scope-type-vars scope-type-vars}
@@ -2591,12 +2611,12 @@
   (-> Text ($' Lux AST))
   (_lux_case state
     {#info info #source source #modules modules
-     #scopes   scopes   #type-vars   types   #host host
+     #scopes   scopes   #type-context   types   #host host
      #seed   seed #expected expected
      #cursor cursor
      #scope-type-vars scope-type-vars}
     (#Right {#info info #source source #modules modules
-             #scopes   scopes   #type-vars   types   #host host
+             #scopes   scopes   #type-context   types   #host host
              #seed   (n.+ +1 seed) #expected expected
              #cursor cursor
              #scope-type-vars scope-type-vars}
@@ -3462,7 +3482,7 @@
   (-> Text (Lux Module))
   (function [state]
     (let [{#info info #source    source   #modules modules
-           #scopes scopes #type-vars types    #host    host
+           #scopes scopes #type-context types    #host    host
            #seed seed #expected  expected #cursor  cursor
            #scope-type-vars scope-type-vars} state]
       (case (get name modules)
@@ -3525,7 +3545,7 @@
   (Lux Type)
   (function [state]
     (let [{#info info #source    source   #modules modules
-           #scopes scopes #type-vars types    #host    host
+           #scopes scopes #type-context types    #host    host
            #seed seed #expected  expected #cursor  cursor
            #scope-type-vars scope-type-vars} state]
       (case expected
@@ -4049,7 +4069,7 @@
   (-> Text (Lux (List Text)))
   (let [modules (case state
                   {#info info #source    source   #modules modules
-                   #scopes scopes #type-vars types    #host    host
+                   #scopes scopes #type-context types    #host    host
                    #seed seed #expected  expected #cursor  cursor
                    #scope-type-vars scope-type-vars}
                   modules)]
@@ -4104,7 +4124,7 @@
   (-> Text Compiler (Maybe Type))
   (case state
     {#info info #source    source   #modules modules
-     #scopes scopes #type-vars types    #host    host
+     #scopes scopes #type-context types    #host    host
      #seed seed #expected  expected #cursor  cursor
      #scope-type-vars scope-type-vars}
     (find (: (-> Scope (Maybe Type))
@@ -4126,7 +4146,7 @@
   (-> Ident Compiler (Maybe Type))
   (let [[v-prefix v-name] name
         {#info info #source    source   #modules modules
-         #scopes scopes #type-vars types    #host    host
+         #scopes scopes #type-context types    #host    host
          #seed seed #expected  expected #cursor  cursor
          #scope-type-vars scope-type-vars} state]
     (case (get v-prefix modules)
@@ -4145,7 +4165,7 @@
   (-> Ident (Lux [Type Void]))
   (let [[v-prefix v-name] name
         {#info info #source    source   #modules modules
-         #scopes scopes #type-vars types    #host    host
+         #scopes scopes #type-context types    #host    host
          #seed seed #expected  expected #cursor  cursor
          #scope-type-vars scope-type-vars} state]
     (case (get v-prefix modules)
@@ -5504,7 +5524,7 @@
   (Lux (List Nat))
   (case state
     {#info info #source    source   #modules modules
-     #scopes scopes #type-vars types    #host    host
+     #scopes scopes #type-context types    #host    host
      #seed seed #expected  expected #cursor  cursor
      #scope-type-vars scope-type-vars}
     (#Right state scope-type-vars)
diff --git a/stdlib/source/lux/macro.lux b/stdlib/source/lux/macro.lux
index 5a3d3829d..93920c67b 100644
--- a/stdlib/source/lux/macro.lux
+++ b/stdlib/source/lux/macro.lux
@@ -614,6 +614,11 @@
   (function [compiler]
     (#;Right [compiler compiler])))
 
+(def: #export type-context
+  (Lux Type-Context)
+  (function [compiler]
+    (#;Right [compiler (get@ #;type-context compiler)])))
+
 (do-template [<macro> <func> <desc>]
   [(macro: #export (<macro> tokens)
      {#;doc (doc "Performs a macro-expansion and logs the resulting ASTs."
diff --git a/stdlib/source/lux/math/simple.lux b/stdlib/source/lux/math/simple.lux
index 6a2f2f710..6e6e23592 100644
--- a/stdlib/source/lux/math/simple.lux
+++ b/stdlib/source/lux/math/simple.lux
@@ -11,9 +11,9 @@
        (type [check])))
 
 (def: (find-type-var id env)
-  (-> Nat (Bindings Nat (Maybe Type)) (Lux Type))
+  (-> Nat Type-Context (Lux Type))
   (case (list;find (|>. product;left (n.= id))
-                   (get@ #;mappings env))
+                   (get@ #;var-bindings env))
     (#;Some [_ (#;Some type)])
     (case type
       (#;VarT id')
@@ -36,7 +36,7 @@
      compiler macro;get-compiler]
     (case raw-type
       (#;VarT id)
-      (find-type-var id (get@ #;type-vars compiler))
+      (find-type-var id (get@ #;type-context compiler))
 
       _
       (wrap raw-type))))
diff --git a/stdlib/source/lux/type/auto.lux b/stdlib/source/lux/type/auto.lux
index 95e422b13..bb1ecc1c6 100644
--- a/stdlib/source/lux/type/auto.lux
+++ b/stdlib/source/lux/type/auto.lux
@@ -17,9 +17,9 @@
        ))
 
 (def: (find-type-var id env)
-  (-> Nat (Bindings Nat (Maybe Type)) (Lux Type))
+  (-> Nat Type-Context (Lux Type))
   (case (list;find (|>. product;left (n.= id))
-                   (get@ #;mappings env))
+                   (get@ #;var-bindings env))
     (#;Some [_ (#;Some type)])
     (case type
       (#;VarT id')
@@ -42,7 +42,7 @@
      compiler macro;get-compiler]
     (case raw-type
       (#;VarT id)
-      (find-type-var id (get@ #;type-vars compiler))
+      (find-type-var id (get@ #;type-context compiler))
 
       _
       (wrap raw-type))))
@@ -76,25 +76,25 @@
   (case member
     ["" simple-name]
     (macro;either (do Monad<Lux>
-                       [member (macro;normalize member)
-                        _ (macro;resolve-tag member)]
-                       (wrap member))
-                     (do Monad<Lux>
-                       [this-module-name macro;current-module-name
-                        imp-mods (macro;imported-modules this-module-name)
-                        tag-lists (mapM @ macro;tag-lists imp-mods)
-                        #let [tag-lists (|> tag-lists List/join (List/map product;left) List/join)
-                              candidates (list;filter (. (Text/= simple-name) product;right)
-                                                      tag-lists)]]
-                       (case candidates
-                         #;Nil
-                         (macro;fail (format "Unknown tag: " (%ident member)))
-                         
-                         (#;Cons winner #;Nil)
-                         (wrap winner)
-                         
-                         _
-                         (macro;fail (format "Too many candidate tags: " (%list %ident candidates))))))
+                    [member (macro;normalize member)
+                     _ (macro;resolve-tag member)]
+                    (wrap member))
+                  (do Monad<Lux>
+                    [this-module-name macro;current-module-name
+                     imp-mods (macro;imported-modules this-module-name)
+                     tag-lists (mapM @ macro;tag-lists imp-mods)
+                     #let [tag-lists (|> tag-lists List/join (List/map product;left) List/join)
+                           candidates (list;filter (. (Text/= simple-name) product;right)
+                                                   tag-lists)]]
+                    (case candidates
+                      #;Nil
+                      (macro;fail (format "Unknown tag: " (%ident member)))
+                      
+                      (#;Cons winner #;Nil)
+                      (wrap winner)
+                      
+                      _
+                      (macro;fail (format "Too many candidate tags: " (%list %ident candidates))))))
 
     _
     (:: Monad<Lux> wrap member)))
@@ -191,22 +191,13 @@
                          input-types)]
     (tc;check output-type member-type')))
 
-(def: compiler-type-context
-  (Lux tc;Context)
-  (function [compiler]
-    (let [type-vars (get@ #;type-vars compiler)
-          context (|> tc;fresh-context
-                      (set@ #tc;var-counter (get@ #;counter type-vars))
-                      (set@ #tc;bindings (dict;from-list number;Hash<Nat> (get@ #;mappings type-vars))))]
-      (#;Right [compiler context]))))
-
 (type: #rec Instance
   {#constructor Ident
    #dependencies (List Instance)})
 
 (def: (test-provision provision context dep alts)
-  (-> (-> Compiler tc;Context Type (Check Instance))
-      tc;Context Type (List [Ident Type])
+  (-> (-> Compiler Type-Context Type (Check Instance))
+      Type-Context Type (List [Ident Type])
       (Lux (List Instance)))
   (do Monad<Lux>
     [compiler macro;get-compiler]
@@ -233,12 +224,12 @@
       (wrap found))))
 
 (def: (provision compiler context dep)
-  (-> Compiler tc;Context Type (Check Instance))
+  (-> Compiler Type-Context Type (Check Instance))
   (case (macro;run compiler
-                      ($_ macro;either
-                          (do Monad<Lux> [alts local-env] (test-provision provision context dep alts))
-                          (do Monad<Lux> [alts local-structs] (test-provision provision context dep alts))
-                          (do Monad<Lux> [alts import-structs] (test-provision provision context dep alts))))
+                   ($_ macro;either
+                       (do Monad<Lux> [alts local-env] (test-provision provision context dep alts))
+                       (do Monad<Lux> [alts local-structs] (test-provision provision context dep alts))
+                       (do Monad<Lux> [alts import-structs] (test-provision provision context dep alts))))
     (#;Left error)
     (tc;fail error)
 
@@ -258,7 +249,7 @@
   (-> Type Nat (List Type) Type (List [Ident Type]) (Lux (List Instance)))
   (do Monad<Lux>
     [compiler macro;get-compiler
-     context compiler-type-context]
+     context macro;type-context]
     (case (|> alts
               (List/map (function [[alt-name alt-type]]
                           (case (tc;run context
@@ -357,10 +348,10 @@
 
         _
         (macro;fail (format "Too many options available: "
-                               (|> chosen-ones
-                                   (List/map (. %ident product;left))
-                                   (text;join-with ", "))
-                               " --- for type: " (%type sig-type)))))
+                            (|> chosen-ones
+                                (List/map (. %ident product;left))
+                                (text;join-with ", "))
+                            " --- for type: " (%type sig-type)))))
 
     (#;Right [args _])
     (do @
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index 4d93c9024..1fec0891a 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -7,28 +7,20 @@
                 monad)
        (data [text "Text/" Monoid<Text> Eq<Text>]
              text/format
-             [number]
              maybe
              [product]
-             (coll [list]
-                   [dict])
+             (coll [list])
              [error #- fail])
        [type "Type/" Eq<Type>]
        ))
 
-(type: #export Id Nat)
-
 (type: #export Fixed (List [[Type Type] Bool]))
 
-(type: #export Context
-  {#var-counter Id
-   #ex-counter Id
-   #bindings (dict;Dict Id (Maybe Type))
-   #fixed Fixed
-   })
-
 (type: #export (Check a)
-  (-> Context (Error [Context a])))
+  (-> Type-Context (Error [Type-Context a])))
+
+(type: #export Type-Vars
+  (List [Nat (Maybe Type)]))
 
 (struct: #export _ (Functor Check)
   (def: (map f fa)
@@ -85,9 +77,51 @@
 
 (open Monad<Check> "Check/")
 
+(def: (var::get id plist)
+  (-> Nat Type-Vars (Maybe (Maybe Type)))
+  (case plist
+    #;Nil
+    #;None
+
+    (#;Cons [var-id var-type]
+            plist')
+    (if (n.= id var-id)
+      (#;Some var-type)
+      (var::get id plist'))
+    ))
+
+(def: (var::put id value plist)
+  (-> Nat (Maybe Type) Type-Vars Type-Vars)
+  (case plist
+    #;Nil
+    (list [id value])
+
+    (#;Cons [var-id var-type]
+            plist')
+    (if (n.= id var-id)
+      (#;Cons [var-id value]
+              plist')
+      (#;Cons [var-id var-type]
+              (var::put id value plist')))
+    ))
+
+(def: (var::remove id plist)
+  (-> Nat Type-Vars Type-Vars)
+  (case plist
+    #;Nil
+    #;Nil
+
+    (#;Cons [var-id var-type]
+            plist')
+    (if (n.= id var-id)
+      plist'
+      (#;Cons [var-id var-type]
+              (var::remove id plist')))
+    ))
+
 ## [[Logic]]
 (def: #export (run context proc)
-  (All [a] (-> Context (Check a) (Error a)))
+  (All [a] (-> Type-Context (Check a) (Error a)))
   (case (proc context)
     (#;Left error)
     (#;Left error)
@@ -107,16 +141,16 @@
 
 (def: #export existential
   {#;doc "A producer of existential types."}
-  (Check [Id Type])
+  (Check [Nat Type])
   (function [context]
-    (let [id (get@ #ex-counter context)]
-      (#;Right [(update@ #ex-counter n.inc context)
+    (let [id (get@ #;ex-counter context)]
+      (#;Right [(update@ #;ex-counter n.inc context)
                 [id (#;ExT id)]]))))
 
 (def: #export (bound? id)
-  (-> Id (Check Bool))
+  (-> Nat (Check Bool))
   (function [context]
-    (case (|> context (get@ #bindings) (dict;get id))
+    (case (|> context (get@ #;var-bindings) (var::get id))
       (#;Some (#;Some _))
       (#;Right [context true])
 
@@ -127,9 +161,9 @@
       (#;Left (format "Unknown type-var: " (%n id))))))
 
 (def: #export (read-var id)
-  (-> Id (Check Type))
+  (-> Nat (Check Type))
   (function [context]
-    (case (|> context (get@ #bindings) (dict;get id))
+    (case (|> context (get@ #;var-bindings) (var::get id))
       (#;Some (#;Some type))
       (#;Right [context type])
 
@@ -140,43 +174,43 @@
       (#;Left (format "Unknown type-var: " (%n id))))))
 
 (def: #export (write-var id type)
-  (-> Id Type (Check Unit))
+  (-> Nat Type (Check Unit))
   (function [context]
-    (case (|> context (get@ #bindings) (dict;get id))
+    (case (|> context (get@ #;var-bindings) (var::get id))
       (#;Some (#;Some bound))
       (#;Left (format "Cannot rebind type-var: " (%n id) " | Current type: " (%type bound)))
       
       (#;Some #;None)
-      (#;Right [(update@ #bindings (dict;put id (#;Some type)) context)
+      (#;Right [(update@ #;var-bindings (var::put id (#;Some type)) context)
                 []])
 
       #;None
       (#;Left (format "Unknown type-var: " (%n id))))))
 
 (def: (rewrite-var id type)
-  (-> Id Type (Check Unit))
+  (-> Nat Type (Check Unit))
   (function [context]
-    (case (|> context (get@ #bindings) (dict;get id))
+    (case (|> context (get@ #;var-bindings) (var::get id))
       (#;Some _)
-      (#;Right [(update@ #bindings (dict;put id (#;Some type)) context)
+      (#;Right [(update@ #;var-bindings (var::put id (#;Some type)) context)
                 []])
       
       #;None
       (#;Left (format "Unknown type-var: " (%n id))))))
 
 (def: #export (clear-var id)
-  (-> Id (Check Unit))
+  (-> Nat (Check Unit))
   (function [context]
-    (case (|> context (get@ #bindings) (dict;get id))
+    (case (|> context (get@ #;var-bindings) (var::get id))
       (#;Some _)
-      (#;Right [(update@ #bindings (dict;put id #;None) context)
+      (#;Right [(update@ #;var-bindings (var::put id #;None) context)
                 []])
       
       #;None
       (#;Left (format "Unknown type-var: " (%n id))))))
 
 (def: #export (clean t-id type)
-  (-> Id Type (Check Type))
+  (-> Nat Type (Check Type))
   (case type
     (#;VarT id)
     (if (n.= t-id id)
@@ -237,33 +271,28 @@
     ))
 
 (def: #export create-var
-  (Check [Id Type])
+  (Check [Nat Type])
   (function [context]
-    (let [id (get@ #var-counter context)]
+    (let [id (get@ #;var-counter context)]
       (#;Right [(|> context
-                    (update@ #var-counter n.inc)
-                    (update@ #bindings (dict;put id #;None)))
+                    (update@ #;var-counter n.inc)
+                    (update@ #;var-bindings (var::put id #;None)))
                 [id (#;VarT id)]]))))
 
-(do-template [<get> <set> <tag> <type>]
-  [(def: <get>
-     (Check <type>)
-     (function [context]
-       (#;Right [context
-                 (get@ <tag> context)])))
-
-   (def: (<set> value)
-     (-> <type> (Check Unit))
-     (function [context]
-       (#;Right [(set@ <tag> value context)
-                 []])))]
-
-  [get-bindings  set-bindings  #bindings  (dict;Dict Id (Maybe Type))]
-  [get-fixed set-fixed #fixed Fixed]
-  )
+(def: get-bindings
+  (Check (List [Nat (Maybe Type)]))
+  (function [context]
+    (#;Right [context
+              (get@ #;var-bindings context)])))
+
+(def: (set-bindings value)
+  (-> (List [Nat (Maybe Type)]) (Check Unit))
+  (function [context]
+    (#;Right [(set@ #;var-bindings value context)
+              []])))
 
 (def: #export (delete-var id)
-  (-> Id (Check Unit))
+  (-> Nat (Check Unit))
   (do Monad<Check>
     [? (bound? id)
      _ (if ?
@@ -292,11 +321,11 @@
                                [b-type'' (clean id b-type')]
                                (wrap [b-id (#;Some b-type'')])))
                            )))
-                     (dict;entries bindings))]
-    (set-bindings (|> bindings' (dict;from-list number;Hash<Nat>) (dict;remove id)))))
+                     bindings)]
+    (set-bindings (var::remove id bindings'))))
 
 (def: #export (with-var k)
-  (All [a] (-> (-> [Id Type] (Check a)) (Check a)))
+  (All [a] (-> (-> [Nat Type] (Check a)) (Check a)))
   (do Monad<Check>
     [[id var] create-var
      output (k [id var])
@@ -304,11 +333,10 @@
     (wrap output)))
 
 (def: #export fresh-context
-  Context
-  {#var-counter +0
-   #ex-counter +0
-   #bindings (dict;new number;Hash<Nat>)
-   #fixed (list)
+  Type-Context
+  {#;var-counter +0
+   #;ex-counter +0
+   #;var-bindings (list)
    })
 
 (def: (attempt op)
@@ -327,12 +355,10 @@
     (#;Left message)))
 
 (def: (fail-check expected actual)
-  (-> Type Type (Check Unit))
+  (All [a] (-> Type Type (Check a)))
   (fail (format "Expected: " (%type expected) "\n\n"
                 "Actual:   " (%type actual))))
 
-(def: success (Check Unit) (Check/wrap []))
-
 (def: (either left right)
   (All [a] (-> (Check a) (Check a) (Check a)))
   (function [context]
@@ -355,158 +381,171 @@
   (-> [Type Type] Bool Fixed Fixed)
   (#;Cons [ea status] fixed))
 
-(def: #export (check expected actual)
+(def: #export (check' expected actual fixed)
   {#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
-  (-> Type Type (Check Unit))
+  (-> Type Type Fixed (Check Fixed))
   (if (is expected actual)
-    success
+    (Check/wrap fixed)
     (case [expected actual]
       [(#;VarT e-id) (#;VarT a-id)]
       (if (n.= e-id a-id)
-        success
+        (Check/wrap fixed)
         (do Monad<Check>
           [ebound (attempt (read-var e-id))
            abound (attempt (read-var a-id))]
           (case [ebound abound]
             [#;None #;None]
-            (write-var e-id actual)
+            (do @
+              [_ (write-var e-id actual)]
+              (wrap fixed))
             
             [(#;Some etype) #;None]
-            (check etype actual)
+            (check' etype actual fixed)
 
             [#;None (#;Some atype)]
-            (check expected atype)
+            (check' expected atype fixed)
 
             [(#;Some etype) (#;Some atype)]
-            (check etype atype))))
+            (check' etype atype fixed))))
       
       [(#;VarT id) _]
-      (either (write-var id actual)
+      (either (do Monad<Check>
+                [_ (write-var id actual)]
+                (wrap fixed))
               (do Monad<Check>
                 [bound (read-var id)]
-                (check bound actual)))
+                (check' bound actual fixed)))
       
       [_ (#;VarT id)]
-      (either (write-var id expected)
+      (either (do Monad<Check>
+                [_ (write-var id expected)]
+                (wrap fixed))
               (do Monad<Check>
                 [bound (read-var id)]
-                (check expected bound)))
+                (check' expected bound fixed)))
 
       [(#;AppT (#;ExT eid) eA) (#;AppT (#;ExT aid) aA)]
       (if (n.= eid aid)
-        (check eA aA)
+        (check' eA aA fixed)
         (fail-check expected actual))
 
       [(#;AppT (#;VarT id) A1) (#;AppT F2 A2)]
       (either (do Monad<Check>
                 [F1 (read-var id)]
-                (check (#;AppT F1 A1) actual))
+                (check' (#;AppT F1 A1) actual fixed))
               (do Monad<Check>
-                [_ (check (#;VarT id) F2)
+                [fixed (check' (#;VarT id) F2 fixed)
                  e' (apply-type! F2 A1)
                  a' (apply-type! F2 A2)]
-                (check e' a')))
+                (check' e' a' fixed)))
       
       [(#;AppT F1 A1) (#;AppT (#;VarT id) A2)]
       (either (do Monad<Check>
                 [F2 (read-var id)]
-                (check expected (#;AppT F2 A2)))
+                (check' expected (#;AppT F2 A2) fixed))
               (do Monad<Check>
-                [_ (check F1 (#;VarT id))
+                [fixed (check' F1 (#;VarT id) fixed)
                  e' (apply-type! F1 A1)
                  a' (apply-type! F1 A2)]
-                (check e' a')))
+                (check' e' a' fixed)))
 
       [(#;AppT F A) _]
-      (do Monad<Check>
-        [#let [fx-pair [expected actual]]
-         fixed get-fixed]
+      (let [fx-pair [expected actual]]
         (case (fx-get fx-pair fixed)
           (#;Some ?)
           (if ?
-            success
+            (Check/wrap fixed)
             (fail-check expected actual))
 
           #;None
           (do Monad<Check>
-            [expected' (apply-type! F A)
-             _ (set-fixed (fx-put fx-pair true fixed))]
-            (check expected' actual))))
+            [expected' (apply-type! F A)]
+            (check' expected' actual (fx-put fx-pair true fixed)))))
 
       [_ (#;AppT F A)]
       (do Monad<Check>
         [actual' (apply-type! F A)]
-        (check expected actual'))
+        (check' expected actual' fixed))
 
       [(#;UnivQ _) _]
       (do Monad<Check>
         [[ex-id ex] existential
          expected' (apply-type! expected ex)]
-        (check expected' actual))
+        (check' expected' actual fixed))
 
       [_ (#;UnivQ _)]
       (with-var
         (function [[var-id var]]
           (do Monad<Check>
             [actual' (apply-type! actual var)
-             =output (check expected actual')
+             fixed (check' expected actual' fixed)
              _ (clean var-id expected)]
-            success)))
+            (Check/wrap fixed))))
 
       [(#;ExQ e!env e!def) _]
       (with-var
         (function [[var-id var]]
           (do Monad<Check>
             [expected' (apply-type! expected var)
-             =output (check expected' actual)
+             fixed (check' expected' actual fixed)
              _ (clean var-id actual)]
-            success)))
+            (Check/wrap fixed))))
 
       [_ (#;ExQ a!env a!def)]
       (do Monad<Check>
         [[ex-id ex] existential
          actual' (apply-type! actual ex)]
-        (check expected actual'))
+        (check' expected actual' fixed))
 
       [(#;HostT e-name e-params) (#;HostT a-name a-params)]
-      (if (Text/= e-name a-name)
+      (if (and (Text/= e-name a-name)
+               (n.= (list;size e-params)
+                    (list;size a-params)))
         (do Monad<Check>
-          [_ (mapM Monad<Check>
-                   (function [[e a]] (check e a))
-                   (list;zip2 e-params a-params))]
-          success)
+          [fixed (foldM Monad<Check>
+                        (function [[e a] fixed] (check' e a fixed))
+                        fixed
+                        (list;zip2 e-params a-params))]
+          (Check/wrap fixed))
         (fail-check expected actual))
 
       (^template [<unit> <append>]
         [<unit> <unit>]
-        success
+        (Check/wrap fixed)
         
         [(<append> eL eR) (<append> aL aR)]
         (do Monad<Check>
-          [_ (check eL aL)]
-          (check eR aR)))
+          [fixed (check' eL aL fixed)]
+          (check' eR aR fixed)))
       ([#;VoidT #;SumT]
        [#;UnitT #;ProdT])
       
       [(#;FunctionT eI eO) (#;FunctionT aI aO)]
       (do Monad<Check>
-        [_ (check aI eI)]
-        (check eO aO))
+        [fixed (check' aI eI fixed)]
+        (check' eO aO fixed))
 
       [(#;ExT e!id) (#;ExT a!id)]
       (if (n.= e!id a!id)
-        success
+        (Check/wrap fixed)
         (fail-check expected actual))
 
       [(#;NamedT _ ?etype) _]
-      (check ?etype actual)
+      (check' ?etype actual fixed)
 
       [_ (#;NamedT _ ?atype)]
-      (check expected ?atype)
+      (check' expected ?atype fixed)
 
       _
       (fail-check expected actual))))
 
+(def: #export (check expected actual)
+  {#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
+  (-> Type Type (Check Unit))
+  (do Monad<Check>
+    [fixed (check' expected actual (list))]
+    (wrap [])))
+
 (def: #export (checks? expected actual)
   {#;doc "A simple type-checking function that just returns a yes/no answer."}
   (-> Type Type Bool)
@@ -518,6 +557,6 @@
     true))
 
 (def: #export get-context
-  (Check Context)
+  (Check Type-Context)
   (function [context]
     (#;Right [context context])))