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 9da19828..9dff8d9f 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 @@ -82,13 +82,15 @@ (define (mover cset dbound vars f) (map/cset (lambda (cmap dmap) + (when (hash-has-key? (dmap-map dmap) dbound) + (int-err "Tried to move vars to dbound that already exists")) (% cons (hash-remove* cmap (cons dbound vars)) (dmap-meet (singleton-dmap dbound (f cmap)) - (make-dmap (hash-remove (dmap-map dmap) dbound))))) + dmap))) cset)) ;; dbound : index variable @@ -237,7 +239,10 @@ #:return-unless (<= (length ss) (length ts)) #f (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)] + (define-values (ts-front ts-back) (split-at ts (length ss))) + (% cset-meet + (cgen/list V X Y ss ts-front) + (% move-vars-to-dmap (cgen/list V (append vars X) Y new-tys ts-back) dbound vars))] ;; dotted above, nothing below [((seq ss (null-end)) (seq ts (dotted-end dty dbound))) @@ -246,7 +251,10 @@ #:return-unless (<= (length ts) (length ss)) #f (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)] + (define-values (ss-front ss-back) (split-at ss (length ts))) + (% cset-meet + (cgen/list V X Y ss-front ts) + (% move-vars-to-dmap (cgen/list V (append vars X) Y ss-back new-tys) dbound vars))] ;; same dotted bound [((seq ss (dotted-end s-dty dbound)) @@ -287,24 +295,33 @@ (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 (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)] + (define-values (ss-front ss-back) (split-at ss (length ts))) + (% cset-meet + (cgen/list V X Y ss-front ts) + (% move-vars+rest-to-dmap + (% cset-meet + (cgen/list (cons new-bound V) (append vars X) (cons new-bound Y) ss-back new-tys) + (cgen V (cons dbound X) Y s-rest t-dty)) + vars dbound #:exact #t))] [((seq ss (dotted-end s-dty dbound)) (seq ts (uniform-end t-rest))) (cond [(memq dbound Y) (define new-bound (gensym dbound)) + (define length-delta (- (length ts) (length ss))) (define-values (vars new-tys) - (generate-dbound-prefix dbound s-dty (max 0 (- (length ts) (length ss))) new-bound)) - (% move-vars+rest-to-dmap - (% cset-meet - (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)] + (generate-dbound-prefix dbound s-dty (max 0 length-delta) new-bound)) + (% cset-meet + (cgen/list V X Y ss (if (positive? length-delta) + (drop-right ts length-delta) + (extend ss ts t-rest))) + (% move-vars+rest-to-dmap + (% cset-meet + (cgen/list (cons new-bound V) (append vars X) (cons new-bound Y) + new-tys (take-right ts (max 0 length-delta))) + (cgen V (cons dbound X) Y s-dty t-rest)) + vars dbound))] [else (extend-tvars (list dbound) (cgen/seq (cons dbound V) X Y (seq ss (uniform-end s-dty)) t-seq))])])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt index 090aacd8..6a5b2a87 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt @@ -228,6 +228,23 @@ [infer-t (-> (-values (list -Bottom))) (-> (-values (list (-v b) (-v b)))) #:vars '(a)] [infer-t (-> (-values (list (-v a)))) (-> (-values (list (-v b) (-v b)))) #:vars '(a)] + [infer-t + (-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-lst (-v b)) 'b)) + (-lst* (-> Univ Univ)) + #:indices '(b) #:fail] + [infer-t + (-lst* (-> Univ Univ)) + (-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-lst (-v b)) 'b)) + #:indices '(b) #:fail] + [infer-t + (-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b)) + (-pair (-> -Symbol Univ) (-lst -String)) + #:indices '(b) #:fail] + [infer-t + (-pair (-> -Symbol Univ) (-lst -String)) + (-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b)) + #:indices '(b) #:fail] + ;; Currently Broken ;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b)) [i2-t (-v a) N ('a N)]