From da30fb6f740b28a58ba901a1ae44600f99bc4eaf Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Mon, 19 Dec 2016 08:28:49 -0500 Subject: [PATCH] be less eager about bottom propogation Moving to eager propagating of bottom works for most cases, but in some cases flattening types such as (Pairof Bottom Any) to Bottom made things like type inference break for some cases (since (Listof Nothing) == Null, and (Listof A) did not structurally like up like it used to). Perhaps w/ a little more effort inference and any other potential issues could work better with propagating bottom, but for now we'll be slightly less aggressive about it. i.e. this fixes pfds, which commit 8e7f390 broke. --- .../typed-racket/infer/intersect.rkt | 19 ++- .../typed-racket/rep/type-rep.rkt | 109 ++++-------------- .../typed-racket/types/base-abbrev.rkt | 10 ++ .../typed-racket/types/update.rkt | 11 +- typed-racket-test/fail/issue-169-1.rkt | 2 +- typed-racket-test/fail/issue-169-2.rkt | 2 +- typed-racket-test/succeed/inf-nested-bot.rkt | 16 +++ 7 files changed, 62 insertions(+), 107 deletions(-) create mode 100644 typed-racket-test/succeed/inf-nested-bot.rkt diff --git a/typed-racket-lib/typed-racket/infer/intersect.rkt b/typed-racket-lib/typed-racket/infer/intersect.rkt index e6f4c3fa..f3be5875 100644 --- a/typed-racket-lib/typed-racket/infer/intersect.rkt +++ b/typed-racket-lib/typed-racket/infer/intersect.rkt @@ -51,15 +51,15 @@ ;; structural recursion on types [((Pair: a1 d1) (Pair: a2 d2)) - (-pair (rec a1 a2) (rec d1 d2))] + (rebuild -pair (rec a1 a2) (rec d1 d2))] ;; 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*)) - (-Syntax (rec t1* t2*))] + (rebuild -Syntax (rec t1* t2*))] [((Promise: t1*) (Promise: t2*)) - (-Promise (rec t1* t2*))] + (rebuild -Promise (rec t1* t2*))] [((Union: t1s) t2) (match t2 @@ -130,9 +130,6 @@ ;; and sometimes we want to make sure and _not_ add t2 to the result ;; we just want to keep the parts of t1 consistent with t2) (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))) ;; resolved is a set tracking previously seen restrict cases ;; (i.e. pairs of t1 t2) to prevent infinite unfolding. ;; subtyping performs a similar check for the same @@ -150,17 +147,17 @@ ;; structural recursion on types [((Pair: a1 d1) (Pair: a2 d2)) - (build-type -pair - (restrict a1 a2 resolved) - (restrict d1 d2 resolved))] + (rebuild -pair + (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* resolved))] + (rebuild -Syntax (restrict t1* t2* resolved))] [((Promise: t1*) (Promise: t2*)) - (build-type -Promise (restrict t1* t2* resolved))] + (rebuild -Promise (restrict t1* t2* resolved))] ;; unions [((Union: t1s) t2) diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt index 205e7719..eae71e50 100644 --- a/typed-racket-lib/typed-racket/rep/type-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt @@ -199,11 +199,7 @@ ;; left and right are Types (def-structural Pair ([left #:covariant] [right #:covariant]) - [#:mask mask:pair] - [#:custom-constructor - (if (or (Bottom? left) (Bottom? right)) - -Bottom - (make-Pair left right))]) + [#:mask mask:pair]) ;;---------------- ;; Mutable Pairs @@ -216,11 +212,7 @@ ;; *mutable* pairs - distinct from regular pairs ;; left and right are Types (def-structural MPair ([left #:invariant] [right #:invariant]) - [#:mask mask:mpair] - [#:custom-constructor - (if (or (Bottom? left) (Bottom? right)) - -Bottom - (make-MPair left right))]) + [#:mask mask:mpair]) ;;---------- ;; Vectors @@ -242,11 +234,7 @@ [#:singleton -BoxTop]) (def-structural Box ([elem #:invariant]) - [#:mask mask:box] - [#:custom-constructor - (if (Bottom? elem) - -Bottom - (make-Box elem))]) + [#:mask mask:box]) ;;---------- ;; Channel @@ -257,11 +245,7 @@ [#:singleton -ChannelTop]) (def-structural Channel ([elem #:invariant]) - [#:mask mask:channel] - [#:custom-constructor - (if (Bottom? elem) - -Bottom - (make-Channel elem))]) + [#:mask mask:channel]) ;;---------------- ;; Async-Channel @@ -272,11 +256,7 @@ [#:singleton -Async-ChannelTop]) (def-structural Async-Channel ([elem #:invariant]) - [#:mask mask:channel] - [#:custom-constructor - (if (Bottom? elem) - -Bottom - (make-Async-Channel elem))]) + [#:mask mask:channel]) ;;------------- ;; ThreadCell @@ -287,33 +267,21 @@ [#:singleton -ThreadCellTop]) (def-structural ThreadCell ([elem #:invariant]) - [#:mask mask:thread-cell] - [#:custom-constructor - (if (Bottom? elem) - -Bottom - (make-ThreadCell elem))]) + [#:mask mask:thread-cell]) ;;---------- ;; Promise ;;---------- (def-structural Promise ([elem #:covariant]) - [#:mask mask:promise] - [#:custom-constructor - (if (Bottom? elem) - -Bottom - (make-Promise elem))]) + [#:mask mask:promise]) ;;------------ ;; Ephemeron ;;------------ (def-structural Ephemeron ([elem #:covariant]) - [#:mask mask:ephemeron] - [#:custom-constructor - (if (Bottom? elem) - -Bottom - (make-Ephemeron elem))]) + [#:mask mask:ephemeron]) ;;----------- @@ -325,11 +293,7 @@ [#:singleton -Weak-BoxTop]) (def-structural Weak-Box ([elem #:invariant]) - [#:mask mask:other-box] - [#:custom-constructor - (if (Bottom? elem) - -Bottom - (make-Weak-Box elem))]) + [#:mask mask:other-box]) ;;--------------- @@ -337,11 +301,7 @@ ;;--------------- (def-structural CustodianBox ([elem #:covariant]) - [#:mask mask:other-box] - [#:custom-constructor - (if (Bottom? elem) - -Bottom - (make-CustodianBox elem))]) + [#:mask mask:other-box]) ;;------ ;; Set @@ -385,22 +345,14 @@ ;; t is the type of the result of syntax-e, not the result of syntax->datum (def-structural Syntax ([t #:covariant]) - [#:mask mask:syntax] - [#:custom-constructor - (if (Bottom? t) - -Bottom - (make-Syntax t))]) + [#:mask mask:syntax]) ;;--------- ;; Future ;;--------- (def-structural Future ([t #:covariant]) - [#:mask mask:future] - [#:custom-constructor - (if (Bottom? t) - -Bottom - (make-Future t))]) + [#:mask mask:future]) ;;--------------- @@ -417,11 +369,7 @@ ;; and the codomains of `handler` (def-structural Prompt-Tagof ([body #:invariant] [handler #:invariant]) - [#:mask mask:prompt-tag] - [#:custom-constructor - (if (or (Bottom? body) (Bottom? handler)) - -Bottom - (make-Prompt-Tagof body handler))]) + [#:mask mask:prompt-tag]) ;;-------------------------- ;; Continuation-Mark-Keyof @@ -460,11 +408,7 @@ [#:frees (f) (make-invariant (combine-frees (map f elems)))] [#:fmap (f) (make-HeterogeneousVector (map f elems))] [#:for-each (f) (for-each f elems)] - [#:mask mask:vector] - [#:custom-constructor - (if (ormap Bottom? elems) - -Bottom - (make-HeterogeneousVector elems))]) + [#:mask mask:vector]) ;; * * * * * * * @@ -617,14 +561,12 @@ ;; This should eventually be based on understanding of struct properties. [#:mask (mask-union mask:struct mask:procedure)] [#:custom-constructor - (cond - [(ormap (λ (fld) (Bottom? (fld-t fld))) flds) -Bottom] - [else (make-Struct (normalize-id name) - parent - flds - proc - poly? - (normalize-id pred-id))])]) + (make-Struct (normalize-id name) + parent + flds + proc + poly? + (normalize-id pred-id))]) ;; Represents prefab structs ;; key : prefab key encoding mutability, auto-fields, etc. @@ -634,11 +576,7 @@ [#:frees (f) (combine-frees (map f flds))] [#:fmap (f) (make-Prefab key (map f flds))] [#:for-each (f) (for-each f flds)] - [#:mask mask:prefab] - [#:custom-constructor - (cond - [(ormap Bottom? flds) -Bottom] - [else (make-Prefab key flds)])]) + [#:mask mask:prefab]) (def-type StructTypeTop () [#:mask mask:struct-type] @@ -772,10 +710,7 @@ [#:fmap (f) (make-Refinement (f parent) pred)] [#:for-each (f) (f parent)] [#:mask (λ (t) (mask (Refinement-parent t)))] - [#:custom-constructor - (if (Bottom? parent) - -Bottom - (make-Refinement parent (normalize-id pred)))]) + [#:custom-constructor (make-Refinement parent (normalize-id pred))]) ;; A Row used in type instantiation ;; For now, this should not appear in user code. It's used diff --git a/typed-racket-lib/typed-racket/types/base-abbrev.rkt b/typed-racket-lib/typed-racket/types/base-abbrev.rkt index c1cc701c..b6538aff 100644 --- a/typed-racket-lib/typed-racket/types/base-abbrev.rkt +++ b/typed-racket-lib/typed-racket/types/base-abbrev.rkt @@ -22,6 +22,16 @@ (rename-out [make-Listof -lst] [make-MListof -mlst])) +(define-syntax (rebuild stx) + (syntax-case stx () + [(_ mk args ...) + (with-syntax ([(t ...) (generate-temporaries #'(args ...))]) + (syntax/loc stx + (let ([t args] ...) + (if (or (Bottom? t) ...) + -Bottom + (mk t ...)))))])) + (define/decl -False (make-Value #f)) (define/decl -True (make-Value #t)) (define/decl -Boolean (Un -False -True)) diff --git a/typed-racket-lib/typed-racket/types/update.rkt b/typed-racket-lib/typed-racket/types/update.rkt index c6148416..2f6bde85 100644 --- a/typed-racket-lib/typed-racket/types/update.rkt +++ b/typed-racket-lib/typed-racket/types/update.rkt @@ -23,9 +23,6 @@ ;; in *syntactic order* (e.g. (car (cdr x)) -> '(car cdr)) (define/cond-contract (update t new-t pos? path-elems) (Type? Type? boolean? (listof PathElem?) . -> . Type?) - ;; build-type: build a type while propogating bottom - (define (build constructor . args) - (if (memf Bottom? args) -Bottom (apply constructor args))) ;; update's inner recursive loop ;; puts path in *accessed* order ;; (i.e. (car (cdr x)) --> (list cdr car)) @@ -38,15 +35,15 @@ (match* ((resolve t) path-elem) ;; pair ops [((Pair: t s) (CarPE:)) - (build -pair (update t rst) s)] + (rebuild -pair (update t rst) s)] [((Pair: t s) (CdrPE:)) - (build -pair t (update s rst))] + (rebuild -pair t (update s rst))] ;; syntax ops [((Syntax: t) (SyntaxPE:)) - (build -Syntax (update t rst))] + (rebuild -Syntax (update t rst))] ;; promise op [((Promise: t) (ForcePE:)) - (build -Promise (update t rst))] + (rebuild -Promise (update t rst))] ;; struct ops [((Struct: nm par flds proc poly pred) diff --git a/typed-racket-test/fail/issue-169-1.rkt b/typed-racket-test/fail/issue-169-1.rkt index 125886d9..5f6eaa7c 100644 --- a/typed-racket-test/fail/issue-169-1.rkt +++ b/typed-racket-test/fail/issue-169-1.rkt @@ -1,5 +1,5 @@ #; -(exn-pred #rx"expected: \\Null.*given: \\(Listof Pos\\*\\)") +(exn-pred #rx"expected: \\(Listof Nothing\\).*given: \\(Listof Pos\\*\\)") #lang typed/racket (define-type Pos Integer) (define-new-subtype Pos* (p Pos)) diff --git a/typed-racket-test/fail/issue-169-2.rkt b/typed-racket-test/fail/issue-169-2.rkt index e38bd54f..fbb99eb0 100644 --- a/typed-racket-test/fail/issue-169-2.rkt +++ b/typed-racket-test/fail/issue-169-2.rkt @@ -1,5 +1,5 @@ #; -(exn-pred #rx"expected: \\Null.*given: \\(Listof Pos\\*\\)") +(exn-pred #rx"expected: \\(Listof Nothing\\).*given: \\(Listof Pos\\*\\)") #lang typed/racket (define-type Pos Integer) (define-new-subtype Pos* (p Pos)) diff --git a/typed-racket-test/succeed/inf-nested-bot.rkt b/typed-racket-test/succeed/inf-nested-bot.rkt new file mode 100644 index 00000000..12465507 --- /dev/null +++ b/typed-racket-test/succeed/inf-nested-bot.rkt @@ -0,0 +1,16 @@ +#lang typed/racket + +(define-type (Promiseof A) (Boxof (U (→ (Listof A)) (Listof A)))) +(struct: (A) Queue ([fld : (Promiseof A)])) + +(define-syntax-rule (empty A) + ((inst Queue A) (box (lambda: () '())))) + +(: empty? : (All (A) ((Queue A) -> Boolean))) +(define (empty? q) + (null? (Queue-fld q))) + +;; make sure that inference works on nested 'Nothing' types +(empty? (empty Nothing)) + +