From f9f2b9bab9651c75eb5c884276e8d8c6449ef16d Mon Sep 17 00:00:00 2001
From: Eduardo Julian
Date: Thu, 20 Oct 2016 21:05:26 -0400
Subject: - Added code for handling some corner cases in the type-checker.

---
 src/lux/type.clj | 29 ++++++++++++++++++++++-------
 1 file changed, 22 insertions(+), 7 deletions(-)

(limited to 'src')

diff --git a/src/lux/type.clj b/src/lux/type.clj
index 87c330691..774d6b4d8 100644
--- a/src/lux/type.clj
+++ b/src/lux/type.clj
@@ -11,7 +11,8 @@
             (lux [base :as & :refer [|do return* return fail fail* assert! |let |case]])
             [lux.type.host :as &&host]))
 
-(declare show-type)
+(declare show-type
+         type=)
 
 ;; [Utils]
 (defn |list? [xs]
@@ -196,7 +197,9 @@
     (if-let [tvar (->> state (&/get$ &/$type-vars) (&/get$ &/$mappings) (&/|get id))]
       (|case tvar
         (&/$Some bound)
-        (fail* (str "[Type Error] Can't rebind type var: " id " | Current type: " (show-type bound)))
+        (if (type= type bound)
+          (return* state nil)
+          (fail* (str "[Type Error] Can't re-bind type var: " id " | Current type: " (show-type bound))))
         
         (&/$None)
         (return* (&/update$ &/$type-vars (fn [ts] (&/update$ &/$mappings #(&/|put id (&/$Some type) %)
@@ -710,11 +713,23 @@
             (return* state* output)
 
             (&/$Left _)
-            ((|do [fixpoints* (check* class-loader fixpoints invariant?? (&/$VarT ?id) F2)
-                   e* (apply-type F2 A1)
-                   a* (apply-type F2 A2)]
-               (check* class-loader fixpoints* invariant?? e* a*))
-             state)))
+            (|case F2
+              (&/$UnivQ (&/$Cons _) _)
+              ((|do [actual* (apply-type F2 A2)]
+                 (check* class-loader fixpoints invariant?? expected actual*))
+               state)
+
+              (&/$ExT _)
+              ((|do [fixpoints* (check* class-loader fixpoints invariant?? (&/$VarT ?id) F2)]
+                 (check* class-loader fixpoints* invariant?? A1 A2))
+               state)
+
+              _
+              ((|do [fixpoints* (check* class-loader fixpoints invariant?? (&/$VarT ?id) F2)
+                     e* (apply-type F2 A1)
+                     a* (apply-type F2 A2)]
+                 (check* class-loader fixpoints* invariant?? e* a*))
+               state))))
         
         [(&/$AppT F1 A1) (&/$AppT (&/$VarT ?id) A2)]
         (fn [state]
-- 
cgit v1.2.3