diff --git a/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt b/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt index 1376d537..e9cef977 100644 --- a/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt +++ b/typed-racket-lib/typed-racket/base-env/base-types-extra.rkt @@ -22,7 +22,8 @@ (define-other-types -> ->* case-> U Rec All Opaque Vector Parameterof List List* Class Object Unit Values AnyValues Instance Refinement - pred Struct Struct-Type Prefab Top Bot Distinction Sequenceof) + pred Struct Struct-Type Prefab Top Bot Distinction Sequenceof + ∩) (provide (rename-out [All ∀] [U Un] diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt index 0fa557fb..0c7ed99f 100644 --- a/typed-racket-lib/typed-racket/env/init-envs.rkt +++ b/typed-racket-lib/typed-racket/env/init-envs.rkt @@ -13,7 +13,7 @@ (rep type-rep object-rep prop-rep rep-utils free-variance) (for-syntax syntax/parse racket/base) (types abbrev union) - racket/dict racket/list racket/promise + racket/dict racket/list racket/set racket/promise mzlib/pconvert racket/match) (provide ;; convenience form for defining an initial environment @@ -84,6 +84,8 @@ `(->acc (list ,@(map sub dom)) ,(sub t) ,(sub pth))] [(Result: t (PropSet: (TrueProp:) (TrueProp:)) (Empty:)) `(-result ,(sub t))] [(Union: elems) (split-union elems)] + [(Intersection: elems) `(make-Intersection (set ,@(for/list ([elem (in-immutable-set elems)]) + (sub elem))))] [(Base: n cnt pred _) (int-err "Base type ~a not in predefined-type-table" n)] [(Name: stx args struct?) `(make-Name (quote-syntax ,stx) ,args ,struct?)] diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt index 4df1930e..aa2cc101 100644 --- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -19,7 +19,7 @@ "constraint-structs.rkt" "signatures.rkt" "fail.rkt" "promote-demote.rkt" - racket/match + racket/match racket/set mzlib/etc (contract-req) (for-syntax @@ -525,6 +525,19 @@ [((? Mu? s) t) (cg (unfold s) t)] [(s (? Mu? t)) (cg s (unfold t))] + ;; find *an* element of elems which can be made a subtype of T + [((Intersection: ts) T) + (cset-join + (for*/list ([t (in-immutable-set ts)] + [v (in-value (cg t T))] + #:when v) + v))] + + ;; constrain S to be below *each* element of elems, and then combine the constraints + [(S (Intersection: ts)) + (define cs (for/list/fail ([ts (in-immutable-set ts)]) (cg S ts))) + (and cs (cset-meet* (cons empty cs)))] + ;; constrain *each* element of es to be below T, and then combine the constraints [((Union: es) T) (define cs (for/list/fail ([e (in-list es)]) (cg e T))) diff --git a/typed-racket-lib/typed-racket/infer/restrict.rkt b/typed-racket-lib/typed-racket/infer/restrict.rkt index 64b0debe..c3e62452 100644 --- a/typed-racket-lib/typed-racket/infer/restrict.rkt +++ b/typed-racket-lib/typed-racket/infer/restrict.rkt @@ -12,8 +12,7 @@ ;; restrict t1 to be a subtype of t2 -;; if `pref' is 'new, use t2 when giving up, otherwise use t1 -(define (restrict t1 t2 [pref 'new]) +(define (restrict t1 t2) ;; build-type: build a type while propogating bottom (define (build-type constructor . args) (if (memf Bottom? args) -Bottom (apply constructor args))) @@ -21,7 +20,7 @@ ;; (i.e. pairs of t1 t2) to prevent infinite unfolding. ;; subtyping performs a similar check for the same ;; reason - (define (restrict* t1 t2 pref resolved) + (define (restrict* t1 t2 resolved) (match* (t1 t2) ;; already a subtype [(_ _) #:when (subtype t1 t2) @@ -34,35 +33,40 @@ ;; structural recursion on types [((Pair: a1 d1) (Pair: a2 d2)) (build-type -pair - (restrict* a1 a2 pref resolved) - (restrict* d1 d2 pref resolved))] + (restrict* a1 a2 resolved) + (restrict* d1 d2 resolved))] ;; FIXME: support structural updating for structs when structs are updated to ;; contain not only *if* they are polymorphic, but *which* fields are too ;;[((Struct: _ _ _ _ _ _) ;; (Struct: _ _ _ _ _ _))] [((Syntax: t1*) (Syntax: t2*)) - (build-type -Syntax (restrict* t1* t2* pref resolved))] + (build-type -Syntax (restrict* t1* t2* resolved))] [((Promise: t1*) (Promise: t2*)) - (build-type -Promise (restrict* t1* t2* pref resolved))] + (build-type -Promise (restrict* t1* t2* resolved))] ;; unions - [((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 pref resolved)) t1s))] - [(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* pref resolved)) t2s))] + [((Union: t1s) _) (apply Un (map (λ (t1*) (restrict* t1* t2 resolved)) t1s))] + [(_ (Union: t2s)) (apply Un (map (λ (t2*) (restrict* t1 t2* resolved)) t2s))] + + ;; intersections + [((Intersection: t1s) _) + (apply -unsafe-intersect (for/list ([t1 (in-immutable-set t1s)]) + (restrict* t1 t2 resolved)))] + [(_ (Intersection: t2s)) + (apply -unsafe-intersect (for/list ([t2 (in-immutable-set t2s)]) + (restrict* t1 t2 resolved)))] ;; resolve resolvable types if we haven't already done so [((? needs-resolving?) _) #:when (not (set-member? resolved (cons t1 t2))) - (restrict* (resolve t1) t2 pref (set-add resolved (cons t1 t2)))] + (restrict* (resolve t1) t2 (set-add resolved (cons t1 t2)))] [(_ (? needs-resolving?)) #:when (not (set-member? resolved (cons t1 t2))) - (restrict* t1 (resolve t2) pref (set-add resolved (cons t1 t2)))] + (restrict* t1 (resolve t2) (set-add resolved (cons t1 t2)))] ;; we don't actually want this - want something that's a part of t1 [(_ _) #:when (subtype t2 t1) t2] - - ;; there's no overlap, so the restriction is empty - [(_ _) #:when (not (overlap t1 t2)) - (Un)] - - ;; t2 and t1 have a complex relationship, so we punt - [(_ _) (if (eq? pref 'new) t2 t1)])) - (restrict* t1 t2 pref (set))) + + ;; t2 and t1 have a complex relationship, so we intersect + ;; (note: intersection checks for overlap) + [(_ _) (-unsafe-intersect t1 t2)])) + (restrict* t1 t2 (set))) diff --git a/typed-racket-lib/typed-racket/private/parse-type.rkt b/typed-racket-lib/typed-racket/private/parse-type.rkt index eaff072b..cef67ae4 100644 --- a/typed-racket-lib/typed-racket/private/parse-type.rkt +++ b/typed-racket-lib/typed-racket/private/parse-type.rkt @@ -2,11 +2,12 @@ ;; This module provides functions for parsing types written by the user -(require "../utils/utils.rkt" +(require (rename-in "../utils/utils.rkt" [infer infer-in]) (except-in (rep type-rep object-rep) make-arr) (rename-in (types abbrev union utils prop-ops resolve classes prefab signatures) [make-arr* make-arr]) + (only-in (infer-in infer) restrict) (utils tc-utils stxclass-util literal-syntax-class) syntax/stx (prefix-in c: (contract-req)) syntax/parse racket/sequence @@ -109,6 +110,7 @@ (define-literal-syntax-class #:for-label Bot) (define-literal-syntax-class #:for-label Distinction) (define-literal-syntax-class #:for-label Sequenceof) +(define-literal-syntax-class #:for-label ∩) ;; (Syntax -> Type) -> Syntax Any -> Syntax ;; See `parse-type/id`. This is a curried generalization. @@ -466,6 +468,10 @@ t*))))] [(:U^ ts ...) (apply Un (parse-types #'(ts ...)))] + [(:∩^ ts ...) + (for/fold ([ty Univ]) + ([t (in-list (parse-types #'(ts ...)))]) + (restrict ty t))] [(:quote^ t) (parse-quoted-type #'t)] [(:All^ . rest) diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt index 29938c64..e0d00490 100644 --- a/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -14,10 +14,10 @@ (private parse-type syntax-properties) racket/match racket/syntax racket/list racket/format - racket/dict + racket/dict racket/set syntax/flatten-begin (only-in (types abbrev) -Bottom -Boolean) - (static-contracts instantiate optimize structures combinators) + (static-contracts instantiate optimize structures combinators constraints) ;; TODO make this from contract-req (prefix-in c: racket/contract) (contract-req) @@ -211,6 +211,15 @@ ctc-cache sc-cache)))] [_ form])))) +;; get-max-contract-kind +;; static-contract -> (or/c 'flat 'chaperone 'impersonator) +;; recurse into a contract finding the max +;; kind (e.g. flat < chaperone < impersonator) +(define (get-max-contract-kind sc) + (define (get-restriction sc) + (sc->constraints sc get-restriction)) + (kind-max-max (contract-restrict-value (get-restriction sc)))) + ;; To avoid misspellings (define impersonator-sym 'impersonator) (define chaperone-sym 'chaperone) @@ -385,6 +394,21 @@ (if numeric-sc (apply or/sc numeric-sc (map t->sc non-numeric)) (apply or/sc (map t->sc elems)))] + [(Intersection: ts) + (define-values (chaperones/impersonators others) + (for/fold ([cs/is null] [others null]) + ([elem (in-immutable-set ts)]) + (define c (t->sc elem)) + (if (equal? flat-sym (get-max-contract-kind c)) + (values cs/is (cons c others)) + (values (cons c cs/is) others)))) + (cond + [(> (length chaperones/impersonators) 1) + (fail #:reason (~a "Intersection type contract contains" + " more than 1 non-flat contract: " + type))] + [else + (apply and/sc (append others chaperones/impersonators))])] [(and t (Function: arrs)) #:when (any->bool? arrs) ;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T) diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt index 68b2a23c..0b79e2e8 100644 --- a/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -8,7 +8,7 @@ ;; TODO use contract-req (require (utils tc-utils) "rep-utils.rkt" "object-rep.rkt" "prop-rep.rkt" "free-variance.rkt" - racket/match racket/list + racket/match racket/list racket/set racket/contract racket/lazy-require racket/promise @@ -19,6 +19,7 @@ PolyDots-names: PolyRow-names: PolyRow-fresh: Type-seq + -unsafe-intersect Mu-unsafe: Poly-unsafe: PolyDots-unsafe: Mu? Poly? PolyDots? PolyRow? @@ -53,8 +54,9 @@ ;; Ugly hack - should use units (lazy-require - ("../types/union.rkt" (Un)) - ("../types/resolve.rkt" (resolve-app))) + ("../types/union.rkt" (Un)) + ("../types/remove-intersect.rkt" (overlap)) + ("../types/resolve.rkt" (resolve-app))) (define name-table (make-weak-hasheq)) @@ -449,6 +451,55 @@ (define d* (remove-duplicates d)) (if (and (pair? d*) (null? (cdr d*))) (car d*) d*))]) + +;; Intersection +(def-type Intersection ([elems (and/c (set/c Type/c) + (λ (s) (>= (set-count s) 2)))]) + [#:intern (for/set ([e (in-immutable-set elems)]) + (Rep-seq e))] + [#:frees (λ (f) (combine-frees (for/list ([elem (in-immutable-set elems)]) + (f elem))))] + [#:fold-rhs (let ([elems (for/list ([elem (in-immutable-set elems)]) + (type-rec-id elem))]) + (apply -unsafe-intersect elems))] + [#:key (let () + (define d + (let loop ([ts (set->list elems)] [res null]) + (cond [(null? ts) res] + [else + (define k (Type-key (car ts))) + (cond [(not k) (list #f)] + [(pair? k) (loop (cdr ts) (append k res))] + [else (loop (cdr ts) (cons k res))])]))) + (define d* (remove-duplicates d)) + (if (and (pair? d*) (null? (cdr d*))) (car d*) d*))]) + +;; constructor for intersections +;; in general, intersections should be built +;; using the 'restrict' operator, which worries +;; about actual subtyping, etc... +(define (-unsafe-intersect . ts) + (let loop ([elems (set)] + [ts ts]) + (match ts + [(list) + (cond + [(set-empty? elems) (Univ)] + ;; size = 1 ? + [(= 1 (set-count elems)) (set-first elems)] + ;; size > 1, build an intersection + [else (*Intersection elems)])] + [(cons t ts) + (match t + [(? Bottom?) t] + [(Univ:) (loop elems ts)] + [(Intersection: ts*) (loop (set-union elems ts*) ts)] + [t (cond + [(for/or ([elem (in-immutable-set elems)]) (not (overlap elem t))) + (*Union (list))] + [else (loop (set-add elems t) ts)])])]))) + + (def-type Univ () [#:frees #f] [#:fold-rhs #:base]) ;; in : Type diff --git a/typed-racket-lib/typed-racket/static-contracts/constraints.rkt b/typed-racket-lib/typed-racket/static-contracts/constraints.rkt index 0d595068..03ceec0d 100644 --- a/typed-racket-lib/typed-racket/static-contracts/constraints.rkt +++ b/typed-racket-lib/typed-racket/static-contracts/constraints.rkt @@ -61,7 +61,8 @@ contract-restrict-recursive-values contract-restrict? - ) + contract-restrict-value + kind-max-max) (module structs racket/base (require racket/contract diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt index 24ddd46e..b4ad0099 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt @@ -366,18 +366,18 @@ (define (find-stx-type datum-stx [expected #f]) (match datum-stx [(? syntax? (app syntax-e stx-e)) - (match (and expected (resolve (restrict expected (-Syntax Univ) 'orig))) + (match (and expected (resolve (restrict expected (-Syntax Univ)))) [(Syntax: t) (-Syntax (find-stx-type stx-e t))] [_ (-Syntax (find-stx-type stx-e))])] [(or (? symbol?) (? null?) (? number?) (? extflonum?) (? boolean?) (? string?) (? char?) (? bytes?) (? regexp?) (? byte-regexp?) (? keyword?)) (tc-literal #`#,datum-stx expected)] [(cons car cdr) - (match (and expected (resolve (restrict expected (-pair Univ Univ) 'orig))) + (match (and expected (resolve (restrict expected (-pair Univ Univ)))) [(Pair: car-t cdr-t) (-pair (find-stx-type car car-t) (find-stx-type cdr cdr-t))] [_ (-pair (find-stx-type car) (find-stx-type cdr))])] [(vector xs ...) - (match (and expected (resolve (restrict expected -VectorTop 'orig))) + (match (and expected (resolve (restrict expected -VectorTop))) [(Vector: t) (make-Vector (check-below @@ -393,11 +393,11 @@ [_ (make-HeterogeneousVector (for/list ([x (in-list xs)]) (generalize (find-stx-type x #f))))])] [(box x) - (match (and expected (resolve (restrict expected -BoxTop 'orig))) + (match (and expected (resolve (restrict expected -BoxTop))) [(Box: t) (-box (check-below (find-stx-type x t) t))] [_ (-box (generalize (find-stx-type x)))])] [(? hash? h) - (match (and expected (resolve (restrict expected -HashTop 'orig))) + (match (and expected (resolve (restrict expected -HashTop))) [(Hashtable: kt vt) (define kts (hash-map h (lambda (x y) (find-stx-type x kt)))) (define vts (hash-map h (lambda (x y) (find-stx-type y vt)))) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt index 58142990..ae992a71 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt @@ -89,7 +89,7 @@ [i:regexp -Regexp] [() -Null] [(i . r) - (match (and expected (resolve (restrict expected (-pair Univ Univ) 'orig))) + (match (and expected (resolve (restrict expected (-pair Univ Univ)))) [(Pair: a-ty d-ty) (-pair (tc-literal #'i a-ty) @@ -97,7 +97,7 @@ [t (-pair (tc-literal #'i) (tc-literal #'r))])] [(~var i (3d vector?)) - (match (and expected (resolve (restrict expected -VectorTop 'orig))) + (match (and expected (resolve (restrict expected -VectorTop))) [(Vector: t) (make-Vector (check-below @@ -113,7 +113,7 @@ [_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))]) (generalize (tc-literal l #f))))])] [(~var i (3d hash?)) - (match (and expected (resolve (restrict expected -HashTop 'orig))) + (match (and expected (resolve (restrict expected -HashTop))) [(Hashtable: k v) (let* ([h (syntax-e #'i)] [ks (hash-map h (lambda (x y) (tc-literal x k)))] diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt index 96b264a6..8d2c9954 100644 --- a/typed-racket-lib/typed-racket/types/printer.rkt +++ b/typed-racket-lib/typed-racket/types/printer.rkt @@ -460,6 +460,8 @@ [(Union: elems) (define-values (covered remaining) (cover-union type ignored-names)) (cons 'U (append covered (map t->s remaining)))] + [(Intersection: elems) + (cons '∩ (for/list ([elem (in-immutable-set elems)]) (t->s elem)))] [(Pair: l r) `(Pairof ,(t->s l) ,(t->s r))] [(ListDots: dty dbound) `(List ,(t->s dty) ... ,dbound)] [(F: nm) nm] diff --git a/typed-racket-lib/typed-racket/types/remove-intersect.rkt b/typed-racket-lib/typed-racket/types/remove-intersect.rkt index 0920b9a4..22ca317f 100644 --- a/typed-racket-lib/typed-racket/types/remove-intersect.rkt +++ b/typed-racket-lib/typed-racket/types/remove-intersect.rkt @@ -3,7 +3,7 @@ (require "../utils/utils.rkt" (rep type-rep rep-utils) (types union subtype resolve utils) - racket/match) + racket/match racket/set) (provide (rename-out [*remove remove]) overlap) @@ -33,7 +33,7 @@ [else (match (list t1 t2) [(list-no-order (Univ:) _) #t] - [(list-no-order (F: _) _) #t] + [(list-no-order (or (B: _) (F: _)) _) #t] [(list-no-order (Opaque: _) _) #t] [(list (Name/simple: n) (Name/simple: n*)) (or (free-identifier=? n n*) @@ -44,6 +44,9 @@ [(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 (Intersection: ts) s) + (for/and ([t (in-immutable-set ts)]) + (overlap t s))] [(list-no-order (? Poly?) _) #t] ;; conservative [(list (Base: s1 _ _ _) (Base: s2 _ _ _)) (or (subtype t1 t2) (subtype t2 t1))] [(list-no-order (? Base? t) (? Value? s)) (subtype s t)] ;; conservative @@ -106,6 +109,9 @@ old] [(list (Union: l) rem) (apply Un (map (lambda (e) (*remove e rem)) l))] + [(list (Intersection: ts) rem) + (apply -unsafe-intersect + (for/list ([t (in-immutable-set ts)]) (*remove t rem)))] [(list (? Mu? old) t) (*remove (unfold old) t)] [(list (Poly: vs b) t) (make-Poly vs (*remove b rem))] [_ old]))) diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt index acaade54..e5f46015 100644 --- a/typed-racket-lib/typed-racket/types/subtype.rkt +++ b/typed-racket-lib/typed-racket/types/subtype.rkt @@ -1,6 +1,7 @@ #lang racket/base (require (except-in "../utils/utils.rkt" infer) - racket/match racket/function racket/lazy-require racket/list + racket/match racket/function racket/lazy-require + racket/list racket/set (prefix-in c: (contract-req)) (rep type-rep prop-rep object-rep rep-utils) (utils tc-utils early-return) @@ -272,6 +273,18 @@ ;; value types [((Value: v1) (Value: v2)) #:when (equal? v1 v2) A0] + [((Intersection: ss) t) + (and + (for/or ([s (in-immutable-set ss)]) + (subtype* A0 s t)) + A0)] + [(s (Intersection: ts)) + (and + (for/fold ([A A0]) + ([t (in-immutable-set ts)] + #:break (not A)) + (subtype* A s t)) + A0)] ;; values are subtypes of their "type" [((Value: v) (Base: _ _ pred _)) (if (pred v) A0 #f)] ;; tvars are equal if they are the same variable diff --git a/typed-racket-test/succeed/intersection1.rkt b/typed-racket-test/succeed/intersection1.rkt new file mode 100644 index 00000000..bc36beaa --- /dev/null +++ b/typed-racket-test/succeed/intersection1.rkt @@ -0,0 +1,19 @@ +#lang racket/base + + +(module a typed/racket + (provide num-id) + (: num-id (∀ (A) (-> (∩ Number A) (∩ Number A)))) + (define (num-id x) x)) + +(require 'a) + +(let () + (num-id 42) + (void)) + +(with-handlers ([exn:fail:contract? + (λ (ex) (void))]) + (num-id "42")) + + diff --git a/typed-racket-test/unit-tests/contract-tests.rkt b/typed-racket-test/unit-tests/contract-tests.rkt index 4c167b49..21a7cbe0 100644 --- a/typed-racket-test/unit-tests/contract-tests.rkt +++ b/typed-racket-test/unit-tests/contract-tests.rkt @@ -354,4 +354,10 @@ (class object% (super-new) (define/public (m) "m")) #:untyped) + ;; intersection types + (t (-unsafe-intersect (-seq -Symbol) (-pair -Symbol (-lst -Symbol)))) + (t/fail (-unsafe-intersect (-Number . -> . -Number) (-String . -> . -String)) + "more than 1 non-flat contract") + (t/fail (-unsafe-intersect (-box -Symbol) (-box Univ)) + "more than 1 non-flat contract") )) diff --git a/typed-racket-test/unit-tests/parse-type-tests.rkt b/typed-racket-test/unit-tests/parse-type-tests.rkt index 292e89f3..66d0d3ad 100644 --- a/typed-racket-test/unit-tests/parse-type-tests.rkt +++ b/typed-racket-test/unit-tests/parse-type-tests.rkt @@ -406,6 +406,14 @@ ;; GH issue #314 [FAIL ~> #:msg "unbound"] + + ;; intersections + [(∩) Univ] + [(∩ Any) Univ] + [(∩ String Symbol) -Bottom] + [(∩ (-> Number Number) (-> String String)) + (-unsafe-intersect (t:-> -String -String) + (t:-> -Number -Number))] )) ;; FIXME - add tests for parse-values-type, parse-tc-results diff --git a/typed-racket-test/unit-tests/remove-intersect-tests.rkt b/typed-racket-test/unit-tests/remove-intersect-tests.rkt index fe2da6ec..468075d7 100644 --- a/typed-racket-test/unit-tests/remove-intersect-tests.rkt +++ b/typed-racket-test/unit-tests/remove-intersect-tests.rkt @@ -2,6 +2,7 @@ (require "test-utils.rkt" (for-syntax racket/base) (r:infer infer) + (rep type-rep) (types abbrev numeric-tower subtype union remove-intersect) rackunit) (provide tests) @@ -43,7 +44,11 @@ [-Sexp -Listof (-lst -Sexp)] [(-val "one") -Fixnum (Un)] [(Un (-val "one") (-val "two")) (Un (-val "one") (-val 1)) (-val "one")] - )) + ;; intersection cases + [(-v a) -String (-unsafe-intersect (-v a) -String)] + [-String (-v a) (-unsafe-intersect (-v a) -String)] + [(-> -Number -Number) (-> -String -String) (-unsafe-intersect (-> -Number -Number) + (-> -String -String))])) (define-syntax (remo-tests stx) (syntax-case stx () diff --git a/typed-racket-test/unit-tests/subtype-tests.rkt b/typed-racket-test/unit-tests/subtype-tests.rkt index 4e635ca1..0671040e 100644 --- a/typed-racket-test/unit-tests/subtype-tests.rkt +++ b/typed-racket-test/unit-tests/subtype-tests.rkt @@ -50,6 +50,16 @@ [(Un (-val #f) (Un (-val 6) (-val 7))) (-mu x (Un -Number (Un -Boolean -Symbol)))] [(Un -Number (-val #f) (-mu x (Un -Number -Symbol (make-Listof x)))) (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))] + ;; intersections + [(-unsafe-intersect -Number) -Number] + [(-unsafe-intersect -Number -Symbol) -Number] + [(-unsafe-intersect -Boolean -Number) -Number] + [(-unsafe-intersect -Number -Number) -Number] + [FAIL -Number (-unsafe-intersect -Boolean -Number)] + [(-unsafe-intersect -Boolean -Number) (-unsafe-intersect -Boolean -Number)] + [(-unsafe-intersect -Sexp + (Un -Null (-pair -Sexp (-unsafe-intersect (make-Listof Univ) -Sexp)))) + (make-Listof Univ)] ;; sexps vs list*s of nums [(-mu x (Un -Number -Symbol (make-Listof x))) (-mu x (Un -Number -Symbol -Boolean (make-Listof x)))] [(-mu x (Un -Number (make-Listof x))) (-mu x (Un -Number -Symbol (make-Listof x)))]