diff --git a/typed-racket-lib/typed-racket/types/current-seen.rkt b/typed-racket-lib/typed-racket/types/current-seen.rkt index 7ae3e321..93f5f445 100644 --- a/typed-racket-lib/typed-racket/types/current-seen.rkt +++ b/typed-racket-lib/typed-racket/types/current-seen.rkt @@ -7,7 +7,7 @@ ;;************************************************************ -;; Current Seen Continuation Mark +;; Current Seen Continuation Mark for Subtyping ;;************************************************************ ;; ;; Prevents infinite loops when subtyping calls outside diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt index 5525469e..5fb1c4d1 100644 --- a/typed-racket-lib/typed-racket/types/overlap.rkt +++ b/typed-racket-lib/typed-racket/types/overlap.rkt @@ -24,11 +24,13 @@ ;; let's not loop forever while checking overlap (define current-seen (make-parameter '())) (define (seen? t1 t2) - (let ([a (cons t1 t2)] - [b (cons t2 t1)]) - (for/or ([p (in-list (current-seen))]) - (or (equal? p a) - (equal? p b))))) + (for*/or ([p (in-list (current-seen))] + [a (in-value (car p))] + [d (in-value (cdr p))]) + (or (and (equal? t1 a) + (equal? t2 d)) + (and (equal? t1 d) + (equal? t2 a))))) (define-syntax-rule (with-updated-seen t1 t2 body ...) (parameterize ([current-seen (cons (cons t1 t2) (current-seen))]) body ...)) @@ -39,123 +41,122 @@ ;; have a non-empty intersection (define/cond-contract (overlap? t1 t2) (c:-> Type? Type? boolean?) - (cond - [(equal? t1 t2) #t] - [(disjoint-masks? (mask t1) (mask t2)) #f] - [(seen? t1 t2) #t] - [else - (with-updated-seen - t1 t2 - (match*/no-order - (t1 t2) - [((Univ:) _) #:no-order #t] - [((or (B: _) (F: _)) _) #:no-order #t] - [((Opaque: _) _) #:no-order #t] - [((Name/simple: n) (Name/simple: n*)) - (or (free-identifier=? n n*) - (overlap? (resolve-once t1) (resolve-once t2)))] - [(t (or (? Name? s) - (? App? s))) - #:no-order - (overlap? t (resolve-once s))] - [((? Mu? t1) t2) #:no-order (overlap? (unfold t1) t2)] - [((Refinement: t1 _) t2) #:no-order (overlap? t1 t2)] - [((BaseUnion: bbits1 nbits1) - (BaseUnion: bbits2 nbits2)) - (or (bbits-overlap? bbits1 bbits2) - (nbits-overlap? nbits1 nbits2))] - [((BaseUnion: bbits nbits) (Base-bits: num? bits)) - #:no-order - (if num? - (nbits-overlap? nbits bits) - (bbits-overlap? bbits bits))] - [((BaseUnion-bases: bases1) t2) - #:no-order - (for/or ([b1 (in-list bases1)]) (overlap? b1 t2))] - [((Union: (BaseUnion: bbits1 nbits1) _) - (Union: (BaseUnion: bbits2 nbits2) _)) - #:when (or (bbits-overlap? bbits1 bbits2) - (nbits-overlap? nbits1 nbits2)) - #t] - [((Union/set: base1 ts1 elems1) t2) - #:no-order - (or (hash-ref elems1 t2 #f) - (overlap? base1 t2) - (for/or ([t1 (in-list ts1)]) (overlap? t1 t2)))] - ;; we ignore the possible refining prop for simplicities sake - [((Intersection: ts _) s) - #:no-order - (for/and ([t (in-list ts)]) (overlap? t s))] - [((or (Poly-unsafe: _ t1) - (PolyDots-unsafe: _ t1)) - t2) - #:no-order - (overlap? t1 t2)] ;; conservative - [((? Base?) (? Base?)) (or (subtype t1 t2) (subtype t2 t1))] - [((? Base? t) (? Value? s)) #:no-order (subtype s t)] ;; conservative - [((Syntax: t) (Syntax: t*)) (overlap? t t*)] - [((Syntax: _) _) #:no-order #f] - [((? Base?) _) #:no-order #f] - [((Value: (? pair?)) (Pair: _ _)) #:no-order #t] - [((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 - [((Sequence: _) (Val-able: v)) #:no-order (sequence? v)] - ;; hash tables are two-valued sequences - [((Sequence: (or (list _) (list _ _ _ ...))) - (or (? Hashtable?) (? HashtableTop?))) - #:no-order - #f] - ;; these are single-valued sequences - [((Sequence: (list _ _ _ ...)) - (or (? Pair?) (? Vector?) (? VectorTop?))) - #:no-order - #f] - ;; be conservative about other kinds of sequences - [((Sequence: _) _) #:no-order #t] - ;; Values where evt? produces #f cannot be Evt - [((Evt: _) (Val-able: v)) #:no-order (evt? v)] - [((Pair: _ _) _) #:no-order #f] - [((Val-able: (? simple-datum? v1)) - (Val-able: (? simple-datum? v2))) - (equal? v1 v2)] - [((Val-able: (? simple-datum?)) - (or (? Struct?) (? StructTop?) (? Function?))) - #:no-order - #f] - [((Val-able: (not (? hash?))) - (or (? Hashtable?) (? HashtableTop?))) - #:no-order - #f] - [((Struct: n _ flds _ _ _) - (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*)]))] - [((Struct: n #f _ _ _ _) - (StructTop: (Struct: n* #f _ _ _ _))) - #:when (free-identifier=? n n*) - #t] - [((StructTop: (Struct: n* #f _ _ _ _)) - (Struct: n #f _ _ _ _)) - #:when (free-identifier=? n n*) - #t] - ;; n and n* must be different, so there's no overlap - [((Struct: n #f flds _ _ _) - (Struct: n* #f flds* _ _ _)) - #f] - [((Struct: n #f flds _ _ _) - (StructTop: (Struct: n* #f flds* _ _ _))) - #f] - [((StructTop: (Struct: n* #f flds* _ _ _)) - (Struct: n #f flds _ _ _)) - #f] - [((and t1 (Struct: _ _ _ _ _ _)) - (and t2 (Struct: _ _ _ _ _ _))) - (or (subtype t1 t2) (subtype t2 t1) - (parent-of? t1 t2) (parent-of? t2 t1))] - [(_ _) #t]))])) + (match*/no-order + (t1 t2) + [(_ _) #:when (equal? t1 t2) #t] + [(_ _) #:when (disjoint-masks? (mask t1) (mask t2)) #f] + [(_ _) #:when (seen? t1 t2) #t] + [((Univ:) _) #:no-order #t] + [((or (B: _) (F: _)) _) #:no-order #t] + [((Opaque: _) _) #:no-order #t] + [((Name/simple: n) (Name/simple: n*)) #:when (free-identifier=? n n*) #t] + [(t1 (or (? Name? t2) + (? App? t2))) + #:no-order + (with-updated-seen t1 t2 + (let ([t2 (resolve-once t2)]) + (or (not t2) (overlap? t1 t2))))] + [((? Mu? t1) t2) + #:no-order + (with-updated-seen t1 t2 + (overlap? (unfold t1) t2))] + [((Refinement: t1 _) t2) #:no-order (overlap? t1 t2)] + [((BaseUnion: bbits1 nbits1) + (BaseUnion: bbits2 nbits2)) + (or (bbits-overlap? bbits1 bbits2) + (nbits-overlap? nbits1 nbits2))] + [((BaseUnion: bbits nbits) (Base-bits: num? bits)) + #:no-order + (if num? + (nbits-overlap? nbits bits) + (bbits-overlap? bbits bits))] + [((BaseUnion-bases: bases1) t2) + #:no-order + (for/or ([b1 (in-list bases1)]) (overlap? b1 t2))] + [((Union: (BaseUnion: bbits1 nbits1) _) + (Union: (BaseUnion: bbits2 nbits2) _)) + #:when (or (bbits-overlap? bbits1 bbits2) + (nbits-overlap? nbits1 nbits2)) + #t] + [((Union/set: base1 ts1 elems1) t2) + #:no-order + (or (hash-ref elems1 t2 #f) + (overlap? base1 t2) + (for/or ([t1 (in-list ts1)]) (overlap? t1 t2)))] + ;; we ignore the possible refining prop for simplicities sake + [((Intersection: ts _) s) + #:no-order + (for/and ([t (in-list ts)]) (overlap? t s))] + [((or (Poly-unsafe: _ t1) + (PolyDots-unsafe: _ t1)) + t2) + #:no-order + (overlap? t1 t2)] ;; conservative + [((? Base?) (? Base?)) (or (subtype t1 t2) (subtype t2 t1))] + [((? Base? t) (? Value? s)) #:no-order (subtype s t)] ;; conservative + [((Syntax: t) (Syntax: t*)) (overlap? t t*)] + [((Syntax: _) _) #:no-order #f] + [((? Base?) _) #:no-order #f] + [((Value: (? pair?)) (Pair: _ _)) #:no-order #t] + [((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 + [((Sequence: _) (Val-able: v)) #:no-order (sequence? v)] + ;; hash tables are two-valued sequences + [((Sequence: (or (list _) (list _ _ _ ...))) + (or (? Hashtable?) (? HashtableTop?))) + #:no-order + #f] + ;; these are single-valued sequences + [((Sequence: (list _ _ _ ...)) + (or (? Pair?) (? Vector?) (? VectorTop?))) + #:no-order + #f] + ;; be conservative about other kinds of sequences + [((Sequence: _) _) #:no-order #t] + ;; Values where evt? produces #f cannot be Evt + [((Evt: _) (Val-able: v)) #:no-order (evt? v)] + [((Pair: _ _) _) #:no-order #f] + [((Val-able: (? simple-datum? v1)) + (Val-able: (? simple-datum? v2))) + (equal? v1 v2)] + [((Val-able: (? simple-datum?)) + (or (? Struct?) (? StructTop?) (? Function?))) + #:no-order + #f] + [((Val-able: (not (? hash?))) + (or (? Hashtable?) (? HashtableTop?))) + #:no-order + #f] + [((Struct: n _ flds _ _ _) + (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*)]))] + [((Struct: n #f _ _ _ _) + (StructTop: (Struct: n* #f _ _ _ _))) + #:when (free-identifier=? n n*) + #t] + [((StructTop: (Struct: n* #f _ _ _ _)) + (Struct: n #f _ _ _ _)) + #:when (free-identifier=? n n*) + #t] + ;; n and n* must be different, so there's no overlap + [((Struct: n #f flds _ _ _) + (Struct: n* #f flds* _ _ _)) + #f] + [((Struct: n #f flds _ _ _) + (StructTop: (Struct: n* #f flds* _ _ _))) + #f] + [((StructTop: (Struct: n* #f flds* _ _ _)) + (Struct: n #f flds _ _ _)) + #f] + [((and t1 (Struct: _ _ _ _ _ _)) + (and t2 (Struct: _ _ _ _ _ _))) + (or (subtype t1 t2) (subtype t2 t1) + (parent-of? t1 t2) (parent-of? t2 t1))] + [(_ _) #t])) ;; Type Type -> Boolean diff --git a/typed-racket-test/succeed/gh-issue-542.rkt b/typed-racket-test/succeed/gh-issue-542.rkt new file mode 100644 index 00000000..be13878e --- /dev/null +++ b/typed-racket-test/succeed/gh-issue-542.rkt @@ -0,0 +1,4 @@ +#lang typed/racket +(struct (A) S ([f : A])) + +(define-type T (∩ (S Nonnegative-Integer) (S Nonpositive-Integer)))