diff --git a/collects/tests/typed-racket/succeed/pr13710.rkt b/collects/tests/typed-racket/succeed/pr13710.rkt
new file mode 100644
index 0000000000..27e691889b
--- /dev/null
+++ b/collects/tests/typed-racket/succeed/pr13710.rkt
@@ -0,0 +1,23 @@
+#lang typed/racket
+
+(: convert-it (Any -> (HashTable Symbol Number)))
+(define (convert-it a)
+  (if (hash? a)
+      (begin
+        (hash-ref a 3)
+        (hash-has-key? a 3)
+        (ann (hash-remove a 3) HashTableTop)
+        (hash-remove! a 3)
+        (length (hash-map a (lambda: ([x : Any] [y : Any]) x)))
+        (hash-for-each a (lambda: ([x : Any] [y : Any]) (display x)))
+        (add1 (hash-count a))
+        (length (hash-keys a))
+        (length (hash-values a))
+        (length (hash->list a))
+        (for ([(k v) (in-hash a)])
+          (display k))
+        (for/hash: : (HashTable Symbol Number) ([v (in-hash-values a)])
+          (values 'x 1))
+        (for/hash: : (HashTable Symbol Number) ([k (in-hash-keys a)])
+          (values 'x 1)))
+      (error 'convert-it "not a hash ~s" a)))
diff --git a/collects/typed-racket/base-env/base-env.rkt b/collects/typed-racket/base-env/base-env.rkt
index ad881fd510..f4e10e2730 100644
--- a/collects/typed-racket/base-env/base-env.rkt
+++ b/collects/typed-racket/base-env/base-env.rkt
@@ -904,25 +904,36 @@
 [hash-set! (-poly (a b) ((-HT a b) a b . -> . -Void))]
 [hash-ref (-poly (a b c)
                  (cl-> [((-HT a b) a) b]
-                       [((-HT a b) a (-> c)) (Un b c)]))]
+                       [((-HT a b) a (-> c)) (Un b c)]
+                       [(-HashTop a) Univ]
+                       [(-HashTop a (-> c)) Univ]))]
 [hash-ref! (-poly (a b)
                   (cl-> [((-HT a b) a b) b]
                         [((-HT a b) a (-> b)) b]))]
-[hash-has-key? (-poly (a b) (-> (-HT a b) a B))]
+[hash-has-key? (-poly (a b) (cl-> [((-HT a b) a) b]
+                                  [(-HashTop a) b]))]
 [hash-update! (-poly (a b)
                      (cl-> [((-HT a b) a (-> b b)) -Void]
                            [((-HT a b) a (-> b b) (-> b)) -Void]))]
 [hash-update (-poly (a b)
                     (cl-> [((-HT a b) a (-> b b)) (-HT a b)]
                           [((-HT a b) a (-> b b) (-> b)) (-HT a b)]))]
-[hash-remove (-poly (a b) ((-HT a b) a . -> . (-HT a b)))]
-[hash-remove! (-poly (a b) ((-HT a b) a . -> . -Void))]
-[hash-map (-poly (a b c) ((-HT a b) (a b . -> . c) . -> . (-lst c)))]
-[hash-for-each (-poly (a b c) (-> (-HT a b) (-> a b c) -Void))]
-[hash-count (-poly (a b) (-> (-HT a b) -Index))]
-[hash-keys (-poly (a b) ((-HT a b) . -> . (-lst a)))]
-[hash-values (-poly (a b) ((-HT a b) . -> . (-lst b)))]
-[hash->list (-poly (a b) ((-HT a b) . -> . (-lst (-pair a b))))]
+[hash-remove (-poly (a b) (cl-> [((-HT a b) a) (-HT a b)]
+                                [(-HashTop a) -HashTop]))]
+[hash-remove! (-poly (a b) (cl-> [((-HT a b) a) -Void]
+                                 [(-HashTop a) -Void]))]
+[hash-map (-poly (a b c) (cl-> [((-HT a b) (a b . -> . c)) (-lst c)]
+                               [(-HashTop (Univ Univ . -> . c)) (-lst c)]))]
+[hash-for-each (-poly (a b c) (cl-> [((-HT a b) (-> a b c)) -Void]
+                                    [(-HashTop (-> Univ Univ c)) -Void]))]
+[hash-count (-poly (a b) (cl-> [((-HT a b)) -Index]
+                               [(-HashTop) -Index]))]
+[hash-keys (-poly (a b) (cl-> [((-HT a b)) (-lst a)]
+                              [(-HashTop) (-lst Univ)]))]
+[hash-values (-poly (a b) (cl-> [((-HT a b)) (-lst b)]
+                                [(-HashTop) (-lst Univ)]))]
+[hash->list (-poly (a b) (cl-> [((-HT a b)) (-lst (-pair a b))]
+                               [(-HashTop) (-lst (-pair Univ Univ))]))]
 
 [hash-copy (-poly (a b) (-> (-HT a b) (-HT a b)))]
 [eq-hash-code (-poly (a) (-> a -Integer))]
diff --git a/collects/typed-racket/base-env/base-special-env.rkt b/collects/typed-racket/base-env/base-special-env.rkt
index bcb5284848..9ed1915d76 100644
--- a/collects/typed-racket/base-env/base-special-env.rkt
+++ b/collects/typed-racket/base-env/base-special-env.rkt
@@ -92,7 +92,9 @@
    (-poly (a) (-> (-lst a) (-seq a)))]
   ;; in-vector
   [(make-template-identifier 'in-vector 'racket/private/for)
-   (-poly (a) (->opt (-vec a) [-Int (-opt -Int) -Int] (-seq a)))]
+   (-poly (a)
+          (cl->* (->opt (-vec a) [-Int (-opt -Int) -Int] (-seq a))
+                 (->opt -VectorTop [-Int (-opt -Int) -Int] (-seq Univ))))]
   ;; in-string
   [(make-template-identifier 'in-string 'racket/private/for)
    (->opt -String [-Int (-opt -Int) -Int] (-seq -Char))]
@@ -101,11 +103,17 @@
    (->opt -Bytes [-Int (-opt -Int) -Int] (-seq -Byte))]
   ;; in-hash and friends
   [(make-template-identifier 'in-hash 'racket/private/for)
-   (-poly (a b) (-> (-HT a b) (-seq a b)))]
+   (-poly (a b)
+          (cl-> [((-HT a b)) (-seq a b)]
+                [(-HashTop) (-seq Univ Univ)]))]
   [(make-template-identifier 'in-hash-keys 'racket/private/for)
-   (-poly (a b) (-> (-HT a b) (-seq a)))]
+   (-poly (a b)
+          (cl-> [((-HT a b)) (-seq a)]
+                [(-HashTop) (-seq Univ)]))]
   [(make-template-identifier 'in-hash-values 'racket/private/for)
-   (-poly (a b) (-> (-HT a b) (-seq b)))]
+   (-poly (a b)
+          (cl-> [((-HT a b)) (-seq b)]
+                [(-HashTop) (-seq Univ)]))]
   ;; in-port
   [(make-template-identifier 'in-port 'racket/private/for)
    (->opt [(-> -Input-Port Univ) -Input-Port] (-seq Univ))]
diff --git a/collects/typed-racket/base-env/base-types.rkt b/collects/typed-racket/base-env/base-types.rkt
index 49530b238d..c3039a310b 100644
--- a/collects/typed-racket/base-env/base-types.rkt
+++ b/collects/typed-racket/base-env/base-types.rkt
@@ -111,6 +111,8 @@
 [Sexp -Sexp]         ;; (Sexpof (U)), syntax->datum of "2D" syntax
 [Identifier Ident]
 [Procedure top-func]
+[VectorTop -VectorTop]
+[HashTableTop -HashTop]
 [Keyword -Keyword]
 [Thread -Thread]
 [Resolved-Module-Path -Resolved-Module-Path]