Substitute constraints after recursive call

Now it typechecks! Also fix type-equal? being too lenient

diff --git a/typecheck.scm b/typecheck.scm
index a767ed07fb1c2244819c0bcbbb2539ff9ecc12bf..219b010202a7f7a0127847e8372ea7e064a05efb 100644 (file)
--- a/typecheck.scm
+++ b/typecheck.scm
@@ -180,8 +180,9 @@
                 (let* [(func-type (env-lookup env (car x)))
                        (return-type (fresh-tvar))
                        (other-func-type `(abs ,func-type ,return-type))
-                       (cs (~ func-type other-func-type))]
-                  (list cs return-type))
+                       (cs (~ func-type other-func-type))
+                       (resolved-return-type (substitute cs return-type))]
+                  (list cs resolved-return-type))
 
                                        ; regular function
                 (let* ((arg-type-res (check env (cadr x)))
@@ -244,10 +245,16 @@
 
                                        ; TODO: what's the most appropriate substitution?
                                        ; should all constraints just be limited to a pair?
+                                       ; this is currently horrific and i don't know what im doing.
+                                       ; should probably use ast-find here or during consolidation
+                                       ; to detect substitutions more than one layer deep
+                                       ; e.g. (abs t1 int) ~ (abs bool int)
+                                       ; substituting these constraints with t1 should resolve t1 with bool
 (define (substitute cs t)
                                        ; gets the first concrete type
                                        ; otherwise returns the last type variable
 
+                                       ; removes t itself from cs, to prevent infinite recursion
   (define cs-without-t
     (map (lambda (c)
           (filter (lambda (x) (not (eqv? t x))) c))
@@ -324,7 +331,9 @@
              (lambda (acc c)
                (if (tvar? c) acc #f))]
             [test (lambda (acc c)
-                    (and acc (fold-left test-kind #t c)))])
+                    (and acc
+                         (fold-left test-kind #t c) ; check only tvar substitutions
+                         (<= (length c) 2)))])      ; check maximum 2 subs per equality group
          (fold-left test #t cs)))))
 
                                        ; input: a list of binds ((x . y) (y . 3))