diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
index 2663815..f2fec6b 100644
--- a/turnstile/examples/rosette/rosette.rkt
+++ b/turnstile/examples/rosette/rosette.rkt
@@ -10,7 +10,7 @@
            zero? void sub1 or and not add1 = - * + boolean? integer? list)
          (for-syntax (except-in "../../../turnstile/turnstile.rkt")))
 (provide (rename-out [ro:#%module-begin #%module-begin]))
-(extends "../stlc+union.rkt" #:except if #%app #%module-begin)
+(extends "../stlc+union+case.rkt" #:except if #%app #%module-begin add1 sub1 +)
 (reuse List list #:from "../stlc+cons.rkt")
 (require (only-in "../stlc+reco+var.rkt" [define stlc:define]))
 ;(require (only-in "../stlc+reco+var.rkt" define-type-alias))
@@ -49,11 +49,43 @@
 
 (define-typed-syntax app #:export-as #%app
   [(_ e_fn e_arg ...) ≫
-   [⊢ [e_fn ≫ e_fn- ⇒ : (~→ τ_in ... τ_out)]]
+   [⊢ [e_fn ≫ e_fn- ⇒ : (~→ ~! τ_in ... τ_out)]]
    #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
    (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
    [⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
    --------
+   [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]
+  [(_ e_fn e_arg ...) ≫
+   [⊢ [e_fn ≫ e_fn- ⇒ : (~case-> ~! . (~and ty_fns ((~→ . _) ...)))]]
+   [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
+   #:with τ_out
+   (for/first ([ty_f (stx->list #'ty_fns)]
+               #:when (syntax-parse ty_f
+                        [(~→ τ_in ... τ_out)
+                         (and (stx-length=? #'(τ_in ...) #'(e_arg ...))
+                              (typechecks? #'(τ_arg ...) #'(τ_in ...)))]))
+     (syntax-parse ty_f [(~→ _ ... t_out) #'t_out]))
+   #:fail-unless (syntax-e #'τ_out)
+   ; use (failing) typechecks? to get err msg
+   (syntax-parse #'ty_fns
+     [((~→ τ_in ... _) ...)
+      (let* ([τs_expecteds #'((τ_in ...) ...)]
+             [τs_given #'(τ_arg ...)]
+             [expressions #'(e_arg ...)])
+        (format (string-append "type mismatch\n"
+                               "  expected one of:\n"
+                               "    ~a\n"
+                               "  given: ~a\n"
+                               "  expressions: ~a")
+         (string-join
+          (stx-map
+           (lambda (τs_expected)
+             (string-join (stx-map type->str τs_expected) ", "))
+           τs_expecteds)
+          "\n    ")
+           (string-join (stx-map type->str τs_given) ", ")
+           (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))])
+   --------
    [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]])
 
 ;; ----------------------------------------------------------------------------
@@ -76,6 +108,20 @@
 (define-rosette-primop string? : (→ String Bool))
 (define-rosette-primop pregexp : (→ String Regexp))
 
+(define-rosette-primop add1 : (case-> (→ NegInt (U NegInt Zero))
+                                      (→ Zero PosInt)
+                                      (→ PosInt PosInt)
+                                      (→ Nat PosInt)
+                                      (→ Int Int)))
+(define-rosette-primop sub1 : (case-> (→ NegInt NegInt)
+                                      (→ Zero NegInt)
+                                      (→ PosInt Nat)
+                                      (→ Nat Int)
+                                      (→ Int Int)))
+(define-rosette-primop + : (case-> (→ Int Int Int)
+                                   (→ Nat Nat Nat)
+                                   (→ Num Num Num)))
+
 (define-typed-syntax equal?
   [(equal? e1 e2) ≫
    [⊢ [e1 ≫ e1- ⇒ : ty1]]
@@ -130,35 +176,19 @@
 (define-base-type BV) ; represents actual bitvectors
 
 ; a predicate recognizing bv's of a certain size
-(define-syntax BVPred 
-  (make-variable-like-transformer 
-   (add-orig #'(→ BV Bool) #'BVPred)))
-;(define-type-alias BVPred (→ BV Bool))
+(define-named-type-alias BVPred (→ BV Bool))
 
-;; TODO: fix me --- need subtyping?
-;(define-syntax Nat (make-rename-transformer #'Int))
-;(define-type-alias Nat Int)
-
-;; TODO: support higher order case --- need intersect types?
-(define-typed-syntax bv
-  [(_ e_val e_size) ≫
-   [⊢ [e_val ≫ e_val- ⇐ : Int]]
-   [⊢ [e_size ≫ e_size- ⇐ : BVPred]]
-   --------
-   [⊢ [_ ≫ (ro:bv e_val- e_size-) ⇒ : BV]]]
-  [(_ e_val e_size) ≫
-   [⊢ [e_val ≫ e_val- ⇐ : Int]]
-   [⊢ [e_size ≫ e_size- ⇐ : PosInt]]
-   --------
-   [⊢ [_ ≫ (ro:bv e_val- e_size-) ⇒ : BV]]])
+;; support higher order case with case-> types
+(define-rosette-primop bv : (case-> (→ Int BVPred BV)
+                                    (→ Int PosInt BV)))
 
 (define-rosette-primop bv? : (→ BV Bool))
-(define-rosette-primop bitvector : (→ Nat BVPred))
+(define-rosette-primop bitvector : (→ PosInt BVPred))
 (define-rosette-primop bitvector? : (→ BVPred Bool))
-(define-rosette-primop* bitvector bvpred : (→ Nat BVPred))
+(define-rosette-primop* bitvector bvpred : (→ PosInt BVPred))
 (define-rosette-primop* bitvector? bvpred? : (→ BVPred Bool))
-(define-rosette-primop bitvector-size : (→ BVPred Nat))
-(define-rosette-primop* bitvector-size bvpred-size : (→ BVPred Nat))
+(define-rosette-primop bitvector-size : (→ BVPred PosInt))
+(define-rosette-primop* bitvector-size bvpred-size : (→ BVPred PosInt))
 
 (define-rosette-primop bveq : (→ BV BV Bool))
 (define-rosette-primop bvslt : (→ BV BV Bool))
diff --git a/turnstile/examples/stlc+union+case.rkt b/turnstile/examples/stlc+union+case.rkt
index 9455b74..1567098 100644
--- a/turnstile/examples/stlc+union+case.rkt
+++ b/turnstile/examples/stlc+union+case.rkt
@@ -33,7 +33,7 @@
    --------
    [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]]
   [(_ e_fn e_arg ...) ≫
-   [⊢ [e_fn ≫ e_fn- ⇒ : (~case-> . (~and ty_fns ((~→ . _) ...)))]]
+   [⊢ [e_fn ≫ e_fn- ⇒ : (~case-> ~! . (~and ty_fns ((~→ . _) ...)))]]
    [⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
    #:with τ_out
    (for/first ([ty_f (stx->list #'ty_fns)]
@@ -42,6 +42,26 @@
                          (and (stx-length=? #'(τ_in ...) #'(e_arg ...))
                               (typechecks? #'(τ_arg ...) #'(τ_in ...)))]))
      (syntax-parse ty_f [(~→ _ ... t_out) #'t_out]))
+   #:fail-unless (syntax-e #'τ_out)
+   ; use (failing) typechecks? to get err msg
+   (syntax-parse #'ty_fns
+     [((~→ τ_in ... _) ...)
+      (let* ([τs_expecteds #'((τ_in ...) ...)]
+             [τs_given #'(τ_arg ...)]
+             [expressions #'(e_arg ...)])
+        (format (string-append "type mismatch\n"
+                               "  expected one of:\n"
+                               "    ~a\n"
+                               "  given: ~a\n"
+                               "  expressions: ~a")
+         (string-join
+          (stx-map
+           (lambda (τs_expected)
+             (string-join (stx-map type->str τs_expected) ", "))
+           τs_expecteds)
+          "\n    ")
+           (string-join (stx-map type->str τs_given) ", ")
+           (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))])
    --------
    [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
 
@@ -56,7 +76,7 @@
      ((current-type=?) t1 t2)
      (syntax-parse (list t1 t2)
        ; 2 U types, subtype = subset
-       [((~U* . tys1) (~U* . tys2))
+       [((~U* . tys1) _)
         (for/and ([t (stx->list #'tys1)])
           ((current-sub?) t t2))]
        ; 1 U type, 1 non-U type. subtype = member
@@ -64,7 +84,7 @@
         (for/or ([t (stx->list #'tys)])
           ((current-sub?) #'ty t))]
        ; 2 case-> types, subtype = subset
-       [((~case-> . tys1) (~case-> . tys2))
+       [(_ (~case-> . tys2))
         (for/and ([t (stx->list #'tys2)])
           ((current-sub?) t1 t))]
        ; 1 case-> , 1 non-case->
diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt
index 2f925b7..63ca9e0 100644
--- a/turnstile/examples/stlc+union.rkt
+++ b/turnstile/examples/stlc+union.rkt
@@ -3,6 +3,7 @@
  #:except #%app #%datum + add1 sub1 * Int Int? ~Int Float Float? ~Float)
 (reuse define-type-alias #:from "stlc+reco+var.rkt")
 (provide Int Num Nat U
+         define-named-type-alias
          (for-syntax current-sub?))
 
 ;; Simply-Typed Lambda Calculus, plus union types
@@ -21,6 +22,12 @@
 ;; - also *
 ;; Other: sub? current-sub?
 
+(define-syntax define-named-type-alias
+  (syntax-parser
+    [(define-named-type-alias Name:id τ:type)
+     #'(define-syntax Name
+         (make-variable-like-transformer (add-orig #'τ #'Name)))]))
+
 (define-base-types Zero NegInt PosInt Float)
 (define-type-constructor U* #:arity > 0)
 
diff --git a/turnstile/examples/tests/rosette/rosette-tests.rkt b/turnstile/examples/tests/rosette/rosette-tests.rkt
index a9eacf4..3b78bcf 100644
--- a/turnstile/examples/tests/rosette/rosette-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-tests.rkt
@@ -1,28 +1,30 @@
 #lang s-exp "../../rosette/rosette.rkt"
 (require "../rackunit-typechecking.rkt")
 
-(check-type (sub1 10) : Int -> 9) ; TODO: Nat
-(check-type (sub1 0) : Int -> -1) ; TODO: NegInt
-(check-type (sub1 -1) : Int -> -2) ; TODO: NegInt
+(check-type (sub1 10) : Nat -> 9)
+(check-type (sub1 0) : NegInt -> -1)
+(check-type (sub1 -1) : NegInt -> -2)
 
-;(check-type bv : (→ Int BVPred BV))
+(check-type bv : (case-> (→ Int BVPred BV)
+                         (→ Int PosInt BV)))
 (typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String")
+(check-type (bv 1 2) : BV -> (bv 1 (bvpred 2)))
 (check-type (bv 1 (bvpred 2)) : BV -> (bv 1 (bvpred 2)))
 
 (typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero")
-(check-type bitvector : (→ Nat BVPred))
+(check-type bitvector : (→ PosInt BVPred))
 (check-type (bitvector 3) : BVPred)
 (typecheck-fail ((bitvector 4) 1))
 (check-type ((bitvector 4) (bv 10 (bvpred 4))) :  Bool)
 
 ;; same as above, but with bvpred
-(check-type bvpred : (→ Nat BVPred))
+(check-type bvpred : (→ PosInt BVPred))
 (check-type (bvpred 3) : BVPred)
 (typecheck-fail ((bvpred 4) 1))
 (check-type ((bvpred 4) (bv 10 (bvpred 4))) :  Bool)
 ;; typed rosette catches this during typechecking, 
 ;; whereas untyped rosette uses a runtime exn
-(typecheck-fail (bvpred -1) #:with-msg "expected Nat, given NegInt")
+(typecheck-fail (bvpred -1) #:with-msg "expected PosInt, given NegInt")
 ;(check-runtime-exn (bvpred -1))
 
 (typecheck-fail (bitvector? "2"))
@@ -107,3 +109,19 @@
 (check-type (integer->bitvector 3
               (if c (bitvector 5) (bitvector 6))) 
   : BV -> (if c (bv 3 5) (bv 3 6)))
+
+;; case-> subtyping
+(check-type ((λ ([f : (→ Int Int)]) (f 10)) add1) : Int -> 11)
+(check-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Int -> 11)
+(check-type ((λ ([f : (case-> (→ Nat Nat)
+                              (→ Int Int))]) (f 10)) add1) : Int -> 11)
+(check-not-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Nat)
+(check-type ((λ ([f : (case-> (→ Nat Nat)
+                              (→ Int Int))]) (f 10)) add1) : Nat -> 11)
+(typecheck-fail ((λ ([f : (case-> (→ Zero Zero)
+                                  (→ Int Int))]) (f 10)) add1) 
+ #:with-msg
+ (string-append "expected \\(case-> \\(→ Zero Zero\\) \\(→ Int Int\\)\\), "
+                "given \\(case-> \\(→ NegInt \\(U NegInt Zero\\)\\) \\(→ Zero PosInt\\) "
+                "\\(→ PosInt PosInt\\) \\(→ Nat PosInt\\) \\(→ Int Int\\)\\)"))
+