From 1649aab8e3dda2661ace62e17dec861af72a105e Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sat, 14 Jun 2014 19:29:56 -0700 Subject: [PATCH] Correctly instantiate poly dots during inference. This removes the need for the cache of type variables for instantiating dotted variables, because we instantiate the uses at once. Closes PR 14576. Closes PR 14577. Closes PR 14579. Closes PR 14580. original commit: fecaf5127dd51fd11eeb043887f336bfca71810e --- .../typed-racket/infer/infer-unit.rkt | 57 ++++++------------- .../unit-tests/typecheck-tests.rkt | 29 ++++++++++ 2 files changed, 47 insertions(+), 39 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt index dc7e07f6..6be11f09 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -170,37 +170,16 @@ [(_ seq) #'(app List->seq (? values seq))]))) -;; Maps dotted vars (combined with dotted types, to ensure global uniqueness) -;; to "fresh" symbols. -;; That way, we can share the same "fresh" variables between the elements of a -;; cset if they're talking about the same dotted variable. -;; This makes it possible to reduce the size of the csets, since we can detect -;; identical elements that would otherwise differ only by these fresh vars. -;; The domain of this map is pairs (var . dotted-type). -;; The range is this map is a list of symbols generated on demand, as we need -;; more dots. -(define dotted-var-store (make-hash)) -;; Take (generate as needed) n symbols that correspond to variable var used in -;; the context of type t. -(define (var-store-take var t n) - (let* ([key (cons var t)] - [res (hash-ref dotted-var-store key '())]) - (if (>= (length res) n) - ;; there are enough symbols already, take n - (take res n) - ;; we need to generate more - (let* ([new (build-list (- n (length res)) - (lambda (x) (gensym var)))] - [all (append res new)]) - (hash-set! dotted-var-store key all) - all)))) - -(define (generate-dbound-prefix v ty n) - (define vars (var-store-take v ty n)) +;; generate-dbound-prefix: Symbol Type/c Natural Symbol -> (Values (Listof Symbol) (Listof Type/c)) +;; Substitutes n fresh new variables, replaces dotted occurences of v in t with the variables (and +;; maybe new-end), and then for each variable substitutes it in for regular occurences of v. +(define (generate-dbound-prefix v ty n new-end) + (define vars (build-list n (lambda (x) (gensym v)))) + (define ty* (substitute-dots (map make-F vars) (and new-end (make-F new-end)) v ty)) (values vars (for/list ([var (in-list vars)]) - (substitute (make-F var) v ty)))) + (substitute (make-F var) v ty*)))) (define/cond-contract (cgen/filter V X Y s t) @@ -257,7 +236,7 @@ #f #:return-unless (<= (length ss) (length ts)) #f - (define-values (vars new-tys) (generate-dbound-prefix dbound dty (- (length ts) (length ss)))) + (define-values (vars new-tys) (generate-dbound-prefix dbound dty (- (length ts) (length ss)) #f)) (% move-vars-to-dmap (cgen/list V (append vars X) Y (append ss new-tys) ts) dbound vars)] ;; dotted above, nothing below [((seq ss (null-end)) @@ -266,7 +245,7 @@ #f #:return-unless (<= (length ts) (length ss)) #f - (define-values (vars new-tys) (generate-dbound-prefix dbound dty (- (length ss) (length ts)))) + (define-values (vars new-tys) (generate-dbound-prefix dbound dty (- (length ss) (length ts)) #f)) (% move-vars-to-dmap (cgen/list V (append vars X) Y ss (append ts new-tys)) dbound vars)] ;; same dotted bound @@ -305,10 +284,12 @@ #f #:return-unless (<= (length ts) (length ss)) #f - (define-values (vars new-tys) (generate-dbound-prefix dbound t-dty (- (length ss) (length ts)))) + (define new-bound (gensym dbound)) + (define-values (vars new-tys) (generate-dbound-prefix dbound t-dty (- (length ss) (length ts)) + new-bound)) (% move-vars+rest-to-dmap (% cset-meet - (cgen/list V (append vars X) Y ss (append ts new-tys)) + (cgen/list (cons new-bound V) (append vars X) (cons new-bound Y) ss (append ts new-tys)) (cgen V (cons dbound X) Y s-rest t-dty)) vars dbound #:exact #t)] @@ -316,11 +297,12 @@ (seq ts (uniform-end t-rest))) (cond [(memq dbound Y) + (define new-bound (gensym dbound)) (define-values (vars new-tys) - (generate-dbound-prefix dbound s-dty (max 0 (- (length ts) (length ss))))) + (generate-dbound-prefix dbound s-dty (max 0 (- (length ts) (length ss))) new-bound)) (% move-vars+rest-to-dmap (% cset-meet - (cgen/list V (append vars X) Y (append ss new-tys) (extend ss ts t-rest)) + (cgen/list (cons new-bound V) (append vars X) (cons new-bound Y) (append ss new-tys) (extend ss ts t-rest)) (cgen V (cons dbound X) Y s-dty t-rest)) vars dbound)] [else @@ -799,11 +781,8 @@ (define cs-short (cgen/list null X (list dotted-var) short-S T #:expected-cset expected-cset)) #:return-unless cs-short #f - (define new-vars (var-store-take dotted-var T-dotted (length rest-S))) - (define new-Ts (for/list ([v (in-list new-vars)]) - (substitute (make-F v) dotted-var - (substitute-dots (map make-F new-vars) - #f dotted-var T-dotted)))) + (define-values (new-vars new-Ts) + (generate-dbound-prefix dotted-var T-dotted (length rest-S) #f)) (define cs-dotted (cgen/list null (append new-vars X) (list dotted-var) rest-S new-Ts #:expected-cset expected-cset)) #:return-unless cs-dotted #f diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index c44f67fe..086adf8c 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -3037,6 +3037,35 @@ (t:-> Univ -String : (-FS (-and (-filter -String '(0 0)) (-not-filter (-val #f) '(0 0))) -bot) : (make-Path null '(0 0)))] + + ;; PR 14576 + [tc-e + (let: ([foo : (All (b ...) ((List (b ... b -> b) ... b) -> Void)) (lambda (x) (void))]) + (foo (list (λ: ([x : String] [y : Symbol]) x) (λ: ([x : String] [y : Symbol]) y)))) + -Void] + + ;; PR 14579 + [tc-e + (let: ([foo : (All (b ...) ((List (List b ... b) ... b) -> (List (List b ... b) ... b))) + (lambda (x) x)]) + (foo (list (list "string")))) + (-lst* (-lst* -String))] + + ;; PR 14577 + [tc-err + (let: ([foo : (All (b ...) ((List (List b ... b) ... b) -> (List (List b ... b) ... b))) + (lambda (x) x)]) + (foo (list (list)))) + #:ret (ret -Bottom)] + + ;; PR 14580 + [tc-err + (let: ([foo : (All (b ...) ((List (List b ... b) ... b) -> (List (List b ... b) ... b))) + (lambda (x) x)]) + (foo (list (list "string" 'symbol)))) + #:ret (ret (-lst* (-lst* -String))) + #:expected (ret (-lst* (-lst* -String)))] + ) (test-suite