diff --git a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
index 8cf8ae2c..4df335ef 100644
--- a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
+++ b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
@@ -287,8 +287,10 @@
    ;; that `(cast-table-ref id)` can get that type here.
    (λ ()
      (define type-stx
-       (or (cast-table-ref id)
-           #f))
+       (let ([types (cast-table-ref id)])
+         (if types
+             #`(U #,@types)
+             #f)))
      `#s(contract-def ,type-stx ,flat? ,maker? typed))))
 
 
@@ -353,7 +355,7 @@
                                      (make-contract-def-rhs/from-typed existing-ty-id #f #f)))
             (define (store-existing-type existing-type)
               (check-no-free-vars existing-type #'v)
-              (cast-table-set! existing-ty-id (datum->syntax #f existing-type #'v)))
+              (cast-table-add! existing-ty-id (datum->syntax #f existing-type #'v)))
             (define (check-valid-type _)
               (define type (parse-type #'ty))
               (check-no-free-vars type #'ty))
diff --git a/typed-racket-lib/typed-racket/private/cast-table.rkt b/typed-racket-lib/typed-racket/private/cast-table.rkt
index 44aace7a..6b1738fa 100644
--- a/typed-racket-lib/typed-racket/private/cast-table.rkt
+++ b/typed-racket-lib/typed-racket/private/cast-table.rkt
@@ -1,7 +1,7 @@
 #lang racket/base
 
 (provide cast-table-ref
-         cast-table-set!)
+         cast-table-add!)
 
 (require syntax/id-table)
 
@@ -13,13 +13,30 @@
 ;; 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.
+;;
+;; If a cast is within a `case->` functions, it is typechecked with multiple
+;; types. The cast table holds all of those types, and the contract layer
+;; must protect values of any one of those types. This is why the cast-table
+;; contains lists, and why `cast-table-ref` returns a list on success.
 
+;; cast-table : (Free-Id-Tableof (Listof Type-Stx))
+;; interpretation:
+;;   A mapping from lifted-contract-def identifiers to the possible existing
+;;   types of values that the contract has to protect as they go from typed
+;;   to untyped code.
 (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-add! : Id Type-Stx -> Void
+;; Associates the given type with the given contract-def identifier, to signify
+;; that the contract generated by `id` must protect values of type `type-stx`.
+(define (cast-table-add! id type-stx)
+  (free-id-table-update! cast-table id
+    (λ (lst) (cons type-stx lst))
+    (λ () '())))
 
-;; cast-table-ref : Id -> (U False Type-Stx)
+;; cast-table-ref : Id -> (U False (Listof Type-Stx))
+;; On success, returns a list containing all the types of values that the
+;; contract must project as they go from typed to untyped code. On failure,
+;; returns false.
 (define (cast-table-ref id)
   (free-id-table-ref cast-table id #f))
diff --git a/typed-racket-test/succeed/case-arrow-cast-contract.rkt b/typed-racket-test/succeed/case-arrow-cast-contract.rkt
new file mode 100644
index 00000000..89bfd92a
--- /dev/null
+++ b/typed-racket-test/succeed/case-arrow-cast-contract.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket
+
+(require typed/rackunit)
+
+(: f : (case-> (-> (Boxof String) Any)
+               (-> (Boxof Integer) Any)))
+(define (f x)
+  (cast x Any))
+
+(check-equal? (f (box "a")) (box "a"))
+(check-equal? (f (box 1)) (box 1))
+