make cast sound

typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl

@@ -541,9 +541,18 @@ returned by @racket[e], protected by a contract ensuring that it has type
 
 @ex[(cast 3 Integer)
 (eval:error (cast 3 String))
-(cast (lambda: ([x : Any]) x) (String -> String))
+(cast (lambda ([x : Any]) x) (String -> String))
+((cast (lambda ([x : Any]) x) (String -> String)) "hello")
 ]
-}
+
+The value is actually protected with two contracts. The second contract checks
+the new type, but the first contract is put there to enforce the old type, to
+protect higher-order uses of the value.
+
+@ex[
+((cast (lambda ([s : String]) s) (Any -> Any)) "hello")
+(eval:error ((cast (lambda ([s : String]) s) (Any -> Any)) 5))
+]}
 
 @defform*[[(inst e t ...)
            (inst e t ... t ooo bound)]]{

typed-racket-lib/typed-racket/base-env/prims-contract.rkt

@@ -75,6 +75,7 @@
          (for-template "../utils/any-wrap.rkt")
          "../utils/tc-utils.rkt"
          "../private/syntax-properties.rkt"
+         "../private/cast-table.rkt"
          "../typecheck/internal-forms.rkt"
          ;; struct-extraction is actually used at both of these phases
          "../utils/struct-extraction.rkt"
@@ -250,9 +251,27 @@
 ;;  make-predicate
 ;;  cast
 
-;; Helper to construct syntax for contract definitions
+;; Helpers to construct syntax for contract definitions
+;; make-contract-def-rhs : Type-Stx Boolean Boolean -> Syntax
 (define (make-contract-def-rhs type flat? maker?)
-  (contract-def-property #'#f `#s(contract-def ,type ,flat? ,maker? untyped)))
+  (define contract-def `#s(contract-def ,type ,flat? ,maker? untyped))
+  (contract-def-property #'#f (λ () contract-def)))
+
+;; make-contract-def-rhs/from-typed : Id Boolean Boolean -> Syntax
+(define (make-contract-def-rhs/from-typed id flat? maker?)
+  (contract-def-property
+   #'#f
+   ;; This function should only be called after the type-checking pass has finished.
+   ;; By then `tc/#%expression` will have recognized the `casted-expr` property and
+   ;; will have added the casted expression's original type to the cast-table, so
+   ;; that `(cast-table-ref id)` can get that type here.
+   (λ ()
+     (define type-stx
+       (or (cast-table-ref id)
+           (int-err (string-append
+                     "contract-def-property: thunk called too early\n"
+                     "  This should only be called after the type-checking pass has finished."))))
+     `#s(contract-def ,type-stx ,flat? ,maker? typed))))
 
 
 (define (define-predicate stx)
@@ -289,17 +308,17 @@
 (define (cast stx)
   (syntax-parse stx
     [(_ v:expr ty:expr)
-     (define (apply-contract ctc-expr)
+     (define (apply-contract v ctc-expr pos neg)
        #`(#%expression
           #,(ignore-some/expr
-             #`(let-values (((val) #,(with-type* #'v #'Any)))
+             #`(let-values (((val) #,(with-type* v #'Any)))
                  #,(syntax-property
                     (quasisyntax/loc stx
                       (contract
                        #,ctc-expr
                        val
-                       'cast
-                       'typed-world
+                       '#,pos
+                       '#,neg
                        val
                        (quote-srcloc #,stx)))
                     'feature-profile:TR-dynamic-check #t))
@@ -308,8 +327,15 @@
      (cond [(not (unbox typed-context?)) ; no-check, don't check
             #'v]
            [else
-            (define ctc (syntax-local-lift-expression
-                         (make-contract-def-rhs #'ty #f #f)))
+            (define new-ty-ctc (syntax-local-lift-expression
+                                (make-contract-def-rhs #'ty #f #f)))
+            (define existing-ty-id new-ty-ctc)
+            (define existing-ty-ctc (syntax-local-lift-expression
+                                     (make-contract-def-rhs/from-typed existing-ty-id #f #f)))
+            (define (store-existing-type existing-type)
+              (cast-table-set! existing-ty-id existing-type))
+            (when (equal? (syntax-local-context) 'top-level)
+              (store-existing-type #'Any))
             (define (check-valid-type _)
               (define type (parse-type #'ty))
               (define vars (fv type))
@@ -319,7 +345,12 @@
                  "Type ~a could not be converted to a contract because it contains free variables."
                  type)))
             #`(#,(external-check-property #'#%expression check-valid-type)
-               #,(apply-contract ctc))])]))
+               #,(apply-contract
+                  (apply-contract
+                   #`(#,(casted-expr-property #'#%expression store-existing-type)
+                      v)
+                   existing-ty-ctc 'typed-world 'cast)
+                  new-ty-ctc 'cast 'typed-world))])]))
 
 
 

typed-racket-lib/typed-racket/private/cast-table.rkt

@@ -0,0 +1,25 @@
+#lang racket/base
+
+(provide cast-table-ref
+         cast-table-set!)
+
+(require syntax/id-table)
+
+;; A module that helps store information about the original types of casted
+;; expressions.
+;;
+;; Casts in Typed Racket must generate two contracts. One from typed to untyped,
+;; and another from untyped to typed. The contract from typed to untyped is
+;; generated based on the existing type of the expression, which must be stored
+;; in this table so that it can be looked up later in the contract-generation
+;; pass.
+
+(define cast-table (make-free-id-table))
+
+;; cast-table-set! : Id Type-Stx -> Void
+(define (cast-table-set! id type-stx)
+  (free-id-table-set! cast-table id type-stx))
+
+;; cast-table-ref : Id -> (U False Type-Stx)
+(define (cast-table-ref id)
+  (free-id-table-ref cast-table id #f))

typed-racket-lib/typed-racket/private/syntax-properties.rkt

@@ -50,9 +50,10 @@
   (ignore typechecker:ignore #:mark)
   (ignore-some typechecker:ignore-some #:mark)
   (ignore-some-expr typechecker:ignore-some)
-  (contract-def typechecker:contract-def)
+  (contract-def typechecker:contract-def) ; -> Contract-Def (struct in type-contract.rkt)
   (contract-def/provide typechecker:contract-def/provide)
   (external-check typechecker:external-check)
+  (casted-expr typechecker:casted-expr) ; Type -> Void, takes the original type of the casted expr
   (with-type typechecker:with-type #:mark)
   (type-ascription type-ascription)
   (type-inst type-inst)

typed-racket-lib/typed-racket/private/type-contract.rkt

@@ -39,14 +39,26 @@
 ;; submod for testing
 (module* test-exports #f (provide type->contract))
 
+;; has-contrat-def-property? : Syntax -> Boolean
+(define (has-contract-def-property? stx)
+  (syntax-parse stx
+    #:literal-sets (kernel-literals)
+    [(define-values (_) e)
+     (and (contract-def-property #'e)
+          #t)]
+    [_ #f]))
+
 (struct contract-def (type flat? maker? typed-side) #:prefab)
 
+;; get-contract-def-property : Syntax -> (U False Contract-Def)
 ;; Checks if the given syntax needs to be fixed up for contract generation
 ;; and if yes it returns the information stored in the property
 (define (get-contract-def-property stx)
   (syntax-parse stx
     #:literal-sets (kernel-literals)
-    [(define-values (_) e) (contract-def-property #'e)]
+    [(define-values (_) e)
+     (and (contract-def-property #'e)
+          ((contract-def-property #'e)))]
     [_ #f]))
 
 ;; type->contract-fail : Syntax Type #:ctc-str String
@@ -185,7 +197,7 @@
   (define sc-cache (make-hash))
   (with-new-name-tables
    (for/list ((e (in-list forms)))
-     (if (not (get-contract-def-property e))
+     (if (not (has-contract-def-property? e))
          e
          (begin (set-box! include-extra-requires? #t)
                 (generate-contract-def e ctc-cache sc-cache))))))

typed-racket-lib/typed-racket/private/with-types.rkt

@@ -154,10 +154,11 @@
 (define (type-stxs->ids+defs type-stxs typed-side)
   (for/lists (_1 _2) ([t (in-list type-stxs)])
     (define ctc-id (generate-temporary))
+    (define contract-def `#s(contract-def ,t #f #f ,typed-side))
     (values ctc-id
             #`(define-values (#,ctc-id)
                 #,(contract-def-property
-                   #'#f `#s(contract-def ,t #f #f ,typed-side))))))
+                   #'#f (λ () contract-def))))))
 
 (define (wt-core stx)
   (define-syntax-class typed-id

typed-racket-lib/typed-racket/typecheck/tc-expression.rkt

@@ -34,6 +34,14 @@
      (if expected
         (tc-expr/check #'e expected)
         (tc-expr #'e))]
+    [(exp:casted-expr^ e)
+     (define result (tc-expr #'e))
+     (match result
+       [(tc-result1: ty)
+        ((attribute exp.value) ty)
+        result]
+       [_
+        (tc-error/expr "Cannot cast expression that produces multiple values")])]
     [(_ e)
      (if expected
          (tc-expr/check #'e expected)

typed-racket-test/succeed/cast-mod.rkt

@@ -1,9 +1,74 @@
 #lang typed/racket/base
 
-(cast 2 Number)
-(cast 2 Integer)
-(cast (list 2 4) (Listof Byte))
-(cast (vector 2 4) (Vectorof Byte))
+(require typed/rackunit)
 
+(check-equal? (cast 2 Number) 2)
+(check-equal? (cast 2 Integer) 2)
+(check-equal? (cast (list 2 4) (Listof Byte)) (list 2 4))
+(check-pred vector? (cast (vector 2 4) (Vectorof Byte)))
+
+(check-equal? ((cast (lambda (x) 7) (String -> Number)) "seven") 7)
+
+(: pos-fx-sub1 : Positive-Fixnum -> Nonnegative-Fixnum)
+(define (pos-fx-sub1 x)
+  (sub1 x))
+
+(check-equal? ((cast pos-fx-sub1 (Number -> Number)) 5) 4)
+
+(check-exn #rx"expected: Positive-Fixnum\n *given: 0.5"
+           (λ () ((cast pos-fx-sub1 (Number -> Number)) 0.5) 4))
+
+(check-exn #rx"expected: Positive-Fixnum\n *given: \"hello\""
+           (λ () ((cast pos-fx-sub1 (String -> String)) "hello")))
+
+(check-exn #rx"expected: Positive-Fixnum\n *given: \"hello\""
+           (λ () ((cast pos-fx-sub1 (Any -> Any)) "hello")))
+
+(test-case "cast on mutator functions"
+  (: v : Boolean)
+  (define v #f)
+  (: f : Boolean -> Boolean)
+  (define (f x)
+    (set! v x)
+    x)
+
+  (check-equal? v #f)
+  (check-equal? ((cast f (Boolean -> Boolean)) #t) #t)
+  (check-equal? v #t)
+  (check-exn #rx"expected: \\(or/c #f #t\\)\n *given: \"hello\""
+             (λ () ((cast f (String -> String)) "hello")))
+  (check-equal? v #t
+                "if the previous test hadn't errored, this would be \"hello\" with type Boolean"))
+
+(test-case "cast on mutable boxes"
+  (: b1 : (Boxof Integer))
+  (define b1 (box 42))
+  (define b2 (cast b1 (Boxof String)))
+  (check-equal? (unbox b1) 42)
+  (check-exn #rx"expected: Integer\n *given: \"hi\""
+             (λ () (set-box! b2 "hi")))
+  (check-equal? (unbox b1) 42
+                "if the previous test hadn't errored, this would be \"hi\" with type Integer"))
+
+(test-case "cast on mutable vectors"
+  (: v1 : (Vectorof Integer))
+  (define v1 (vector 42))
+  (define v2 (cast v1 (Vectorof String)))
+  (check-equal? (vector-ref v1 0) 42)
+  (check-exn #rx"expected: Integer\n *given: \"hi\""
+             (λ () (vector-set! v2 0 "hi")))
+  (check-equal? (vector-ref v1 0) 42
+                "if the previous test hadn't errored, this would be \"hi\" with type Integer"))
+
+;; Struct definitions need to be at the module level for some reason.
+(struct (X) s ([i : X]) #:mutable)
+(test-case "cast on mutable structs"
+  (: s1 : (s Integer))
+  (define s1 (s 42))
+  (define s2 (cast s1 (s String)))
+  (check-equal? (s-i s1) 42)
+  (check-exn #rx"expected: Integer\n *given: \"hi\""
+             (λ () (set-s-i! s2 "hi")))
+  (check-equal? (s-i s1) 42
+                "if the previous test hadn't errored, this would be \"hi\" with type Integer"))
 
-((cast (lambda (x) 7) (String -> Number)) "seven")

typed-racket-test/succeed/cast-top-level.rkt

@@ -2,10 +2,80 @@
 
 (require typed/racket/base)
 
+(require typed/rackunit)
+
 (cast 2 Number)
 (cast 2 Integer)
 (cast (list 2 4) (Listof Byte))
 (cast (vector 2 4) (Vectorof Byte))
 
+(check-equal? (cast 2 Number) 2)
+(check-equal? (cast 2 Integer) 2)
+(check-equal? (cast (list 2 4) (Listof Byte)) (list 2 4))
+(check-pred vector? (cast (vector 2 4) (Vectorof Byte)))
+
+(check-equal? ((cast (lambda (x) 7) (String -> Number)) "seven") 7)
+
+(: pos-fx-sub1 : Positive-Fixnum -> Nonnegative-Fixnum)
+(define (pos-fx-sub1 x)
+  (sub1 x))
+
+(check-equal? ((cast pos-fx-sub1 (Number -> Number)) 5) 4)
+
+(check-exn #rx"expected: Positive-Fixnum\n *given: 0.5"
+           (λ () ((cast pos-fx-sub1 (Number -> Number)) 0.5) 4))
+
+(check-exn #rx"expected: Positive-Fixnum\n *given: \"hello\""
+           (λ () ((cast pos-fx-sub1 (String -> String)) "hello")))
+
+(check-exn #rx"expected: Positive-Fixnum\n *given: \"hello\""
+           (λ () ((cast pos-fx-sub1 (Any -> Any)) "hello")))
+
+(test-case "cast on mutator functions"
+  (: v : Boolean)
+  (define v #f)
+  (: f : Boolean -> Boolean)
+  (define (f x)
+    (set! v x)
+    x)
+
+  (check-equal? v #f)
+  (check-equal? ((cast f (Boolean -> Boolean)) #t) #t)
+  (check-equal? v #t)
+  (check-exn #rx"expected: \\(or/c #f #t\\)\n *given: \"hello\""
+             (λ () ((cast f (String -> String)) "hello")))
+  (check-equal? v #t
+                "if the previous test hadn't errored, this would be \"hello\" with type Boolean"))
+
+(test-case "cast on mutable boxes"
+  (: b1 : (Boxof Integer))
+  (define b1 (box 42))
+  (define b2 (cast b1 (Boxof String)))
+  (check-equal? (unbox b1) 42)
+  (check-exn #rx"expected: Integer\n *given: \"hi\""
+             (λ () (set-box! b2 "hi")))
+  (check-equal? (unbox b1) 42
+                "if the previous test hadn't errored, this would be \"hi\" with type Integer"))
+
+(test-case "cast on mutable vectors"
+  (: v1 : (Vectorof Integer))
+  (define v1 (vector 42))
+  (define v2 (cast v1 (Vectorof String)))
+  (check-equal? (vector-ref v1 0) 42)
+  (check-exn #rx"expected: Integer\n *given: \"hi\""
+             (λ () (vector-set! v2 0 "hi")))
+  (check-equal? (vector-ref v1 0) 42
+                "if the previous test hadn't errored, this would be \"hi\" with type Integer"))
+
+;; Struct definitions need to be at the top level for some reason.
+(struct (X) s ([i : X]) #:mutable)
+(test-case "cast on mutable structs"
+  (: s1 : (s Integer))
+  (define s1 (s 42))
+  (define s2 (cast s1 (s String)))
+  (check-equal? (s-i s1) 42)
+  (check-exn #rx"expected: Integer\n *given: \"hi\""
+             (λ () (set-s-i! s2 "hi")))
+  (check-equal? (s-i s1) 42
+                "if the previous test hadn't errored, this would be \"hi\" with type Integer"))
 
-((cast (lambda (x) 7) (String -> Number)) "seven")