From 16db5ecc78e7fb4467893f8792176f86a5c83638 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Tue, 6 Jan 2015 13:51:40 -0500 Subject: [PATCH] dont let-alias type vars, better overlap & restrict --- .../typed-racket/infer/restrict.rkt | 4 +- .../typed-racket/typecheck/tc-let-unit.rkt | 16 ++-- .../typed-racket/types/remove-intersect.rkt | 78 +++++++------------ .../unit-tests/typecheck-tests.rkt | 15 +++- 4 files changed, 53 insertions(+), 60 deletions(-) diff --git a/typed-racket-lib/typed-racket/infer/restrict.rkt b/typed-racket-lib/typed-racket/infer/restrict.rkt index 5318e8c8..64b0debe 100644 --- a/typed-racket-lib/typed-racket/infer/restrict.rkt +++ b/typed-racket-lib/typed-racket/infer/restrict.rkt @@ -51,9 +51,9 @@ ;; resolve resolvable types if we haven't already done so [((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2))) - (restrict* (resolve-once t1) t2 pref (set-add resolved (cons t1 t2)))] + (restrict* (resolve t1) t2 pref (set-add resolved (cons t1 t2)))] [(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2))) - (restrict* t1 (resolve-once t2) pref (set-add resolved (cons t1 t2)))] + (restrict* t1 (resolve t2) pref (set-add resolved (cons t1 t2)))] ;; we don't actually want this - want something that's a part of t1 [(_ _) #:when (subtype t2 t1) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt index a125db5e..0270b0da 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt @@ -6,7 +6,7 @@ (private type-annotation parse-type syntax-properties) (env lexical-env type-alias-helper mvar-env global-env scoped-tvar-env) - (rep filter-rep object-rep) + (rep filter-rep object-rep type-rep) syntax/free-vars (typecheck signatures tc-metafunctions tc-subst internal-forms tc-envops) (utils tarjan) @@ -52,7 +52,7 @@ (match e-r [(list (tc-result: e-ts (FilterSet: fs+ fs-) os) ...) (values e-ts - (map (λ (o n) (if (is-var-mutated? n) -empty-obj o)) os names) + (map (λ (o n t) (if (or (is-var-mutated? n) (F? t)) -empty-obj o)) os names e-ts) (apply append (for/list ([n (in-list names)] [t (in-list e-ts)] @@ -64,12 +64,12 @@ (list f+)] [(is-var-mutated? n) (list)] - ;; n is being bound to an expression w/ object o - ;; we don't need any new info, aliasing and the - ;; lexical environment will have the needed info - [(Path? o) (list)] - ;; n is being bound to an expression w/o an object - ;; so remember n in our propositions + ;; n is being bound to an expression w/ object o, no new info + ;; is required due to aliasing (note: we currently do not + ;; alias objects typed as type variables) + [(and (Path? o) (not (F? t))) (list)] + ;; n is being bound to an expression w/o an object (or whose + ;; type is a type variable) so create props about n [else (list (-or (-and (-not-filter (-val #f) n) f+) (-and (-filter (-val #f) n) f-)))]))))] [(list (tc-result: e-ts (NoFilter:) _) ...) diff --git a/typed-racket-lib/typed-racket/types/remove-intersect.rkt b/typed-racket-lib/typed-racket/types/remove-intersect.rkt index bdd8dba9..b8447630 100644 --- a/typed-racket-lib/typed-racket/types/remove-intersect.rkt +++ b/typed-racket-lib/typed-racket/types/remove-intersect.rkt @@ -32,69 +32,49 @@ #f] [else (match (list t1 t2) - [(list (Univ:) _) #t] - [(list _ (Univ:)) #t] - [(list (F: _) _) #t] - [(list _ (F: _)) #t] + [(list-no-order (Univ:) _) #t] + [(list-no-order (F: _) _) #t] [(list (Opaque: _) _) #t] - [(list _ (Opaque: _)) #t] + [(list-no-order _ (Opaque: _)) #t] [(list (Name/simple: n) (Name/simple: n*)) (or (free-identifier=? n n*) (overlap (resolve-once t1) (resolve-once t2)))] - [(list _ (? Name?)) - (overlap t1 (resolve-once t2))] - [(list (? Name?) _) - (overlap (resolve-once t1) t2)] - [(list (? Mu?) _) (overlap (unfold t1) t2)] - [(list _ (? Mu?)) (overlap t1 (unfold t2))] - - [(list (Refinement: t _) t2) (overlap t t2)] - [(list t1 (Refinement: t _)) (overlap t1 t)] - - [(list (Union: e) t) - (ormap (lambda (t*) (overlap t* t)) e)] - [(list t (Union: e)) - (ormap (lambda (t*) (overlap t t*)) e)] - [(or (list _ (? Poly?)) (list (? Poly?) _)) - #t] ;; these can have overlap, conservatively + [(list-no-order t (? Name? s)) + (overlap t (resolve-once s))] + [(list-no-order (? Mu? t) s) (overlap (unfold t) s)] + [(list-no-order (Refinement: t _) s) (overlap t s)] + [(list-no-order (Union: ts) s) + (ormap (lambda (t*) (overlap t* s)) ts)] + [(list-no-order (? Poly?) _) #t] ;; conservative [(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))] - [(list (Base: _ _ _ _) (Value: _)) (subtype t2 t1)] ;; conservative - [(list (Value: _) (Base: _ _ _ _)) (subtype t1 t2)] ;; conservative - [(list (Syntax: t) (Syntax: t*)) - (overlap t t*)] - [(or (list (Syntax: _) _) - (list _ (Syntax: _))) - #f] - [(list (Base: _ _ _ _) _) #f] - [(list _ (Base: _ _ _ _)) #f] - [(list (Value: (? pair? v)) (Pair: _ _)) #t] - [(list (Pair: _ _) (Value: (? pair? v))) #t] - [(list (Pair: a b) (Pair: a* b*)) - (and (overlap a a*) - (overlap b b*))] - ;; lots of things are sequences - [(list (Sequence: _) _) #t] - [(list _ (Sequence: _)) #t] - [(or (list (Pair: _ _) _) - (list _ (Pair: _ _))) - #f] + [(list-no-order (? Base? t) (? Value? s)) (subtype t s)] ;; conservative + [(list (Syntax: t) (Syntax: t*)) (overlap t t*)] + [(list-no-order (Syntax: _) _) #f] + [(list-no-order (Base: _ _ _ _) _) #f] + [(list-no-order (Value: (? pair?)) (Pair: _ _)) #t] + [(list (Pair: a b) (Pair: a* b*)) (and (overlap a a*) + (overlap b b*))] + ;; lots of things are sequences, but not values where sequence? produces #f + [(list-no-order (Sequence: _) (Value: v)) (sequence? v)] + [(list-no-order (Sequence: _) _) #t] + ;; Values where evt? produces #f cannot be Evt + [(list-no-order (Evt: _) (Value: v)) (evt? v)] + [(list-no-order (Pair: _ _) _) #f] [(list (Value: (? simple-datum? v1)) (Value: (? simple-datum? v2))) (equal? v1 v2)] - [(or (list (Value: (? simple-datum?)) - (or (? Struct?) (? StructTop?) (? Function?))) - (list (or (? Struct?) (? StructTop?) (? Function?)) - (Value: (? simple-datum?)))) + [(list-no-order (Value: (? simple-datum?)) + (or (? Struct?) (? StructTop?) (? Function?))) #f] [(list (Struct: n _ flds _ _ _) - (Struct: n* _ flds* _ _ _)) (=> nevermind) - (unless (free-identifier=? n n*) (nevermind)) + (Struct: n* _ flds* _ _ _)) + #:when (free-identifier=? n n*) (for/and ([f (in-list flds)] [f* (in-list flds*)]) (match* (f f*) [((fld: t _ _) (fld: t* _ _)) (overlap t t*)]))] [(list (Struct: n #f _ _ _ _) - (StructTop: (Struct: n* #f _ _ _ _))) (=> nevermind) - (unless (free-identifier=? n n*) (nevermind)) + (StructTop: (Struct: n* #f _ _ _ _))) + #:when (free-identifier=? n n*) #t] ;; n and n* must be different, so there's no overlap [(list (Struct: n #f flds _ _ _) diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt index 63eafd48..06d8aaf8 100644 --- a/typed-racket-test/unit-tests/typecheck-tests.rkt +++ b/typed-racket-test/unit-tests/typecheck-tests.rkt @@ -1957,7 +1957,7 @@ (Boolean -> #t)) (t:-> -Boolean (-val #t))] - [tc-e (sequence? 'foo) + [tc-e (sequence? (ann 'foo Any)) -Boolean] [tc-err (stop-before (inst empty-sequence Symbol) zero?)] [tc-e (stop-before (inst empty-sequence Integer) zero?) @@ -3402,6 +3402,19 @@ x* 42))))))] + ;; ensure let-aliasing doesn't cause problems w/ type variable types + [tc-e (let () + (: foo (All (A) (-> A (Tuple Number A)))) + (define foo + (λ (x) + (let ([x* x]) + (cond + [(number? x*) (list x* x)] + [(number? x) (list x x*)] + [else (list 42 x*)])))) + (void)) + -Void] + ;; tests looking up path-types into unions [tc-e (let () (: foo ((U (Pairof Number Number) (Pairof Number String)) -> Number))