- Fixed some type-checking errors.

2 files changed, 43 insertions, 32 deletions

diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux
index 424a3188f..1432308f8 100644
--- a/new-luxc/source/luxc/analyser/function.lux
+++ b/new-luxc/source/luxc/analyser/function.lux
@@ -19,10 +19,10 @@
   (-> &;Analyser Text Text Code (Meta Analysis))
   (do Monad<Meta>
     [functionT meta;expected-type]
-    (loop [expected functionT]
+    (loop [expectedT functionT]
       (&;with-stacked-errors
-        (function [_] (format "Functions require function types: " (type;to-text expected)))
-        (case expected
+        (function [_] (format "Functions require function types: " (type;to-text expectedT)))
+        (case expectedT
           (#;Named name unnamedT)
           (recur unnamedT)
 
@@ -38,22 +38,22 @@
           (do @
             [[var-id var] (&;with-type-env
                             tc;existential)]
-            (recur (maybe;assume (type;apply (list var) expected))))
+            (recur (maybe;assume (type;apply (list var) expectedT))))
 
           (#;ExQ _)
           (&common;with-var
             (function [[var-id var]]
-              (recur (maybe;assume (type;apply (list var) expected)))))
+              (recur (maybe;assume (type;apply (list var) expectedT)))))
           
           (#;Var id)
           (do @
             [? (&;with-type-env
-                 (tc;bound? id))]
+                 (tc;concrete? id))]
             (if ?
               (do @
-                [expected' (&;with-type-env
-                             (tc;read id))]
-                (recur expected'))
+                [expectedT' (&;with-type-env
+                              (tc;read id))]
+                (recur expectedT'))
               ## Inference
               (&common;with-var
                 (function [[input-id inputT]]
@@ -65,13 +65,13 @@
                          funT' (&;with-type-env
                                  (tc;clean output-id funT))
                          concrete-input? (&;with-type-env
-                                           (tc;bound? input-id))
+                                           (tc;concrete? input-id))
                          funT'' (if concrete-input?
                                   (&;with-type-env
                                     (tc;clean input-id funT'))
                                   (wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT'))))
                          _ (&;with-type-env
-                             (tc;check expected funT''))]
+                             (tc;check expectedT funT''))]
                         (wrap funA))
                       ))))))
 
@@ -80,7 +80,7 @@
               &;with-scope
               ## Functions have access not only to their argument, but
               ## also to themselves, through a local variable.
-              (&scope;with-local [func-name functionT])
+              (&scope;with-local [func-name expectedT])
               (&scope;with-local [arg-name inputT])
               (&;with-expected-type outputT)
               (analyse body))
diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux
index 920eb876c..0fa56b600 100644
--- a/stdlib/source/lux/meta/type/check.lux
+++ b/stdlib/source/lux/meta/type/check.lux
@@ -157,7 +157,7 @@
   (-> Var (Check Bool))
   (function [context]
     (case (|> context (get@ #;var-bindings) (var::get id))
-      (#;Some (#;Some _))
+      (#;Some (#;Some bound))
       (#e;Success [context true])
 
       (#;Some #;None)
@@ -166,6 +166,19 @@
       #;None
       (ex;throw Unknown-Type-Var (nat/encode id)))))
 
+(def: #export (concrete? id)
+  (-> Var (Check Bool))
+  (function [context]
+    (case (|> context (get@ #;var-bindings) (var::get id))
+      (#;Some (#;Some bound))
+      (#e;Success [context (case bound (#;Var _) false _ true)])
+
+      (#;Some #;None)
+      (#e;Success [context false])
+      
+      #;None
+      (ex;throw Unknown-Type-Var (nat/encode id)))))
+
 (def: #export (read id)
   (-> Var (Check Type))
   (function [context]
@@ -215,6 +228,13 @@
       #;None
       (ex;throw Unknown-Type-Var (nat/encode id)))))
 
+(def: #export (throw exception message)
+  (All [a] (-> ex;Exception Text (Check a)))
+  (function [context]
+    (ex;throw exception message)))
+
+(exception: #export Cannot-Clean-Unbound-Var)
+
 (def: #export (clean t-id type)
   (-> Var Type (Check Type))
   (case type
@@ -224,27 +244,15 @@
         [? (bound? id)]
         (if ?
           (read id)
-          (wrap type)))
+          (throw Cannot-Clean-Unbound-Var (type;to-text type))))
       (do Monad<Check>
-        [? (bound? id)]
+        [? (concrete? id)]
         (if ?
           (do Monad<Check>
             [=type (read id)
-             ==type (clean t-id =type)]
-            (case ==type
-              (#;Var =id)
-              (if (n.= t-id =id)
-                (do Monad<Check>
-                  [_ (clear id)]
-                  (wrap type))
-                (do Monad<Check>
-                  [_ (update ==type id)]
-                  (wrap type)))
-
-              _
-              (do Monad<Check>
-                [_ (update ==type id)]
-                (wrap type))))
+             ==type (clean t-id =type)
+             _ (update ==type id)]
+            (wrap type))
           (wrap type))))
 
     (#;Primitive name params)
@@ -355,7 +363,8 @@
 (def: #export (delete id)
   (-> Var (Check Unit))
   (do Monad<Check>
-    [?link (pre-link id)]
+    [_ (wrap [])
+     ?link (pre-link id)]
     (case ?link
       #;None
       (delete' id)
@@ -363,7 +372,9 @@
       (#;Some pre)
       (do @
         [post (read id)
-         _ (update post pre)]
+         _ (if (type/= (#;Var pre) post)
+             (clear pre)
+             (update post pre))]
         (delete' id)))))
 
 (def: #export (with k)