- Type-vars no longer get deleted.

- Fixed some bugs.

6 files changed, 91 insertions, 163 deletions

diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux
index 738183410..9b41010d9 100644
--- a/stdlib/source/lux.lux
+++ b/stdlib/source/lux.lux
@@ -1208,8 +1208,8 @@
 (def:'' (length list)
   #;Nil
   (#UnivQ #Nil
-          (#Function ($' List (#Bound +1)) Int))
-  (fold (function'' [_ acc] ("lux int +" 1 acc)) 0 list))
+          (#Function ($' List (#Bound +1)) Nat))
+  (fold (function'' [_ acc] ("lux nat +" +1 acc)) +0 list))
 
 (macro:' #export (All tokens)
   (#Cons [(tag$ ["lux" "doc"])
@@ -1250,8 +1250,7 @@
                                                                       [false _]
                                                                       (replace-syntax (#Cons [self-name (make-bound ("lux nat *"
                                                                                                                      +2 ("lux nat -"
-                                                                                                                         ("lux int to-nat"
-                                                                                                                          (length names))
+                                                                                                                         (length names)
                                                                                                                          +1)))]
                                                                                              #Nil)
                                                                                       body')})
@@ -1302,7 +1301,7 @@
                                                                       [false _]
                                                                       (replace-syntax (#Cons [self-name (make-bound ("lux nat *"
                                                                                                                      +2 ("lux nat -"
-                                                                                                                         ("lux int to-nat" (length names))
+                                                                                                                         (length names)
                                                                                                                          +1)))]
                                                                                              #Nil)
                                                                                       body')})
@@ -1634,8 +1633,8 @@
   (#Named ["lux" "Monad"]
           (All [m]
             (& (All [a] (-> a ($' m a)))
-               (All [a b] (-> ($' m a)
-                              (-> a ($' m b))
+               (All [a b] (-> (-> a ($' m b))
+                              ($' m a)
                               ($' m b)))))))
 
 (def:''' Monad<Maybe>
@@ -1645,7 +1644,7 @@
    (function' [x] (#Some x))
    
    #bind
-   (function' [ma f]
+   (function' [f ma]
               ("lux case" ma
                {#None     #None
                 (#Some a) (f a)}))})
@@ -1659,7 +1658,7 @@
                          (#Right state x)))
    
    #bind
-   (function' [ma f]
+   (function' [f ma]
               (function' [state]
                          ("lux case" (ma state)
                           {(#Left msg)
@@ -1682,8 +1681,8 @@
 
                                            _
                                            (form$ (list g!bind
-                                                        value
-                                                        (form$ (list (text$ "lux function") (symbol$ ["" ""]) var body'))))}))))
+                                                        (form$ (list (text$ "lux function") (symbol$ ["" ""]) var body'))
+                                                        value))}))))
                        body
                        (reverse (as-pairs bindings)))]
           (return (list (form$ (list (text$ "lux case")
@@ -1770,7 +1769,7 @@
 (def:''' (text/compose x y)
   #Nil
   (-> Text Text Text)
-  ("lux text append" x y))
+  ("lux text concat" x y))
 
 (def:''' (ident/encode ident)
   #Nil
@@ -2197,7 +2196,7 @@
       (let' [apply ("lux check" (-> RepEnv ($' List Code))
                     (function' [env] (map (apply-template env) templates)))
              num-bindings (length bindings')]
-            (if (every? (function' [sample] ("lux int =" num-bindings sample))
+            (if (every? (function' [sample] ("lux nat =" num-bindings sample))
                         (map length data'))
               (|> data'
                   (join-map (. apply (make-env bindings')))
@@ -2211,12 +2210,12 @@
     (fail "Wrong syntax for do-template")}))
 
 (do-template [<type>
-              <=-proc> <lt-proc> <=-name> <lt-name> <lte-name> <gt-name> <gte-name>
+              <eq-proc> <lt-proc> <eq-name> <lt-name> <lte-name> <gt-name> <gte-name>
               <eq-doc> <<-doc> <<=-doc> <>-doc> <>=-doc>]
-  [(def:''' #export (<=-name> test subject)
+  [(def:''' #export (<eq-name> test subject)
      (list [(tag$ ["lux" "doc"]) (text$ <eq-doc>)])
      (-> <type> <type> Bool)
-     (<=-proc> subject test))
+     (<eq-proc> subject test))
    
    (def:''' #export (<lt-name> test subject)
      (list [(tag$ ["lux" "doc"]) (text$ <<-doc>)])
@@ -2228,7 +2227,7 @@
      (-> <type> <type> Bool)
      (if (<lt-proc> subject test)
        true
-       (<=-proc> subject test)))
+       (<eq-proc> subject test)))
    
    (def:''' #export (<gt-name> test subject)
      (list [(tag$ ["lux" "doc"]) (text$ <>-doc>)])
@@ -2240,7 +2239,7 @@
      (-> <type> <type> Bool)
      (if (<lt-proc> test subject)
        true
-       (<=-proc> subject test)))]
+       (<eq-proc> subject test)))]
 
   [ Nat "lux nat =" "lux nat <"   n.= n.< n.<= n.> n.>=
    "Nat(ural) equality." "Nat(ural) less-than." "Nat(ural) less-than-equal." "Nat(ural) greater-than." "Nat(ural) greater-than-equal."]
@@ -2343,9 +2342,9 @@
     (let' [loop ("lux check" (-> Nat Text Text)
                  (function' recur [input output]
                             (if ("lux nat =" input +0)
-                              ("lux text append" "+" output)
+                              ("lux text concat" "+" output)
                               (recur ("lux nat /" input +10)
-                                     ("lux text append" (digit-to-text ("lux nat %" input +10))
+                                     ("lux text concat" (digit-to-text ("lux nat %" input +10))
                                       output)))))]
           (loop value ""))}))
 
@@ -2367,9 +2366,9 @@
           (("lux check" (-> Int Text Text)
             (function' recur [input  output]
                        (if (i.= 0 input)
-                         ("lux text append" sign output)
+                         ("lux text concat" sign output)
                          (recur (i./ 10 input)
-                                ("lux text append" (|> input (i.% 10) ("lux coerce" Nat) digit-to-text)
+                                ("lux text concat" (|> input (i.% 10) ("lux coerce" Nat) digit-to-text)
                                  output)))))
            (|> value (i./ 10) int/abs)
            (|> value (i.% 10) int/abs ("lux coerce" Nat) digit-to-text)))))
@@ -2381,8 +2380,8 @@
 
 (def:''' (multiple? div n)
   #Nil
-  (-> Int Int Bool)
-  (i.= 0 (i.% div n)))
+  (-> Nat Nat Bool)
+  (|> n (n.% div) (n.= +0)))
 
 (def:''' #export (not x)
   (list [(tag$ ["lux" "doc"])
@@ -2982,7 +2981,7 @@
                    (op x y))")])
   (case tokens
     (^ (list [_ (#Tuple bindings)] body))
-    (if (multiple? 2 (length bindings))
+    (if (multiple? +2 (length bindings))
       (|> bindings as-pairs reverse
           (fold (: (-> [Code Code] Code Code)
                    (function' [lr body']
@@ -3436,15 +3435,15 @@
 
 (def: (nth idx xs)
   (All [a]
-    (-> Int (List a) (Maybe a)))
+    (-> Nat (List a) (Maybe a)))
   (case xs
     #Nil
     #None
 
     (#Cons x xs')
-    (if (i.= idx 0)
+    (if (n.= +0 idx)
       (#Some x)
-      (nth (i.- 1 idx) xs')
+      (nth (n.- +1 idx) xs')
       )))
 
 (def: (beta-reduce env type)
@@ -3479,7 +3478,7 @@
     (#Function (beta-reduce env ?input) (beta-reduce env ?output))
 
     (#Bound idx)
-    (case (nth ("lux nat to-int" idx) env)
+    (case (nth idx env)
       (#Some bound)
       bound
 
@@ -4073,7 +4072,7 @@
       parts
       (let [[ups parts'] (split-with (text/= "..") parts)
             num-ups (length ups)]
-        (if (i.= num-ups 0)
+        (if (n.= +0 num-ups)
           (return module)
           (case (nth num-ups (split-module-contexts current-module))
             #None
@@ -4433,7 +4432,7 @@
                 (n.odd? num) \"odd\"
                 ## else-branch
                 \"???\")"}
-  (if (i.= 0 (i.% 2 (length tokens)))
+  (if (n.= +0 (n.% +2 (length tokens)))
     (fail "cond requires an even number of arguments.")
     (case (reverse tokens)
       (^ (list& else branches'))
@@ -4971,7 +4970,7 @@
              (do Monad<Maybe>
                [bindings' (monad/map Monad<Maybe> get-name bindings)
                 data' (monad/map Monad<Maybe> tuple->list data)]
-               (if (every? (i.= (length bindings')) (map length data'))
+               (if (every? (n.= (length bindings')) (map length data'))
                  (let [apply (: (-> RepEnv (List Code))
                                 (function [env] (map (apply-template env) templates)))]
                    (|> data'
diff --git a/stdlib/source/lux/data/coll/list.lux b/stdlib/source/lux/data/coll/list.lux
index efdb727a5..4d4090835 100644
--- a/stdlib/source/lux/data/coll/list.lux
+++ b/stdlib/source/lux/data/coll/list.lux
@@ -368,7 +368,7 @@
                            (map (function [idx]
                                   (let [base (Nat/encode idx)]
                                     [(symbol$ base)
-                                     (symbol$ ("lux text append" base "'"))]))))
+                                     (symbol$ ("lux text concat" base "'"))]))))
             pattern (` [(~@ (map (function [[v vs]] (` (#;Cons (~ v) (~ vs))))
                                  vars+lists))])
             g!step (symbol$ "\tstep\t")
@@ -415,7 +415,7 @@
                            (map (function [idx]
                                   (let [base (Nat/encode idx)]
                                     [(symbol$ base)
-                                     (symbol$ ("lux text append" base "'"))]))))
+                                     (symbol$ ("lux text concat" base "'"))]))))
             pattern (` [(~@ (map (function [[v vs]] (` (#;Cons (~ v) (~ vs))))
                                  vars+lists))])
             g!step (symbol$ "\tstep\t")
diff --git a/stdlib/source/lux/data/number.lux b/stdlib/source/lux/data/number.lux
index 4dc0e4685..e9009102b 100644
--- a/stdlib/source/lux/data/number.lux
+++ b/stdlib/source/lux/data/number.lux
@@ -182,10 +182,10 @@
        (loop [input value
               output ""]
          (let [digit (maybe;assume (get-char <char-set> (n.% <base> input)))
-               output' ("lux text append" digit output)
+               output' ("lux text concat" digit output)
                input' (n./ <base> input)]
            (if (n.= +0 input')
-             ("lux text append" "+" output')
+             ("lux text concat" "+" output')
              (recur input' output')))))
 
      (def: (decode repr)
@@ -200,7 +200,7 @@
                    (let [digit (maybe;assume (get-char input idx))]
                      (case ("lux text index" <char-set> digit +0)
                        #;None
-                       (#E;Error ("lux text append" <error> repr))
+                       (#E;Error ("lux text concat" <error> repr))
 
                        (#;Some index)
                        (recur (n.inc idx)
@@ -208,8 +208,8 @@
                    (#E;Success output))))
 
              _
-             (#E;Error ("lux text append" <error> repr)))
-           (#E;Error ("lux text append" <error> repr))))))]
+             (#E;Error ("lux text concat" <error> repr)))
+           (#E;Error ("lux text concat" <error> repr))))))]
 
   [Binary@Codec<Text,Nat> +2  "01"               "Invalid binary syntax for Nat: "]
   [Octal@Codec<Text,Nat>  +8  "01234567"         "Invalid octal syntax for Nat: "]
@@ -230,10 +230,10 @@
                              (get-char <char-set>)
                              maybe;assume)]
              (if (i.= 0 input)
-               ("lux text append" sign output)
+               ("lux text concat" sign output)
                (let [digit (maybe;assume (get-char <char-set> (int-to-nat (i.% <base> input))))]
                  (recur (i./ <base> input)
-                        ("lux text append" digit output))))))))
+                        ("lux text concat" digit output))))))))
 
      (def: (decode repr)
        (let [input-size ("lux text size" repr)]
@@ -280,22 +280,22 @@
                             (if (n.= +0 zeroes-left)
                               output
                               (recur (n.dec zeroes-left)
-                                     ("lux text append" "0" output))))
-             padded-output ("lux text append" zero-padding raw-output)]
-         ("lux text append" "." padded-output)))
+                                     ("lux text concat" "0" output))))
+             padded-output ("lux text concat" zero-padding raw-output)]
+         ("lux text concat" "." padded-output)))
 
      (def: (decode repr)
        (let [repr-size ("lux text size" repr)]
          (if (n.>= +2 repr-size)
            (case ("lux text char" repr +0)
              (^multi (^ (#;Some (char ".")))
-                     [(:: <nat> decode ("lux text append" "+" (de-prefix repr)))
+                     [(:: <nat> decode ("lux text concat" "+" (de-prefix repr)))
                       (#;Some output)])
              (#E;Success (:! Deg output))
 
              _
-             (#E;Error ("lux text append" <error> repr)))
-           (#E;Error ("lux text append" <error> repr))))))]
+             (#E;Error ("lux text concat" <error> repr)))
+           (#E;Error ("lux text concat" <error> repr))))))]
 
   [Binary@Codec<Text,Deg> Binary@Codec<Text,Nat> +1 "Invalid binary syntax: "]
   [Octal@Codec<Text,Deg>  Octal@Codec<Text,Nat>  +3 "Invalid octal syntax: "]
@@ -313,13 +313,13 @@
                             (loop [dec-left decimal
                                    output ""]
                               (if (f.= 0.0 dec-left)
-                                ("lux text append" "." output)
+                                ("lux text concat" "." output)
                                 (let [shifted (f.* <base> dec-left)
                                       digit (|> shifted (f.% <base>) frac-to-int int-to-nat
                                                 (get-char <char-set>) maybe;assume)]
                                   (recur (f.% 1.0 shifted)
-                                         ("lux text append" output digit))))))]
-         ("lux text append" whole-part decimal-part)))
+                                         ("lux text concat" output digit))))))]
+         ("lux text concat" whole-part decimal-part)))
 
      (def: (decode repr)
        (case ("lux text index" repr "." +0)
@@ -340,7 +340,7 @@
                                  (recur (n.dec muls-left)
                                         (f.* <base> output))))
                    adjusted-decimal (|> decimal int-to-frac (f./ div-power))
-                   dec-deg (case (:: Hex@Codec<Text,Deg> decode ("lux text append" "." decimal-part))
+                   dec-deg (case (:: Hex@Codec<Text,Deg> decode ("lux text concat" "." decimal-part))
                              (#E;Success dec-deg)
                              dec-deg
 
@@ -350,10 +350,10 @@
                                 (f.* sign adjusted-decimal))))
 
              _
-             (#E;Error ("lux text append" <error> repr))))
+             (#E;Error ("lux text concat" <error> repr))))
 
          _
-         (#E;Error ("lux text append" <error> repr)))))]
+         (#E;Error ("lux text concat" <error> repr)))))]
 
   [Binary@Codec<Text,Frac> Binary@Codec<Text,Int> 2.0 "01" "Invalid binary syntax: "]
   )
@@ -457,7 +457,7 @@
     ""
 
     (#;Cons x xs')
-    ("lux text append" x (re-join-chunks xs'))))
+    ("lux text concat" x (re-join-chunks xs'))))
 
 (do-template [<from> <from-translator> <to> <to-translator> <base-bits>]
   [(def: (<from> on-left? input)
@@ -473,10 +473,10 @@
                               (if (n.= +0 zeroes-left)
                                 output
                                 (recur (n.dec zeroes-left)
-                                       ("lux text append" "0" output))))))
+                                       ("lux text concat" "0" output))))))
            padded-input (if on-left?
-                          ("lux text append" zero-padding input)
-                          ("lux text append" input zero-padding))]
+                          ("lux text concat" zero-padding input)
+                          ("lux text concat" input zero-padding))]
        (|> padded-input
            (segment-digits <base-bits>)
            (map <from-translator>)
@@ -504,9 +504,9 @@
                                        dot-idx))
              decimal-part (maybe;assume ("lux text clip" raw-bin (n.inc dot-idx) ("lux text size" raw-bin)))
              hex-output (|> (<from> false decimal-part)
-                            ("lux text append" ".")
-                            ("lux text append" (<from> true whole-part))
-                            ("lux text append" (if (f.= -1.0 sign) "-" "")))]
+                            ("lux text concat" ".")
+                            ("lux text concat" (<from> true whole-part))
+                            ("lux text concat" (if (f.= -1.0 sign) "-" "")))]
          hex-output))
 
      (def: (decode repr)
@@ -521,18 +521,18 @@
            (let [whole-part (maybe;assume ("lux text clip" repr (if (f.= -1.0 sign) +1 +0) split-index))
                  decimal-part (maybe;assume ("lux text clip" repr (n.inc split-index) ("lux text size" repr)))
                  as-binary (|> (<to> decimal-part)
-                               ("lux text append" ".")
-                               ("lux text append" (<to> whole-part))
-                               ("lux text append" (if (f.= -1.0 sign) "-" "")))]
+                               ("lux text concat" ".")
+                               ("lux text concat" (<to> whole-part))
+                               ("lux text concat" (if (f.= -1.0 sign) "-" "")))]
              (case (:: Binary@Codec<Text,Frac> decode as-binary)
                (#E;Error _)
-               (#E;Error ("lux text append" <error> repr))
+               (#E;Error ("lux text concat" <error> repr))
 
                output
                output))
 
            _
-           (#E;Error ("lux text append" <error> repr))))))]
+           (#E;Error ("lux text concat" <error> repr))))))]
 
   [Octal@Codec<Text,Frac> "Invalid octaladecimal syntax: " binary-to-octal octal-to-binary]
   [Hex@Codec<Text,Frac>   "Invalid hexadecimal syntax: "   binary-to-hex   hex-to-binary]
@@ -605,7 +605,7 @@
 
 (def: (prepend left right)
   (-> Text Text Text)
-  ("lux text append" left right))
+  ("lux text concat" left right))
 
 (def: (digits-times-5! idx output)
   (-> Nat Digits Digits)
@@ -643,7 +643,7 @@
           (recur (n.dec idx) true output)
           (recur (n.dec idx)
                  false
-                 ("lux text append"
+                 ("lux text concat"
                   (:: Codec<Text,Int> encode (:! Int digit))
                   output))))
       (if all-zeroes?
@@ -730,7 +730,7 @@
                        digits'))
               (recur (n.dec idx)
                      digits))
-            ("lux text append" "." (digits-to-text digits))
+            ("lux text concat" "." (digits-to-text digits))
             )))))
 
   (def: (decode input)
@@ -761,8 +761,8 @@
               (#E;Success (:! Deg output))))
 
           #;None
-          (#E;Error ("lux text append" "Wrong syntax for Deg: " input)))
-        (#E;Error ("lux text append" "Wrong syntax for Deg: " input))))
+          (#E;Error ("lux text concat" "Wrong syntax for Deg: " input)))
+        (#E;Error ("lux text concat" "Wrong syntax for Deg: " input))))
     ))
 
 (def: (log2 input)
diff --git a/stdlib/source/lux/data/text.lux b/stdlib/source/lux/data/text.lux
index e8eb20b43..812047e35 100644
--- a/stdlib/source/lux/data/text.lux
+++ b/stdlib/source/lux/data/text.lux
@@ -131,7 +131,7 @@
 (struct: #export _ (Monoid Text)
   (def: identity "")
   (def: (compose left right)
-    ("lux text append" left right)))
+    ("lux text concat" left right)))
 
 (open Monoid<Text> "text/")
 
diff --git a/stdlib/source/lux/meta/type/auto.lux b/stdlib/source/lux/meta/type/auto.lux
index 0162d7a04..a2013d3b1 100644
--- a/stdlib/source/lux/meta/type/auto.lux
+++ b/stdlib/source/lux/meta/type/auto.lux
@@ -156,7 +156,7 @@
 
     (#;UnivQ _)
     (do Monad<Check>
-      [[id var] tc;create]
+      [[id var] tc;var]
       (apply-function-type (maybe;assume (type;apply (list var) func))
                            arg))
 
@@ -173,7 +173,7 @@
   (case type
     (#;UnivQ _)
     (do Monad<Check>
-      [[id var] tc;create
+      [[id var] tc;var
        [ids final-output] (concrete-type (maybe;assume (type;apply (list var) type)))]
       (wrap [(#;Cons id ids)
              final-output]))
diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux
index b12470418..bd49a5588 100644
--- a/stdlib/source/lux/meta/type/check.lux
+++ b/stdlib/source/lux/meta/type/check.lux
@@ -230,36 +230,21 @@
       #;None
       (ex;throw Unknown-Type-Var (nat/encode id)))))
 
-(def: #export (clear id)
-  (-> Var (Check Unit))
-  (function [context]
-    (case (|> context (get@ #;var-bindings) (var::get id))
-      (#;Some _)
-      (#e;Success [(update@ #;var-bindings (var::put id #;None) context)
-                   []])
-      
-      #;None
-      (ex;throw Unknown-Type-Var (nat/encode id)))))
-
 (def: #export (clean t-id type)
   (-> Var Type (Check Type))
   (case type
     (#;Var id)
-    (if (n.= t-id id)
-      (do Monad<Check>
-        [? (bound? id)]
-        (if ?
+    (do Monad<Check>
+      [? (concrete? id)]
+      (if ?
+        (if (n.= t-id id)
           (read id)
-          (wrap type)))
-      (do Monad<Check>
-        [? (concrete? id)]
-        (if ?
           (do Monad<Check>
             [=type (read id)
              ==type (clean t-id =type)
              _ (update ==type id)]
-            (wrap type))
-          (wrap type))))
+            (wrap type)))
+        (wrap type)))
 
     (#;Primitive name params)
     (do Monad<Check>
@@ -290,7 +275,7 @@
     (:: Monad<Check> wrap type)
     ))
 
-(def: #export create
+(def: #export var
   (Check [Var Type])
   (function [context]
     (let [id (get@ #;var-counter context)]
@@ -311,29 +296,6 @@
     (#e;Success [(set@ #;var-bindings value context)
                  []])))
 
-(def: (pre-link id)
-  (-> Var (Check (Maybe Var)))
-  (function [context]
-    (loop [current id]
-      (case (|> context (get@ #;var-bindings) (var::get current))
-        (#;Some (#;Some type))
-        (case type
-          (#;Var post)
-          (if (n.= id post)
-            (#e;Success [context (#;Some current)])
-            (recur post))
-          
-          _
-          (if (n.= current id)
-            (#e;Success [context #;None])
-            (ex;throw Improper-Ring (nat/encode id))))
-
-        (#;Some #;None)
-        (#e;Success [context #;None])
-        
-        #;None
-        (ex;throw Unknown-Type-Var (nat/encode current))))))
-
 (type: #export Ring (Set Var))
 
 (def: empty-ring Ring (set;new number;Hash<Nat>))
@@ -360,37 +322,6 @@
         #;None
         (ex;throw Unknown-Type-Var (nat/encode current))))))
 
-(def: (delete' id)
-  (-> Var (Check Unit))
-  (function [context]
-    (#e;Success [(update@ #;var-bindings (var::remove id) context)
-                 []])))
-
-(def: #export (delete id)
-  (-> Var (Check Unit))
-  (do Monad<Check>
-    [_ (wrap [])
-     ?link (pre-link id)]
-    (case ?link
-      #;None
-      (delete' id)
-
-      (#;Some pre)
-      (do @
-        [post (read id)
-         _ (if (type/= (#;Var pre) post)
-             (clear pre)
-             (update post pre))]
-        (delete' id)))))
-
-(def: #export (with k)
-  (All [a] (-> (-> [Var Type] (Check a)) (Check a)))
-  (do Monad<Check>
-    [[id var] create
-     output (k [id var])
-     _ (delete id)]
-    (wrap output)))
-
 (def: #export fresh-context
   Type-Context
   {#;var-counter +0
@@ -653,22 +584,20 @@
           (check' expected' actual assumptions))
 
         [_ (#;UnivQ _)]
-        (with
-         (function [[var-id var]]
-           (do Monad<Check>
-             [actual' (apply-type! actual var)
-              assumptions (check' expected actual' assumptions)
-              _ (clean var-id expected)]
-             (check/wrap assumptions))))
+        (do Monad<Check>
+          [[var-id var] ;;var
+           actual' (apply-type! actual var)
+           assumptions (check' expected actual' assumptions)
+           _ (clean var-id expected)]
+          (check/wrap assumptions))
 
         [(#;ExQ e!env e!def) _]
-        (with
-         (function [[var-id var]]
-           (do Monad<Check>
-             [expected' (apply-type! expected var)
-              assumptions (check' expected' actual assumptions)
-              _ (clean var-id actual)]
-             (check/wrap assumptions))))
+        (do Monad<Check>
+          [[var-id var] ;;var
+           expected' (apply-type! expected var)
+           assumptions (check' expected' actual assumptions)
+           _ (clean var-id actual)]
+          (check/wrap assumptions))
 
         [_ (#;ExQ a!env a!def)]
         (do Monad<Check>