diff --git a/collects/tests/typed-racket/fail/pr13662.rkt b/collects/tests/typed-racket/fail/pr13662.rkt
new file mode 100644
index 00000000..20f04a3e
--- /dev/null
+++ b/collects/tests/typed-racket/fail/pr13662.rkt
@@ -0,0 +1,20 @@
+#;
+(exn-pred #rx"contract violation" #rx"blaming: untyped")
+#lang racket/load
+
+(module typed typed/racket
+  (provide b g)
+
+  (: b (Boxof (All (a) (a -> a))))
+  (define b ((inst box (All (a) (a -> a))) (lambda (a) a)))
+  
+  (: g (Integer -> Integer))
+  (define (g x)
+    ((unbox b) x)))
+
+(module untyped racket
+  (require 'typed)
+  (set-box! b (lambda (x) "hello"))
+  (g 5))
+
+(require 'untyped)
diff --git a/collects/tests/typed-racket/fail/pr13663.rkt b/collects/tests/typed-racket/fail/pr13663.rkt
new file mode 100644
index 00000000..32babd73
--- /dev/null
+++ b/collects/tests/typed-racket/fail/pr13663.rkt
@@ -0,0 +1,17 @@
+#;
+(exn-pred #rx"contract violation" #rx"blaming: top-level")
+#lang racket/load
+
+(module typed typed/racket
+  (provide g)
+
+  (: f (Byte -> Natural))
+  (define (f x) (add1 x))
+  (: g ((Boxof Any) -> Void))
+  (define (g b) 
+    (set-box! b f)))
+
+(require 'typed)
+(define b (box #f))
+(g b)
+(displayln ((unbox b) "foo"))
diff --git a/collects/tests/typed-racket/fail/pr13665.rkt b/collects/tests/typed-racket/fail/pr13665.rkt
new file mode 100644
index 00000000..37e3bc11
--- /dev/null
+++ b/collects/tests/typed-racket/fail/pr13665.rkt
@@ -0,0 +1,23 @@
+#;
+(exn-pred #rx"contract violation"
+          #rx"higher-order value passed as `Any` in untyped code"
+          #rx"blaming: top-level")
+#lang racket/load
+
+(module typed typed/racket
+  (provide g)
+
+  (define-type Foo (Rec a (U (List Any) (Boxof a))))
+
+
+  (: f (Byte -> Natural))
+  (define (f x) (add1 x))
+  (: g (Foo -> Void))
+  (define (g b) 
+    (when (box? b)
+      (set-box! b (list f)))))
+
+(require 'typed)
+(define b (box (list #f)))
+(g b)
+(displayln ((first (unbox b)) "foo"))
diff --git a/collects/typed-racket/private/type-contract.rkt b/collects/typed-racket/private/type-contract.rkt
index 3a8c9f26..53312a1c 100644
--- a/collects/typed-racket/private/type-contract.rkt
+++ b/collects/typed-racket/private/type-contract.rkt
@@ -116,17 +116,36 @@
 (define (contract-kind->keyword sym)
   (string->keyword (symbol->string sym)))
 
-(define (type->contract ty fail #:typed-side [from-typed? #t] #:kind [kind 'impersonator])
+(define (from-typed? side)
+  (case side
+   [(typed both) #t]
+   [(untyped) #f]))
+
+(define (from-untyped? side)
+  (case side
+   [(untyped both) #t]
+   [(typed) #f]))
+
+(define (flip-side side)
+  (case side
+   [(typed) 'untyped]
+   [(untyped) 'typed]
+   [(both) 'both]))
+
+
+(define (type->contract ty fail #:typed-side [typed-side #t] #:kind [kind 'impersonator])
   (define vars (make-parameter '()))  
   (define current-contract-kind (make-parameter flat-sym))
   (define (increase-current-contract-kind! kind)
     (current-contract-kind (contract-kind-max (current-contract-kind) kind)))
   (let/ec exit
-    (let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null] [kind kind])
+    (let loop ([ty ty] [typed-side (if typed-side 'typed 'untyped)] [structs-seen null] [kind kind])
       (define (t->c t #:seen [structs-seen structs-seen] #:kind [kind kind])
-        (loop t pos? from-typed? structs-seen kind))
+        (loop t typed-side structs-seen kind))
       (define (t->c/neg t #:seen [structs-seen structs-seen] #:flat [kind kind])
-        (loop t (not pos?) (not from-typed?) structs-seen kind))
+        (loop t (flip-side typed-side) structs-seen kind))
+      (define (t->c/both t #:seen [structs-seen structs-seen] #:flat [kind kind])
+        (loop t 'both structs-seen kind))
       (define (t->c/fun f #:method [method? #f])
         (match f
           [(Function: (list (top-arr:))) #'(case->)]
@@ -205,7 +224,7 @@
                               (and rst (t->c/neg rst))))]
                    ;; functions with filters or objects
                    [(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f '())
-                    (if from-typed?
+                    (if (not (from-untyped? typed-side))
                         (values (map t->c/neg dom)
                                 null
                                 (map t->c rngs)
@@ -250,13 +269,13 @@
         [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
         ;; any/c doesn't provide protection in positive position
         [(Univ:)
-         (cond [from-typed? 
+         (cond [(from-typed? typed-side)
                 (set-chaperone!)
                 #'any-wrap/c]
                [else #'any/c])]
         ;; we special-case lists:
         [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
-         (if (and (not from-typed?) (type-equal? elem-ty t:Univ))
+         (if (and (not (from-typed? typed-side)) (type-equal? elem-ty t:Univ))
              #'list?
              #`(listof #,(t->c elem-ty)))]
         [(? (lambda (e) (eq? t:Any-Syntax e))) #'syntax?]
@@ -331,13 +350,13 @@
         [(Sequence: ts) #`(sequence/c #,@(map t->c ts))]
         [(Vector: t)
          (set-chaperone!)
-         #`(vectorof #,(t->c t))]
+         #`(vectorof #,(t->c/both t))]
         [(HeterogeneousVector: ts)
          (set-chaperone!)
-         #`(vector/c #,@(map t->c ts))]
+         #`(vector/c #,@(map t->c/both ts))]
         [(Box: t)
          (set-chaperone!)
-         #`(box/c #,(t->c t))]
+         #`(box/c #,(t->c/both t))]
         [(Pair: t1 t2)
          #`(cons/c #,(t->c t1) #,(t->c t2))]
         [(Promise: t)
@@ -347,20 +366,20 @@
          #`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
         [(Continuation-Mark-Keyof: t)
          (set-chaperone!)
-         #`(continuation-mark-key/c #,(t->c t))]
+         #`(continuation-mark-key/c #,(t->c/both t))]
         ;; TODO: this is not quite right for case->
         [(Prompt-Tagof: s (Function: (list (arr: (list ts ...) _ _ _ _))))
          (set-chaperone!)
-         #`(prompt-tag/c #,@(map t->c ts) #:call/cc #,(t->c s))]
+         #`(prompt-tag/c #,@(map t->c/both ts) #:call/cc #,(t->c/both s))]
         ;; TODO
         [(F: v) (cond [(assoc v (vars)) => second]
                       [else (int-err "unknown var: ~a" v)])]
         [(Poly: vs b)
-         (if from-typed?
-             ;; in positive position, no checking needed for the variables
+         (if (not (from-untyped? typed-side))
+             ;; in typed positions, no checking needed for the variables
              (parameterize ([vars (append (for/list ([v vs]) (list v #'any/c)) (vars))])
                (t->c b))
-             ;; in negative position, use `parameteric/c'
+             ;; in untyped positions, use `parameteric/c'
              (match-let ([(Poly-names: vs-nm _) ty])
                (with-syntax ([(v ...) (generate-temporaries vs-nm)])
                  (set-impersonator!)
@@ -372,12 +391,12 @@
            (with-syntax ([(n*) (generate-temporaries (list n-nm))])
              (parameterize ([vars (cons (list n #'n*) (vars))]
                             [current-contract-kind
-			     (contract-kind-min kind chaperone-sym)])
-               (define ctc (t->c b))
+                             (contract-kind-min kind chaperone-sym)])
+               (define ctc (t->c/both b))
                #`(letrec ([n* (recursive-contract
                                 #,ctc
                                 #,(contract-kind->keyword
-				   (current-contract-kind)))])
+                                   (current-contract-kind)))])
                    n*))))]
         [(Instance: (? Mu? t))
          (t->c (make-Instance (resolve-once t)))]
@@ -410,10 +429,11 @@
                   (with-syntax* ([rec (generate-temporary 'rec)])
                     (define required-recursive-kind
                        (contract-kind-min kind (if mut? impersonator-sym chaperone-sym)))
+                    (define t->c/mut (if mut? t->c/both t->c))
                     ;(printf "kind: ~a mut-k: ~a req-rec-kind: ~a\n" kind (if mut? impersonator-sym chaperone-sym) required-recursive-kind)
                     (parameterize ((current-contract-kind (contract-kind-min kind chaperone-sym)))
-                      (let ((fld-ctc (t->c fty #:seen (cons (cons ty #'rec) structs-seen)
-                                           #:kind required-recursive-kind)))
+                      (let ((fld-ctc (t->c/mut fty #:seen (cons (cons ty #'rec) structs-seen)
+                                               #:kind required-recursive-kind)))
                         #`(let ((rec (recursive-contract struct-ctc #,(contract-kind->keyword (current-contract-kind)))))
                             #,fld-ctc))))))
               #`(letrec ((struct-ctc (struct/c #,nm #,@field-contracts))) struct-ctc))]