From e561cf1ba9b2986a22cb08250247e402ac2a5871 Mon Sep 17 00:00:00 2001 From: Luke Lau Date: Mon, 29 Jul 2019 13:55:23 +0100 Subject: [PATCH] Substitute constraints after recursive call Now it typechecks! Also fix type-equal? being too lenient --- typecheck.scm | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/typecheck.scm b/typecheck.scm index a767ed0..219b010 100644 --- 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)) -- 2.30.2