Support path/object reasoning for promises

original commit: 5802b42f66706b6d7396aa1855f3d1d0b5f2ca17

collects/tests/typed-racket/succeed/promise.rkt

@@ -0,0 +1,14 @@
+#lang typed/racket
+
+(require typed/rackunit)
+
+;; Test path reasoning for promises
+
+(: foo : (Promise (U Integer String)) -> (U Number False))
+(define (foo del)
+  (if (integer? (force del))
+      (+ 1 (force del))
+      (string->number (force del))))
+
+(check-equal? (foo (delay 5)) 6)
+(check-equal? (foo (delay "5")) 5)

collects/typed-racket/base-env/base-env.rkt

@@ -2672,7 +2672,7 @@
 
 ;Section 9.3 (Delayed Evaluation)
 [promise? (make-pred-ty (-Promise Univ))]
-[force (-poly (a) (-> (-Promise a) a))]
+[force (-poly (a) (->acc (list (-Promise a)) a (list -force)))]
 [promise-forced? (-poly (a) (-> (-Promise a) B))]
 [promise-running? (-poly (a) (-> (-Promise a) B))]
 

collects/typed-racket/rep/object-rep.rkt

@@ -1,11 +1,17 @@
 #lang racket/base
 
+;; Representation of "objects" --- these describe the
+;; part of an environment that an expression accesses
+;;
+;; See "Logical Types for Untyped Languages" pg.3
+
 (require "rep-utils.rkt" "free-variance.rkt" "filter-rep.rkt" "../utils/utils.rkt" (contract-req))
 (provide object-equal?)
 
 (def-pathelem CarPE () [#:fold-rhs #:base])
 (def-pathelem CdrPE () [#:fold-rhs #:base])
 (def-pathelem SyntaxPE () [#:fold-rhs #:base])
+(def-pathelem ForcePE () [#:fold-rhs #:base])
 ;; t is always a Name (can't put that into the contract b/c of circularity)
 (def-pathelem StructPE ([t Type/c] [idx natural-number/c])
   [#:frees (λ (f) (f t))]

collects/typed-racket/typecheck/tc-envops.rkt

@@ -38,6 +38,12 @@
     [((Syntax: t) (NotTypeFilter: u (list rst ... (SyntaxPE:)) x))
      (make-Syntax (update t (-not-filter u x rst)))]
 
+    ;; promise op
+    [((Promise: t) (TypeFilter: u (list rst ... (ForcePE:)) x))
+     (make-Promise (update t (-filter u x rst)))]
+    [((Promise: t) (NotTypeFilter: u (list rst ... (ForcePE:)) x))
+     (make-Promise (update t (-not-filter u x rst)))]
+
     ;; struct ops
     [((Struct: nm par flds proc poly pred)
       (TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x))

collects/typed-racket/types/abbrev.rkt

@@ -284,6 +284,7 @@
 (define -car (make-CarPE))
 (define -cdr (make-CdrPE))
 (define -syntax-e (make-SyntaxPE))
+(define -force (make-ForcePE))
 
 
 ;; convenient syntax

collects/typed-racket/types/printer.rkt

@@ -83,6 +83,7 @@
   (match c
     [(CarPE:) (fp "car")]
     [(CdrPE:) (fp "cdr")]
+    [(ForcePE:) (fp "force")]
     [(StructPE: t i) (fp "(~a ~a)" t i)]
     [else (fp "(Unknown Path Element: ~a)" (struct->vector c))]))