diff --git a/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
index 895a71c3..e7aa94d7 100644
--- a/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
+++ b/typed-racket-doc/typed-racket/scribblings/reference/types.scrbl
@@ -389,11 +389,30 @@ corresponding to @racket[trest], where @racket[bound]
 }
 
 
-@defform[(HashTable k v)]{is the type of a @rtech{hash table} with key type
-   @racket[k] and value type @racket[v].
+@defform[(Immutable-HashTable k v)]{is the type of an immutable @rtech{hash table}
+   with key type @racket[k] and value type @racket[v].
 
 @ex[#hash((a . 1) (b . 2))]
 }
+@defform[(Mutable-HashTable k v)]{is the type of a mutable @rtech{hash table}
+   that holds keys strongly (see @r-reference-secref{weakbox})
+   with key type @racket[k] and value type @racket[v].
+
+@ex[(make-hash '((a . 1) (b . 2)))]
+}
+
+@defform[(Weak-HashTable k v)]{is the type of a mutable @rtech{hash table}
+   that holds keys weakly with key type @racket[k] and value type @racket[v].
+
+@ex[(make-weak-hash '((a . 1) (b . 2)))]
+}
+
+@defform[(HashTable k v)]{is the type of a mutable or immutable @rtech{hash table}
+   with key type @racket[k] and value type @racket[v].
+
+@ex[(make-hash '((a . 1) (b . 2)))]
+}
+
 @defidform[HashTableTop]{is the type of a @rtech{hash table} with unknown key
   and value types and is the supertype of all hash table types. Only read-only
   hash table operations (e.g.
@@ -403,6 +422,12 @@ corresponding to @racket[trest], where @racket[bound]
 @ex[(lambda: ([x : Any]) (if (hash? x) x (error "not a hash table!")))]
 }
 
+@defidform[Mutable-HashTableTop]{is the type of a mutable @rtech{hash table}
+  that holds keys strongly with unknown key and value types.}
+
+@defidform[Weak-HashTableTop]{is the type of a mutable @rtech{hash table}
+  that holds keys weakly with unknown key and value types.}
+
 @defform[(Setof t)]{is the type of a @rtech{hash set} of
 @racket[t]. This includes custom hash sets, but not mutable hash set
 or sets that are implemented using @racket[gen:set].
@@ -835,4 +860,4 @@ this top type.
 @defform[(Opaque t)]{A type constructed using the @racket[#:opaque]
 clause of @racket[require/typed].}
 
-@(close-eval the-eval)
\ No newline at end of file
+@(close-eval the-eval)
diff --git a/typed-racket-doc/typed-racket/scribblings/utils.rkt b/typed-racket-doc/typed-racket/scribblings/utils.rkt
index 1874762c..7a52f3d2 100644
--- a/typed-racket-doc/typed-racket/scribblings/utils.rkt
+++ b/typed-racket-doc/typed-racket/scribblings/utils.rkt
@@ -14,6 +14,10 @@
   (secref tag #:doc '(lib "typed-racket/scribblings/ts-guide.scrbl")))
 (define (tr-reference-secref tag)
   (secref tag #:doc '(lib "typed-racket/scribblings/ts-reference.scrbl")))
+(define (r-guide-secref tag)
+  (secref tag #:doc '(lib "scribblings/guide/guide.scrbl")))
+(define (r-reference-secref tag)
+  (secref tag #:doc '(lib "scribblings/reference/reference.scrbl")))
 
 (define ** (let ([* #f]) @racket[*]))
 
diff --git a/typed-racket-lib/typed-racket/base-env/base-env.rkt b/typed-racket-lib/typed-racket/base-env/base-env.rkt
index 8ee2af17..adc4a006 100644
--- a/typed-racket-lib/typed-racket/base-env/base-env.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-env.rkt
@@ -57,7 +57,8 @@
 [eq? (-> Univ Univ B)]
 
 [equal?/recur (-> Univ Univ (-> Univ Univ Univ) B)]
-[immutable? (-> Univ B)]
+[immutable? (asym-pred Univ B (-PS (-is-type 0 (Un -Bytes -BoxTop -String -VectorTop (-Immutable-HT Univ Univ)))
+                                   (-not-type 0 (Un (-Immutable-HT Univ Univ)))))]
 [prop:equal+hash -Struct-Type-Property]
 
 ;; Section 4.1.1 (racket/bool)
@@ -915,77 +916,87 @@
 [box? (make-pred-ty -BoxTop)]
 
 ;; Section 4.13 (Hash Tables)
-[hash? (make-pred-ty -HashtableTop)]
-[hash-eq? (-> -HashtableTop B)]
-[hash-eqv? (-> -HashtableTop B)]
-[hash-equal? (-> -HashtableTop B)]
-[hash-weak? (-> -HashtableTop B)]
-[hash (-poly (a b) (cl->* (-> (-HT a b))
-                          (a b . -> . (-HT a b))
-                          (a b a b . -> . (-HT a b))
-                          (a b a b a b . -> . (-HT a b))
-                          (a b a b a b a b . -> . (-HT a b))))]
-[hasheqv (-poly (a b) (cl->* (-> (-HT a b))
-                             (a b . -> . (-HT a b))
-                             (a b a b . -> . (-HT a b))
-                             (a b a b a b . -> . (-HT a b))
-                             (a b a b a b a b . -> . (-HT a b))))]
-[hasheq (-poly (a b) (cl->* (-> (-HT a b))
-                            (a b . -> . (-HT a b))
-                            (a b a b . -> . (-HT a b))
-                            (a b a b a b . -> . (-HT a b))
-                            (a b a b a b a b . -> . (-HT a b))))]
-[make-hash (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
-[make-hasheq (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
-[make-hasheqv (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
-[make-weak-hash (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
-[make-weak-hasheq (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
-[make-weak-hasheqv (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
-[make-immutable-hash (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
-[make-immutable-hasheq (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
-[make-immutable-hasheqv (-poly (a b) (->opt [(-lst (-pair a b))] (-HT a b)))]
+[hash? (make-pred-ty -HashTableTop)]
+[hash-eq? (-> -HashTableTop B)]
+[hash-eqv? (-> -HashTableTop B)]
+[hash-equal? (-> -HashTableTop B)]
+[hash-weak? (asym-pred -HashTableTop B (-PS (-is-type 0 -Weak-HashTableTop) (-not-type 0 -Weak-HashTableTop)))]
+[hash (-poly (a b) (cl->* (-> (-Immutable-HT a b))
+                          (a b . -> . (-Immutable-HT a b))
+                          (a b a b . -> . (-Immutable-HT a b))
+                          (a b a b a b . -> . (-Immutable-HT a b))
+                          (a b a b a b a b . -> . (-Immutable-HT a b))))]
+[hasheqv (-poly (a b) (cl->* (-> (-Immutable-HT a b))
+                             (a b . -> . (-Immutable-HT a b))
+                             (a b a b . -> . (-Immutable-HT a b))
+                             (a b a b a b . -> . (-Immutable-HT a b))
+                             (a b a b a b a b . -> . (-Immutable-HT a b))))]
+[hasheq (-poly (a b) (cl->* (-> (-Immutable-HT a b))
+                            (a b . -> . (-Immutable-HT a b))
+                            (a b a b . -> . (-Immutable-HT a b))
+                            (a b a b a b . -> . (-Immutable-HT a b))
+                            (a b a b a b a b . -> . (-Immutable-HT a b))))]
+[make-hash (-poly (a b) (->opt [(-lst (-pair a b))] (-Mutable-HT a b)))]
+[make-hasheq (-poly (a b) (->opt [(-lst (-pair a b))] (-Mutable-HT a b)))]
+[make-hasheqv (-poly (a b) (->opt [(-lst (-pair a b))] (-Mutable-HT a b)))]
+[make-weak-hash (-poly (a b) (->opt [(-lst (-pair a b))] (-Weak-HT a b)))]
+[make-weak-hasheq (-poly (a b) (->opt [(-lst (-pair a b))] (-Weak-HT a b)))]
+[make-weak-hasheqv (-poly (a b) (->opt [(-lst (-pair a b))] (-Weak-HT a b)))]
+[make-immutable-hash (-poly (a b) (->opt [(-lst (-pair a b))] (-Immutable-HT a b)))]
+[make-immutable-hasheq (-poly (a b) (->opt [(-lst (-pair a b))] (-Immutable-HT a b)))]
+[make-immutable-hasheqv (-poly (a b) (->opt [(-lst (-pair a b))] (-Immutable-HT a b)))]
 
-[hash-set (-poly (a b) ((-HT a b) a b . -> . (-HT a b)))]
+[hash-set (-poly (a b) ((-HT a b) a b . -> . (-Immutable-HT a b)))]
 [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 (-val #f)) (-opt b)]
                        [((-HT a b) a (-> c)) (Un b c)]
-                       [(-HashtableTop a) Univ]
-                       [(-HashtableTop a (-val #f)) Univ]
-                       [(-HashtableTop a (-> c)) Univ]))]
+                       [(-HashTableTop a) Univ]
+                       [(-HashTableTop a (-val #f)) Univ]
+                       [(-HashTableTop a (-> c)) Univ]))]
 [hash-ref! (-poly (a b) (-> (-HT a b) a (-> b) b))]
-[hash-has-key? (-HashtableTop Univ . -> . B)]
+[hash-has-key? (-HashTableTop Univ . -> . 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) (cl-> [((-HT a b) Univ) (-HT a b)]
-                                [(-HashtableTop Univ) -HashtableTop]))]
+                    (cl-> [((-HT a b) a (-> b b)) (-Immutable-HT a b)]
+                          [((-HT a b) a (-> b b) (-> b)) (-Immutable-HT a b)]))]
+[hash-remove (-poly (a b) (cl-> [((-HT a b) Univ) (-Immutable-HT a b)]
+                                [(-HashTableTop Univ) (-Immutable-HT Univ Univ)]))]
 [hash-remove! (-poly (a b) (cl-> [((-HT a b) a) -Void]
-                                 [(-HashtableTop a) -Void]))]
-[hash-clear! (-> -HashtableTop -Void)]
-[hash-clear (-poly (a b) (cl-> [((-HT a b)) (-HT a b)]
-                               [(-HashtableTop) -HashtableTop]))]
-[hash-copy-clear (-poly (a b) (cl-> [((-HT a b)) (-HT a b)]
-                                    [(-HashtableTop) -HashtableTop]))]
+                                 [(-HashTableTop a) -Void]))]
+[hash-clear! (-> -HashTableTop -Void)]
+[hash-clear (-poly (a b) (cl-> [((-HT a b)) (-Immutable-HT a b)]
+                               [(-HashTableTop) (-Immutable-HT Univ Univ)]))]
+[hash-copy-clear (-poly (a b) (cl-> [((-Immutable-HT a b)) (-Immutable-HT a b)]
+                                    [((-Mutable-HT a b)) (-Mutable-HT a b)]
+                                    [(-Mutable-HashTableTop) -Mutable-HashTableTop]
+                                    [((-Weak-HT a b)) (-Weak-HT a b)]
+                                    [(-Weak-HashTableTop) -Weak-HashTableTop]
+                                    [((-HT a b)) (-HT a b)]
+                                    [(-HashTableTop) -HashTableTop]))]
 
 [hash-map (-poly (a b c) (cl-> [((-HT a b) (a b . -> . c)) (-lst c)]
-                               [(-HashtableTop (Univ Univ . -> . c)) (-lst c)]))]
+                               [(-HashTableTop (Univ Univ . -> . c)) (-lst c)]))]
 [hash-for-each (-poly (a b c) (cl-> [((-HT a b) (-> a b c)) -Void]
-                                    [(-HashtableTop (-> Univ Univ c)) -Void]))]
-[hash-count (-> -HashtableTop -Index)]
-[hash-empty? (-> -HashtableTop -Boolean)]
+                                    [(-HashTableTop (-> Univ Univ c)) -Void]))]
+[hash-count (-> -HashTableTop -Index)]
+[hash-empty? (-> -HashTableTop -Boolean)]
 [hash-keys (-poly (a b) (cl-> [((-HT a b)) (-lst a)]
-                              [(-HashtableTop) (-lst Univ)]))]
+                              [(-HashTableTop) (-lst Univ)]))]
 [hash-values (-poly (a b) (cl-> [((-HT a b)) (-lst b)]
-                                [(-HashtableTop) (-lst Univ)]))]
+                                [(-HashTableTop) (-lst Univ)]))]
 [hash->list (-poly (a b) (cl-> [((-HT a b)) (-lst (-pair a b))]
-                               [(-HashtableTop) (-lst (-pair Univ Univ))]))]
+                               [(-HashTableTop) (-lst (-pair Univ Univ))]))]
 
-[hash-copy (-poly (a b) (-> (-HT a b) (-HT a b)))]
+[hash-copy (-poly (a b) (cl-> [((-Immutable-HT a b)) (-Mutable-HT a b)]
+                              [((-Mutable-HT a b)) (-Mutable-HT a b)]
+                              [(-Mutable-HashTableTop) -Mutable-HashTableTop]
+                              [((-Weak-HT a b)) (-Weak-HT a b)]
+                              [(-Weak-HashTableTop) -Weak-HashTableTop]
+                              [((-HT a b)) (-HT a b)]))]
 [eq-hash-code (-> Univ -Fixnum)]
 [eqv-hash-code (-> Univ -Fixnum)]
 [equal-hash-code (-> Univ -Fixnum)]
@@ -993,23 +1004,62 @@
 [hash-iterate-first (-poly (a b)
                            (cl->*
                             ((-HT a b) . -> . (Un (-val #f) -Integer))
-                            (-> -HashtableTop (Un (-val #f) -Integer))))]
+                            (-> -HashTableTop (Un (-val #f) -Integer))))]
 [hash-iterate-next (-poly (a b)
                            (cl->*
                             ((-HT a b) -Integer . -> . (Un (-val #f) -Integer))
-                            (-> -HashtableTop -Integer (Un (-val #f) -Integer))))]
+                            (-> -HashTableTop -Integer (Un (-val #f) -Integer))))]
 [hash-iterate-key (-poly (a b)
                            (cl->* ((-HT a b) -Integer . -> . a)
-                                  (-> -HashtableTop -Integer Univ)))]
+                                  (-> -HashTableTop -Integer Univ)))]
 [hash-iterate-value (-poly (a b)
                            (cl->* ((-HT a b) -Integer . -> . b)
-                                  (-> -HashtableTop -Integer Univ)))]
+                                  (-> -HashTableTop -Integer Univ)))]
 [hash-iterate-pair (-poly (a b)
                            (cl->* ((-HT a b) -Integer . -> . (-pair a b))
-                                  (-> -HashtableTop -Integer Univ)))]
+                                  (-> -HashTableTop -Integer Univ)))]
 [hash-iterate-key+value (-poly (a b)
                            (cl->* ((-HT a b) -Integer . -> . (-values (list a b)))
-                                  (-> -HashtableTop -Integer (-values (list Univ Univ)))))]
+                                  (-> -HashTableTop -Integer (-values (list Univ Univ)))))]
+
+[unsafe-immutable-hash-iterate-first
+  (-poly (a b) ((-Immutable-HT a b) . -> . (Un (-val #f) -Integer)))]
+[unsafe-immutable-hash-iterate-next
+  (-poly (a b) ((-Immutable-HT a b) -Integer . -> . (Un (-val #f) -Integer)))]
+[unsafe-immutable-hash-iterate-key
+  (-poly (a b) ((-Immutable-HT a b) -Integer . -> . a))]
+[unsafe-immutable-hash-iterate-value
+  (-poly (a b) ((-Immutable-HT a b) -Integer . -> . b))]
+[unsafe-immutable-hash-iterate-pair
+  (-poly (a b) ((-Immutable-HT a b) -Integer . -> . (-pair a b)))]
+[unsafe-immutable-hash-iterate-key+value
+  (-poly (a b) ((-Immutable-HT a b) -Integer . -> . (-values (list a b))))]
+
+[unsafe-mutable-hash-iterate-first
+  (-poly (a b) ((-Mutable-HT a b) . -> . (Un (-val #f) -Integer)))]
+[unsafe-mutable-hash-iterate-next
+  (-poly (a b) ((-Mutable-HT a b) -Integer . -> . (Un (-val #f) -Integer)))]
+[unsafe-mutable-hash-iterate-key
+  (-poly (a b) ((-Mutable-HT a b) -Integer . -> . a))]
+[unsafe-mutable-hash-iterate-value
+  (-poly (a b) ((-Mutable-HT a b) -Integer . -> . b))]
+[unsafe-mutable-hash-iterate-pair
+  (-poly (a b) ((-Mutable-HT a b) -Integer . -> . (-pair a b)))]
+[unsafe-mutable-hash-iterate-key+value
+  (-poly (a b) ((-Mutable-HT a b) -Integer . -> . (-values (list a b))))]
+
+[unsafe-weak-hash-iterate-first
+  (-poly (a b) ((-Weak-HT a b) . -> . (Un (-val #f) -Integer)))]
+[unsafe-weak-hash-iterate-next
+  (-poly (a b) ((-Weak-HT a b) -Integer . -> . (Un (-val #f) -Integer)))]
+[unsafe-weak-hash-iterate-key
+  (-poly (a b) ((-Weak-HT a b) -Integer . -> . a))]
+[unsafe-weak-hash-iterate-value
+  (-poly (a b) ((-Weak-HT a b) -Integer . -> . b))]
+[unsafe-weak-hash-iterate-pair
+  (-poly (a b) ((-Weak-HT a b) -Integer . -> . (-pair a b)))]
+[unsafe-weak-hash-iterate-key+value
+  (-poly (a b) ((-Weak-HT a b) -Integer . -> . (-values (list a b))))]
 
 [make-custom-hash (->opt (-> Univ Univ Univ) (-> Univ -Nat) [(-> Univ -Nat)] Univ)]
 [make-immutable-custom-hash (->opt (-> Univ Univ Univ) (-> Univ -Nat) [(-> Univ -Nat)] Univ)]
@@ -1753,7 +1803,7 @@
         (-poly (a) (->opt (-Syntax a) [(one-of/c 'flip 'add 'remove)] (-Syntax a))))]
 
 [syntax-local-transforming-module-provides? (-> B)]
-[syntax-local-module-defined-identifiers (-> (-HT (Un (-val #f) -Int) (-lst (-Syntax Sym))))]
+[syntax-local-module-defined-identifiers (-> (-Immutable-HT (Un (-val #f) -Int) (-lst (-Syntax Sym))))]
 [syntax-local-module-required-identifiers (-> (-opt -Module-Path) (Un B -Int) (-lst (-pair (-opt -Int) (-lst (-Syntax Sym)))))]
 
 ;; Section 12.5
@@ -1768,7 +1818,7 @@
 
 ;; Section 12.8
 [syntax-recertify (-poly (a) (-> (-Syntax a) (-Syntax Univ) -Inspector Univ (-Syntax a)))]
-[syntax-debug-info (-poly (a) (->opt (-Syntax a) [(-opt -Integer) Univ] -HashtableTop))]
+[syntax-debug-info (-poly (a) (->opt (-Syntax a) [(-opt -Integer) Univ] -HashTableTop))]
 
 ;; Section 12.9
 [expand (-> Univ (-Syntax Univ))]
diff --git a/typed-racket-lib/typed-racket/base-env/base-special-env.rkt b/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
index 19a2aa50..015c9676 100644
--- a/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-special-env.rkt
@@ -174,67 +174,47 @@
   [(make-template-identifier 'default-in-hash 'racket/private/for)
    (-poly (a b)
           (cl-> [((-HT a b)) (-seq a b)]
-                [(-HashtableTop) (-seq Univ Univ)]))]
+                [(-HashTableTop) (-seq Univ Univ)]))]
   [(make-template-identifier 'default-in-hash-keys 'racket/private/for)
    (-poly (a b)
           (cl-> [((-HT a b)) (-seq a)]
-                [(-HashtableTop) (-seq Univ)]))]
+                [(-HashTableTop) (-seq Univ)]))]
   [(make-template-identifier 'default-in-hash-values 'racket/private/for)
    (-poly (a b)
           (cl-> [((-HT a b)) (-seq b)]
-                [(-HashtableTop) (-seq Univ)]))]
+                [(-HashTableTop) (-seq Univ)]))]
   [(make-template-identifier 'default-in-hash-pairs 'racket/private/for)
    (-poly (a b)
           (cl-> [((-HT a b)) (-seq (-pair a b))]
-                [(-HashtableTop) (-seq (-pair Univ Univ))]))]
+                [(-HashTableTop) (-seq (-pair Univ Univ))]))]
   [(make-template-identifier 'default-in-immutable-hash 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq a b)]
-                [(-HashtableTop) (-seq Univ Univ)]))]
+   (-poly (a b) (-> (-Immutable-HT a b) (-seq a b)))]
   [(make-template-identifier 'default-in-immutable-hash-keys 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq a)]
-                [(-HashtableTop) (-seq Univ)]))]
+   (-poly (a b) (-> (-Immutable-HT a b) (-seq a)))]
   [(make-template-identifier 'default-in-immutable-hash-values 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq b)]
-                [(-HashtableTop) (-seq Univ)]))]
+   (-poly (a b) (-> (-Immutable-HT a b) (-seq b)))]
   [(make-template-identifier 'default-in-immutable-hash-pairs 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq (-pair a b))]
-                [(-HashtableTop) (-seq (-pair Univ Univ))]))]
+   (-poly (a b) (-> (-Immutable-HT a b) (-seq (-pair a b))))]
   [(make-template-identifier 'default-in-mutable-hash 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq a b)]
-                [(-HashtableTop) (-seq Univ Univ)]))]
+   (-poly (a b) (-> (-Mutable-HT a b) (-seq a b)))]
   [(make-template-identifier 'default-in-mutable-hash-keys 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq a)]
-                [(-HashtableTop) (-seq Univ)]))]
+   (-poly (a b) (-> (-Mutable-HT a b) (-seq a)))]
   [(make-template-identifier 'default-in-mutable-hash-values 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq b)]
-                [(-HashtableTop) (-seq Univ)]))]
+   (-poly (a b) (-> (-Mutable-HT a b) (-seq b)))]
   [(make-template-identifier 'default-in-mutable-hash-pairs 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq (-pair a b))]
-                [(-HashtableTop) (-seq (-pair Univ Univ))]))]
+   (-poly (a b) (-> (-Mutable-HT a b) (-seq (-pair a b))))]
   [(make-template-identifier 'default-in-weak-hash 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq a b)]
-                [(-HashtableTop) (-seq Univ Univ)]))]
+   (-poly (a b) (-> (-Weak-HT a b) (-seq a b)))]
   [(make-template-identifier 'default-in-weak-hash-keys 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq a)]
-                [(-HashtableTop) (-seq Univ)]))]
+   (-poly (a b) (-> (-Weak-HT a b) (-seq a)))]
   [(make-template-identifier 'default-in-weak-hash-values 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq b)]
-                [(-HashtableTop) (-seq Univ)]))]
+   (-poly (a b) (-> (-Weak-HT a b) (-seq b)))]
   [(make-template-identifier 'default-in-weak-hash-pairs 'racket/private/for)
-   (-poly (a b)
-          (cl-> [((-HT a b)) (-seq (-pair a b))]
-                [(-HashtableTop) (-seq (-pair Univ Univ))]))]
+   (-poly (a b) (-> (-Weak-HT a b) (-seq (-pair a b))))]
+  [(make-template-identifier 'mutable? 'racket/private/for)
+   (-> Univ -Boolean)]
+  [(make-template-identifier 'not-weak? 'racket/private/for)
+   (-> -HashTableTop -Boolean)]
   ;; in-port
   [(make-template-identifier 'in-port 'racket/private/for)
    (-poly (a)
diff --git a/typed-racket-lib/typed-racket/base-env/base-types.rkt b/typed-racket-lib/typed-racket/base-env/base-types.rkt
index 16e21e70..8c08243e 100644
--- a/typed-racket-lib/typed-racket/base-env/base-types.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-types.rkt
@@ -120,7 +120,7 @@
 [ChannelTop -ChannelTop]
 [Async-ChannelTop -Async-ChannelTop]
 [VectorTop -VectorTop]
-[HashTableTop -HashtableTop]
+[HashTableTop -HashTableTop]
 [MPairTop -MPairTop]
 [Thread-CellTop -ThreadCellTop]
 [Prompt-TagTop -Prompt-TagTop]
@@ -170,7 +170,12 @@
 [ExtFlVector -ExtFlVector]
 [FxVector -FxVector]
 [Option (-poly (a) (-opt a))]
-[HashTable (-poly (a b) (-HT a b))]
+[Immutable-HashTable (-poly (a b) (-Immutable-HT a b))]
+[Mutable-HashTable (-poly (a b) (-Mutable-HT a b))]
+[Mutable-HashTableTop -Mutable-HashTableTop]
+[Weak-HashTable (-poly (a b) (-Weak-HT a b))]
+[Weak-HashTableTop -Weak-HashTableTop]
+[HashTable (-poly (a b) (Un (-Mutable-HT a b) (-Immutable-HT a b) (-Weak-HT a b)))]
 [Promise (-poly (a) (-Promise a))]
 [Pair (-poly (a b) (-pair a b))]
 [Boxof (-poly (a) (make-Box a))]
diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt
index 2cefb55e..d3e17b97 100644
--- a/typed-racket-lib/typed-racket/env/init-envs.rkt
+++ b/typed-racket-lib/typed-racket/env/init-envs.rkt
@@ -154,8 +154,12 @@
      `(-Param ,(type->sexp ty))]
     [(Param: in out)
      `(make-Param ,(type->sexp in) ,(type->sexp out))]
-    [(Hashtable: key val)
-     `(make-Hashtable ,(type->sexp key) ,(type->sexp val))]
+    [(Mutable-HashTable: key val)
+     `(make-Mutable-HashTable ,(type->sexp key) ,(type->sexp val))]
+    [(Immutable-HashTable: key val)
+     `(make-Immutable-HashTable ,(type->sexp key) ,(type->sexp val))]
+    [(Weak-HashTable: key val)
+     `(make-Weak-HashTable ,(type->sexp key) ,(type->sexp val))]
     [(Function: (list (arr: dom (Values: (list (Result: t
                                                         (PropSet: (TrueProp:)
                                                                   (TrueProp:))
diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index 82bcaef8..59a2bc71 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -663,8 +663,11 @@
            (for/or ([t (in-list (list -Byte -Index -NonNegFixnum -Nat))])
              (and (subtype S t) t)))
          (% cg type t*)]
-        [((Hashtable: k v) (Sequence: (list k* v*)))
-         (cgen/list context (list k v) (list k* v*))]
+        [((or (Mutable-HashTable: k v)
+              (Immutable-HashTable: k v)
+              (Weak-HashTable: k v))
+          (Sequence: (list k* v*)))
+         (% cset-meet (cg k k*) (cg v v*))]
         [((Set: t) (Sequence: (list t*)))
          (cg t t*)]
 
@@ -744,9 +747,17 @@
         [((CustodianBox: t) (Evt: t*)) (cg S t*)]
         [((Channel: t) (Evt: t*)) (cg t t*)]
         [((Async-Channel: t) (Evt: t*)) (cg t t*)]
-        ;; we assume all HTs are mutable at the moment
-        [((Hashtable: s1 s2) (Hashtable: t1 t2))
-         ;; for mutable hash tables, both are invariant
+        [((Immutable-HashTable: s1 s2)
+          (Immutable-HashTable: t1 t2))
+         ;; for immutable hash tables, covariant
+         (% cset-meet (cg s1 t1) (cg s2 t2))]
+        [((Mutable-HashTable: s1 s2)
+          (Mutable-HashTable: t1 t2))
+         ;; for mutable hash tables, invariant
+         (% cset-meet (cg/inv s1 t1) (cg/inv s2 t2))]
+        [((Weak-HashTable: s1 s2)
+          (Weak-HashTable: t1 t2))
+         ;; for mutable hash tables, invariant
          (% cset-meet (cg/inv s1 t1) (cg/inv s2 t2))]
         ;; syntax is covariant
         [((Syntax: s1) (Syntax: s2))
diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt
index 9f177d8b..a9866ca3 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -178,6 +178,7 @@
       typed-racket/utils/any-wrap typed-racket/utils/struct-type-c
       typed-racket/utils/opaque-object
       typed-racket/utils/evt-contract
+      typed-racket/utils/hash-contract
       typed-racket/utils/sealing-contract
       typed-racket/utils/promise-not-name-contract
       typed-racket/utils/simple-result-arrow
@@ -380,6 +381,20 @@
            (linear-exp/sc const
                           (for/hash ([(obj coeff) (in-terms terms)])
                             (values (obj->sc obj) coeff)))]))
+      (define (hash-types->sc hts)
+        (if (or (null? hts) (null? (cdr hts)))
+          #false ;; too few types, don't merge
+          (let-values ([(key-scs val-scs)
+                        (for/lists (ks vs)
+                                   ([ht (in-list hts)])
+                          (match ht
+                           [(or (Immutable-HashTable: k v)
+                                (Mutable-HashTable: k v)
+                                (Weak-HashTable: k v))
+                            (values (t->sc k) (t->sc v))]
+                           [_
+                            (raise-arguments-error 'hash-types->sc "expected hash/kv?" "given" ht "element of" hts)]))])
+            (hash/sc (apply or/sc key-scs) (apply or/sc val-scs)))))
       (define (only-untyped sc)
         (if (from-typed? typed-side)
             (and/sc sc any-wrap/sc)
@@ -450,8 +465,12 @@
             (apply or/sc (append other-scs (map t->sc (nbits->base-types nbits)))))]
        [(? Union? t)
         (match (normalize-type t)
-          [(Union: (? Bottom?) elems) (apply or/sc (map t->sc elems))]
-          [(Union: base elems) (apply or/sc (t->sc base) (map t->sc elems))]
+          [(Union-all: elems)
+           (define-values [hash-elems other-elems] (partition hash/kv? elems))
+           (define maybe-hash/sc (hash-types->sc hash-elems))
+           (if maybe-hash/sc
+             (apply or/sc maybe-hash/sc (map t->sc other-elems))
+             (apply or/sc (map t->sc elems)))]
           [t (t->sc t)])]
        [(Intersection: ts raw-prop)
         (define-values (impersonators chaperones others)
@@ -526,7 +545,6 @@
        [(BoxTop:) (only-untyped box?/sc)]
        [(ChannelTop:) (only-untyped channel?/sc)]
        [(Async-ChannelTop:) (only-untyped async-channel?/sc)]
-       [(HashtableTop:) (only-untyped hash?/sc)]
        [(MPairTop:) (only-untyped mpair?/sc)]
        [(ThreadCellTop:) (only-untyped thread-cell?/sc)]
        [(Prompt-TagTop:) (only-untyped prompt-tag?/sc)]
@@ -690,10 +708,18 @@
        [(Syntax: (? Base:Symbol?)) identifier?/sc]
        [(Syntax: t)
         (syntax/sc (t->sc t))]
-       [(Param: in out) 
+       [(Param: in out)
         (parameter/sc (t->sc in) (t->sc out))]
-       [(Hashtable: k v)
-        (hash/sc (t->sc k) (t->sc v))]
+       [(Mutable-HashTable: k v)
+        (mutable-hash/sc (t->sc k) (t->sc v))]
+       [(Mutable-HashTableTop:)
+        (only-untyped mutable-hash?/sc)]
+       [(Immutable-HashTable: k v)
+        (immutable-hash/sc (t->sc k) (t->sc v))]
+       [(Weak-HashTable: k v)
+        (weak-hash/sc (t->sc k) (t->sc v))]
+       [(Weak-HashTableTop:)
+        (only-untyped weak-hash?/sc)]
        [(Channel: t)
         (channel/sc (t->sc t))]
        [(Evt: t)
@@ -920,6 +946,18 @@
      (t:subtype -Boolean t)]
     [_ #f]))
 
+;; hash/kv? : Type -> Boolean
+;; True if given type is a HashTable with known key and value types
+;;  aka a "non-Top" HashTable type
+(define (hash/kv? ty)
+  (match ty
+   [(or (Immutable-HashTable: k v)
+        (Mutable-HashTable: k v)
+        (Weak-HashTable: k v))
+    #true]
+   [_
+    #false]))
+
 (module predicates racket/base
   (require racket/extflonum (only-in racket/contract/base >=/c <=/c))
   (provide nonnegative? nonpositive?
diff --git a/typed-racket-lib/typed-racket/rep/type-mask.rkt b/typed-racket-lib/typed-racket/rep/type-mask.rkt
index 260cd52f..d95757ca 100644
--- a/typed-racket-lib/typed-racket/rep/type-mask.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-mask.rkt
@@ -130,7 +130,9 @@
  mask:pair
  mask:mpair
  mask:vector
- mask:hash
+ mask:mutable-hash
+ mask:immutable-hash
+ mask:weak-hash
  mask:box
  mask:channel
  mask:thread-cell
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 04b802f9..4df5eb1b 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -314,16 +314,25 @@
   [#:mask mask:set])
 
 ;;------------
-;; Hashtable
+;; HashTable
 ;;------------
 
-(def-type HashtableTop ()
-  [#:mask mask:hash]
-  [#:singleton -HashtableTop])
+(def-structural Immutable-HashTable ([key #:covariant] [value #:covariant])
+  [#:mask mask:immutable-hash])
 
-;; TODO separate mutable/immutable Hashtables
-(def-structural Hashtable ([key #:invariant] [value #:invariant])
-  [#:mask mask:hash])
+(def-type Mutable-HashTableTop ()
+  [#:mask mask:mutable-hash]
+  [#:singleton -Mutable-HashTableTop])
+
+(def-structural Mutable-HashTable ([key #:invariant] [value #:invariant])
+  [#:mask mask:mutable-hash])
+
+(def-type Weak-HashTableTop ()
+  [#:mask mask:weak-hash]
+  [#:singleton -Weak-HashTableTop])
+
+(def-structural Weak-HashTable ([key #:invariant] [value #:invariant])
+  [#:mask mask:weak-hash])
 
 
 ;;------
diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt
index 77dee79c..e9a117f1 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt
@@ -25,6 +25,11 @@
 (define vector?/sc (flat/sc #'vector?))
 
 (define hash?/sc (flat/sc #'hash?))
+(define mutable-hash?/sc (and/sc hash?/sc
+                                 (flat/sc #'(λ (h) (not (immutable? h))))
+                                 (flat/sc #'(λ (h) (not (hash-weak? h))))))
+(define immutable-hash?/sc (and/sc hash?/sc (flat/sc #'immutable?)))
+(define weak-hash?/sc (and/sc hash?/sc (flat/sc #'hash-weak?)))
 (define empty-hash/sc (and/sc hash?/sc (flat/sc #'(λ (h) (zero? (hash-count h))))))
 
 (define channel?/sc (flat/sc #'channel?))
diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt
index 48bc3283..4bc2ec1d 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt
@@ -17,6 +17,7 @@
                        racket/sequence
                        racket/promise
                        "../../utils/evt-contract.rkt"
+                       "../../utils/hash-contract.rkt"
                        "../../utils/promise-not-name-contract.rkt")
          racket/contract
          racket/async-channel)
@@ -160,10 +161,13 @@
   ((promise/sc (#:covariant)) promise-not-name/c #:chaperone)
   ((syntax/sc (#:covariant #:flat)) syntax/c #:flat)
   ((hash/sc (#:invariant #:flat) (#:invariant)) hash/c #:chaperone)
+  ((mutable-hash/sc (#:invariant #:flat) (#:invariant)) mutable-hash/c #:chaperone)
+  ((immutable-hash/sc (#:covariant #:flat) (#:covariant)) immutable-hash/c #:flat)
+  ((weak-hash/sc (#:invariant #:flat) (#:invariant)) weak-hash/c #:chaperone)
   ((box/sc (#:invariant)) box/c #:chaperone)
   ((parameter/sc (#:contravariant) (#:covariant)) parameter/c #:chaperone)
   ((sequence/sc . (#:covariant)) sequence/c #:impersonator)
   ((channel/sc . (#:invariant)) channel/c #:chaperone)
   ((continuation-mark-key/sc (#:invariant)) continuation-mark-key/c #:chaperone)
   ((evt/sc (#:covariant)) tr:evt/c #:chaperone)
-  ((async-channel/sc (#:invariant)) async-channel/c #:chaperone))
\ No newline at end of file
+  ((async-channel/sc (#:invariant)) async-channel/c #:chaperone))
diff --git a/typed-racket-lib/typed-racket/static-contracts/optimize.rkt b/typed-racket-lib/typed-racket/static-contracts/optimize.rkt
index d2614981..d3618f61 100644
--- a/typed-racket-lib/typed-racket/static-contracts/optimize.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/optimize.rkt
@@ -48,6 +48,9 @@
     [(syntax/sc: (any/sc:)) syntax?/sc]
     [(promise/sc: (any/sc:)) promise?/sc]
     [(hash/sc: (any/sc:) (any/sc:)) hash?/sc]
+    [(mutable-hash/sc: (any/sc:) (any/sc:)) mutable-hash?/sc]
+    [(immutable-hash/sc: (any/sc:) (any/sc:)) immutable-hash?/sc]
+    [(weak-hash/sc: (any/sc:) (any/sc:)) weak-hash?/sc]
 
     ;; or/sc cases
     [(or/sc: scs ...)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
index 588f7d7d..e6e0dea9 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
@@ -409,21 +409,46 @@
        [(Box: t) (-box (check-below (find-stx-type x t) t))]
        [_ (-box (generalize (find-stx-type x)))])]
     [(? hash? h)
-     (match (and expected (resolve (intersect expected -HashtableTop)))
-       [(Hashtable: kt vt)
-        (define kts (hash-map h (lambda (x y) (find-stx-type x kt))))
-        (define vts (hash-map h (lambda (x y) (find-stx-type y vt))))
-        (make-Hashtable
-         (check-below (apply Un kts) kt)
-         (check-below (apply Un vts) vt))]
-       [_ (make-Hashtable (generalize (apply Un (map find-stx-type (hash-keys h))))
-                          (generalize (apply Un (map find-stx-type (hash-values h)))))])]
+     (cond
+      [(immutable? h)
+       (match (and expected (resolve (intersect expected (-Immutable-HT Univ Univ))))
+        [(Immutable-HashTable: k v)
+         (value->HT/find-stx-type h -Immutable-HT k v)]
+        [_
+         (value->HT/find-stx-type h -Immutable-HT)])]
+      [(hash-weak? h)
+       (match (and expected (resolve (intersect expected (-Weak-HT Univ Univ))))
+        [(Weak-HashTable: k v)
+         (value->HT/find-stx-type h -Weak-HT k v)]
+        [_
+         (value->HT/find-stx-type h -Weak-HT)])]
+      [else
+       (match (and expected (resolve (intersect expected (-Mutable-HT Univ Univ))))
+        [(Mutable-HashTable: k v)
+         (value->HT/find-stx-type h -Mutable-HT k v)]
+        [_
+         (value->HT/find-stx-type h -HT)])])]
     [(? prefab-struct-key)
      ;; FIXME is there a type for prefab structs?
      Univ]
     [_ Univ]))
 
-
+;; value->HT/find-stx-type : hash? (-> type? type? type?) -> type?
+;;                         : hash? (-> type? type? type?) type? type? -> type?
+;; Build a HashTable type from a value, type constructor, and (optionally)
+;;  upper bounds on the key and value types.
+(define value->HT/find-stx-type
+  (case-lambda
+   [(h tycon expected-kt expected-vt)
+    (let* ([kts (hash-map h (lambda (x y) (find-stx-type x expected-kt)))]
+           [vts (hash-map h (lambda (x y) (find-stx-type y expected-vt)))]
+           [kt (apply Un kts)]
+           [vt (apply Un vts)])
+      (tycon (check-below kt expected-kt) (check-below vt expected-vt)))]
+   [(h tycon)
+    (let ([kt (generalize (apply Un (map find-stx-type (hash-keys h))))]
+          [vt (generalize (apply Un (map find-stx-type (hash-values h))))])
+      (tycon kt vt))]))
 
 ;; adds linear info for the following operations:
 ;; + * < <= = >= >
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
index fe6c19d6..e1c16fb0 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt
@@ -134,18 +134,20 @@
                                       (-vec-len-of (-id-path v))))
          vec-ty)]
     [(~var i (3d hash?))
-     (match (and expected (resolve (intersect expected -HashtableTop)))
-       [(Hashtable: k v)
-        (let* ([h (syntax-e #'i)]
-               [ks (hash-map h (lambda (x y) (tc-literal x k)))]
-               [vs (hash-map h (lambda (x y) (tc-literal y v)))])
-          (make-Hashtable
-            (check-below (apply Un ks) k)
-            (check-below (apply Un vs) v)))]
-       [_ (let* ([h (syntax-e #'i)]
-                 [ks (hash-map h (lambda (x y) (tc-literal x)))]
-                 [vs (hash-map h (lambda (x y) (tc-literal y)))])
-            (make-Hashtable (generalize (apply Un ks)) (generalize (apply Un vs))))])]
+     (let ([h (syntax-e #'i)])
+       (match (and expected (resolve (intersect expected (-Immutable-HT Univ Univ))))
+        [(Immutable-HashTable: k v)
+         (let* ([kts (hash-map h (lambda (x y) (tc-literal x k)))]
+                [vts (hash-map h (lambda (x y) (tc-literal y v)))]
+                [kt (apply Un kts)]
+                [vt (apply Un vts)])
+           (-Immutable-HT (check-below kt k) (check-below vt v)))]
+        [_
+         (let* ([kts (hash-map h (lambda (x y) (tc-literal x)))]
+                [vts (hash-map h (lambda (x y) (tc-literal y)))]
+                [kt (generalize (apply Un kts))]
+                [vt (generalize (apply Un vts))])
+           (-Immutable-HT kt vt))]))]
     [(~var i (3d prefab-struct-key))
      (tc-prefab (syntax-e #'i) expected)]
     [_ Univ]))
diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt
index dd5d8965..9a207d0f 100644
--- a/typed-racket-lib/typed-racket/types/abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/abbrev.rkt
@@ -118,7 +118,11 @@
 (define/decl -Sexp (-Sexpof (Un)))
 (define Syntax-Sexp (-Sexpof Any-Syntax))
 (define Ident (-Syntax -Symbol))
-(define -HT make-Hashtable)
+(define -Mutable-HT make-Mutable-HashTable)
+(define -Immutable-HT make-Immutable-HashTable)
+(define -Weak-HT make-Weak-HashTable)
+(define (-HT a b) (Un (-Mutable-HT a b) (-Immutable-HT a b) (-Weak-HT a b)))
+(define make-HashTable -HT)
 (define/decl -Port (Un -Output-Port -Input-Port))
 (define/decl -SomeSystemPath (Un -Path -OtherSystemPath))
 (define/decl -Pathlike (Un -String -Path))
diff --git a/typed-racket-lib/typed-racket/types/base-abbrev.rkt b/typed-racket-lib/typed-racket/types/base-abbrev.rkt
index 76a1f6e6..aa379cf6 100644
--- a/typed-racket-lib/typed-racket/types/base-abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/base-abbrev.rkt
@@ -97,6 +97,10 @@
 (define (-AnyValues f) (make-AnyValues f))
 (define/decl ManyUniv (make-AnyValues -tt))
 
+(define/decl -HashTableTop (Un (make-Immutable-HashTable Univ Univ)
+                               -Mutable-HashTableTop
+                               -Weak-HashTableTop))
+
 ;; Function types
 (define/cond-contract (make-arr* dom rng
                                  #:rest [rest #f] #:drest [drest #f] #:kws [kws null]
diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt
index 5fb1c4d1..eb16c3a5 100644
--- a/typed-racket-lib/typed-racket/types/overlap.rkt
+++ b/typed-racket-lib/typed-racket/types/overlap.rkt
@@ -104,7 +104,11 @@
    [((Sequence: _) (Val-able: v)) #:no-order (sequence? v)]
    ;; hash tables are two-valued sequences
    [((Sequence: (or (list _) (list _ _ _ ...)))
-     (or (? Hashtable?) (? HashtableTop?)))
+     (or (? Mutable-HashTable?)
+         (? Mutable-HashTableTop?)
+         (? Immutable-HashTable?)
+         (? Weak-HashTable?)
+         (? Weak-HashTableTop?)))
     #:no-order
     #f]
    ;; these are single-valued sequences
@@ -125,7 +129,11 @@
     #:no-order
     #f]
    [((Val-able: (not (? hash?)))
-     (or (? Hashtable?) (? HashtableTop?)))
+     (or (? Mutable-HashTable?)
+         (? Mutable-HashTableTop?)
+         (? Immutable-HashTable?)
+         (? Weak-HashTable?)
+         (? Weak-HashTableTop?)))
     #:no-order
     #f]
    [((Struct: n _ flds _ _ _)
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 0b886784..1779604a 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -529,7 +529,6 @@
     [(Async-ChannelTop:) 'Async-ChannelTop]
     [(ThreadCellTop:) 'ThreadCellTop]
     [(VectorTop:) 'VectorTop]
-    [(HashtableTop:) 'HashTableTop]
     [(MPairTop:) 'MPairTop]
     [(Prompt-TagTop:) 'Prompt-TagTop]
     [(Continuation-Mark-KeyTop:) 'Continuation-Mark-KeyTop]
@@ -594,7 +593,11 @@
      (if (equal? in out)
          `(Parameterof ,(t->s in))
          `(Parameterof ,(t->s in) ,(t->s out)))]
-    [(Hashtable: k v) `(HashTable ,(t->s k) ,(t->s v))]
+    [(Mutable-HashTable: k v) `(Mutable-HashTable ,(t->s k) ,(t->s v))]
+    [(Mutable-HashTableTop:) 'Mutable-HashTableTop]
+    [(Immutable-HashTable: k v) `(Immutable-HashTable ,(t->s k) ,(t->s v))]
+    [(Weak-HashTable: k v) `(Weak-HashTable ,(t->s k) ,(t->s v))]
+    [(Weak-HashTableTop:) 'Weak-HashTableTop]
     [(Continuation-Mark-Keyof: rhs)
      `(Continuation-Mark-Keyof ,(t->s rhs))]
     [(Prompt-Tagof: body handler)
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index 495864ca..93da56f6 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -649,17 +649,6 @@
    (match t2
      [(Future: elem2) (subtype* A elem1 elem2)]
      [_ (continue<: A t1 t2 obj)])]
-  [(case: Hashtable (Hashtable: key1 val1))
-   (match t2
-     [(? HashtableTop?) A]
-     [(Hashtable: key2 val2) (subtype-seq A
-                                          (type≡? key1 key2)
-                                          (type≡? val1 val2))]
-     [(Sequence: (list key2 val2))
-      (subtype-seq A
-                   (subtype* key1 key2)
-                   (subtype* val1 val2))]
-     [_ (continue<: A t1 t2 obj)])]
   [(case: HeterogeneousVector (HeterogeneousVector: elems1))
    (match t2
      [(VectorTop:) A]
@@ -682,6 +671,20 @@
                  #:break (not A))
         (subtype* A elem1 seq-t))]
      [_ (continue<: A t1 t2 obj)])]
+  [(case: Immutable-HashTable (Immutable-HashTable: key1 val1))
+   (match t2
+    [(Immutable-HashTable: key2 val2)
+     (subtype-seq A
+                  (subtype* key1 key2)
+                  (subtype* val1 val2))]
+    [(Sequence: (list key2 val2))
+     (subtype-seq A
+                  (subtype* key1 key2)
+                  (subtype* val1 val2))]
+    [(or (Mutable-HashTableTop:) (Mutable-HashTable: _ _)
+         (Weak-HashTableTop:) (Weak-HashTable: _ _))
+     #false]
+    [_ (continue<: A t1 t2 obj)])]
   [(case: Instance (Instance: inst-t1))
    (cond
      [(resolvable? inst-t1)
@@ -769,6 +772,20 @@
        (let ([t1 (unfold t1)])
          ;; check needed for if a name that hasn't been resolved yet
          (and (Type? t1) (subtype* A t1 t2)))))]
+  [(case: Mutable-HashTable (Mutable-HashTable: key1 val1))
+   (match t2
+    [(Mutable-HashTableTop:) A]
+    [(Mutable-HashTable: key2 val2)
+     (subtype-seq A
+                  (type≡? key1 key2)
+                  (type≡? val1 val2))]
+    [(Sequence: (list key2 val2))
+     (subtype-seq A
+                  (subtype* key1 key2)
+                  (subtype* val1 val2))]
+    [(or (Weak-HashTableTop:) (Weak-HashTable: _ _) (Immutable-HashTable: _ _))
+     #false]
+    [_ (continue<: A t1 t2 obj)])]
   [(case: Name _)
    (match* (t1 t2)
      ;; Avoid resolving things that refer to different structs.
@@ -1005,4 +1022,19 @@
      [(? Weak-BoxTop?) A]
      [(Weak-Box: elem2) (type≡? A elem1 elem2)]
      [_ (continue<: A t1 t2 obj)])]
+  [(case: Weak-HashTable (Weak-HashTable: key1 val1))
+   (match t2
+    [(Weak-HashTableTop:) A]
+    [(Weak-HashTable: key2 val2)
+     (subtype-seq A
+                  (type≡? key1 key2)
+                  (type≡? val1 val2))]
+    [(Sequence: (list key2 val2))
+     (subtype-seq A
+                  (subtype* key1 key2)
+                  (subtype* val1 val2))]
+    [(or (Mutable-HashTableTop:) (Mutable-HashTable: _ _)
+         (Immutable-HashTable: _ _))
+     #false]
+    [_ (continue<: A t1 t2 obj)])]
   [else: (continue<: A t1 t2 obj)])
diff --git a/typed-racket-lib/typed-racket/utils/hash-contract.rkt b/typed-racket-lib/typed-racket/utils/hash-contract.rkt
new file mode 100644
index 00000000..550d5a26
--- /dev/null
+++ b/typed-racket-lib/typed-racket/utils/hash-contract.rkt
@@ -0,0 +1,8 @@
+#lang racket/base
+
+(require racket/contract)
+(provide mutable-hash/c immutable-hash/c weak-hash/c)
+
+(define (mutable-hash/c k v) (and/c hash? (not/c hash-weak?) (hash/c k v #:immutable #f)))
+(define (immutable-hash/c k v) (hash/c k v #:immutable #t))
+(define (weak-hash/c k v) (and/c hash? hash-weak? (hash/c k v #:immutable #f)))
diff --git a/typed-racket-more/typed/private/framework-types.rkt b/typed-racket-more/typed/private/framework-types.rkt
index 4725b953..eb5b0512 100644
--- a/typed-racket-more/typed/private/framework-types.rkt
+++ b/typed-racket-more/typed/private/framework-types.rkt
@@ -1000,8 +1000,8 @@
 (define-type Keymap:Aug-Keymap<%>
   (Class #:implements Keymap%
          [get-chained-keymaps (-> (Listof (Instance Keymap%)))]
-         [get-map-function-table (-> (HashTable String String))]
-         [get-map-function-table/ht ((HashTable String String) -> (HashTable String String))]))
+         [get-map-function-table (-> (Mutable-HashTable Symbol String))]
+         [get-map-function-table/ht ((HashTable Symbol String) -> (Mutable-HashTable Symbol String))]))
 
 (define-type Keymap:Aug-Keymap-Mixin
   (All (r #:row)
diff --git a/typed-racket-test/fail/bad-immutable-hash-ref.rkt b/typed-racket-test/fail/bad-immutable-hash-ref.rkt
new file mode 100644
index 00000000..d47cc440
--- /dev/null
+++ b/typed-racket-test/fail/bad-immutable-hash-ref.rkt
@@ -0,0 +1,16 @@
+#lang typed/scheme
+
+(: table (Immutable-HashTable Integer (-> Integer)))
+(define table
+  (make-immutable-hash null))
+
+(: lookup (Integer -> Integer))
+(define (lookup n)
+
+  (: thunk (-> Integer))
+  (define thunk
+    (hash-ref table n (lambda () n)))
+
+  (thunk))
+
+(lookup 1)
diff --git a/typed-racket-test/gui/succeed/pr390.rkt b/typed-racket-test/gui/succeed/pr390.rkt
new file mode 100644
index 00000000..8178dcd9
--- /dev/null
+++ b/typed-racket-test/gui/succeed/pr390.rkt
@@ -0,0 +1,19 @@
+#lang typed/racket/base
+
+;; Test types for framework `get-map-function-table/ht`
+
+(require typed/framework typed/racket/class)
+
+(: km (Instance Keymap:Aug-Keymap<%>))
+(define km
+  (cast (keymap:get-global) (Instance Keymap:Aug-Keymap<%>)))
+
+(void
+  (ann
+    (send km get-map-function-table)
+    (HashTable Symbol String))
+
+  ;; Inserts bindings into argument
+  (ann
+    (send km get-map-function-table/ht (ann (make-hash) (HashTable Symbol String)))
+    (Mutable-HashTable Symbol String)))
diff --git a/typed-racket-test/succeed/for-hash.rkt b/typed-racket-test/succeed/for-hash.rkt
index 6e15d463..fb7c74ea 100644
--- a/typed-racket-test/succeed/for-hash.rkt
+++ b/typed-racket-test/succeed/for-hash.rkt
@@ -8,6 +8,12 @@
             ((a (list 1 2 3)))
   (values a 'a)))
 
+(check-pred
+ immutable?
+ (for/hash: : (Immutable-HashTable Integer Symbol)
+            ((a (list 1 2 3)))
+  (values a 'a)))
+
 (check-pred
  hash?
  (for/hash: : (HashTable Integer Symbol)
@@ -15,6 +21,13 @@
              (b '(a b c)))
   (values a b)))
 
+(check-pred
+ immutable?
+ (for/hash: : (Immutable-HashTable Integer Symbol)
+            ((a (list 1 2 3))
+             (b '(a b c)))
+  (values a b)))
+
 (check-pred
  hash?
  (for*/hasheq: : (HashTable Integer Symbol)
@@ -22,6 +35,12 @@
               (b '(a b c)))
   (values a b)))
 
+(check-pred
+ hash?
+ (for*/hasheq: : (Immutable-HashTable Integer Symbol)
+             ((a (list 1 2 3))
+              (b '(a b c)))
+  (values a b)))
 
 (check-pred
  hash-eq?
@@ -43,6 +62,12 @@
               (b '(a b c)))
   (values a b)))
 
+(check-pred
+ hash-eq?
+ (for*/hasheq: : (Immutable-HashTable Integer Symbol)
+             ((a (list 1 2 3))
+              (b '(a b c)))
+  (values a b)))
 
 (check-pred
  hash-eqv?
@@ -64,14 +89,22 @@
               (b '(a b c)))
   (values a b)))
 
-
+(check-pred
+ hash-eqv?
+ (for*/hasheqv: : (Immutable-HashTable Integer Symbol)
+             ((a (list 1 2 3))
+              (b '(a b c)))
+  (values a b)))
 
 (for*/hash: : (HashTable Number Number)
             ((v : Number '(1 2 3))
              (x : Number '(4 5 6)))
      (values v x))
 
-
+(for*/hash: : (Immutable-HashTable Number Number)
+            ((v : Number '(1 2 3))
+             (x : Number '(4 5 6)))
+     (values v x))
 
 (for/hash: : (HashTable Symbol Symbol)
     ((v : Symbol '(a b c)))
@@ -80,3 +113,7 @@
 (for/hash: : (HashTable Symbol Symbol)
     ([(k b) (in-hash (make-immutable-hash '((a . a) (b . b))))])
   (values k b))
+
+(for/hash: : (Immutable-HashTable Symbol Symbol)
+    ([(k b) (in-hash (make-immutable-hash '((a . a) (b . b))))])
+  (values k b))
diff --git a/typed-racket-test/succeed/for.rkt b/typed-racket-test/succeed/for.rkt
index d5329652..ffd77813 100644
--- a/typed-racket-test/succeed/for.rkt
+++ b/typed-racket-test/succeed/for.rkt
@@ -7,6 +7,10 @@
       #t
       (error (format "Check (~a ~a ~a) failed" f a b))))
 
+(: sort-by-first-key (-> (Listof (Listof (Pairof Symbol Any))) (Listof (Listof (Pairof Symbol Any)))))
+(define (sort-by-first-key kv*)
+  ((inst sort (Listof (Pairof Symbol Any)) Symbol) kv* symbol<? #:key caar))
+
 ;; Each test is there twice, once with the type annotation before the for
 ;; clauses, and once after.
 
@@ -409,6 +413,52 @@
 (check equal?
        (for/hasheq: ([k (list 2 3 4)]) : (HashTable Integer String) (values k "val"))
        #hasheq((2 . "val") (3 . "val") (4 . "val")))
+(check equal?
+       (for/hasheq: : (Immutable-HashTable Integer String) ([k (list 2 3 4)]) (values k "val"))
+       #hasheq((2 . "val") (3 . "val") (4 . "val")))
+
+(check equal?
+       (let ([ht #hash((a . 1) (b . 2))])
+         (for/list : (Listof (Listof (Pairof Symbol Integer)))
+                   ([(k1 v1) (in-hash ht)]
+                    [k2 (in-hash-keys ht)]
+                    [v2 (in-hash-values ht)]
+                    [k3+v3 (in-hash-pairs ht)])
+           (list (cons k1 v1) (cons k2 v2) k3+v3)))
+       '(((a . 1) (a . 1) (a . 1)) ((b . 2) (b . 2) (b . 2))))
+
+(check equal?
+       (let ([ht #hash((a . 1) (b . 2))])
+         (sort-by-first-key
+           (for/list : (Listof (Listof (Pairof Symbol Integer)))
+                     ([(k1 v1) (in-hash ht)]
+                      [k2 (in-hash-keys ht)]
+                      [v2 (in-hash-values ht)]
+                      [k3+v3 (in-hash-pairs ht)])
+             (list (cons k1 v1) (cons k2 v2) k3+v3))))
+       '(((a . 1) (a . 1) (a . 1)) ((b . 2) (b . 2) (b . 2))))
+
+(check equal?
+       (let ([ht  (make-hash '((a . 1) (b . 2)))])
+         (sort-by-first-key
+           (for/list : (Listof (Listof (Pairof Symbol Integer)))
+                     ([(k1 v1) (in-mutable-hash ht)]
+                      [k2 (in-mutable-hash-keys ht)]
+                      [v2 (in-mutable-hash-values ht)]
+                      [k3+v3 (in-mutable-hash-pairs ht)])
+             (list (cons k1 v1) (cons k2 v2) k3+v3))))
+       '(((a . 1) (a . 1) (a . 1)) ((b . 2) (b . 2) (b . 2))))
+
+(check equal?
+       (let ([ht : (Weak-HashTable Symbol Integer) (make-weak-hash '((a . 1) (b . 2)))])
+         (sort-by-first-key
+           (for/list : (Listof (Listof (Pairof Symbol Integer)))
+                     ([(k1 v1) (in-weak-hash ht)]
+                      [k2 (in-weak-hash-keys ht)]
+                      [v2 (in-weak-hash-values ht)]
+                      [k3+v3 (in-weak-hash-pairs ht)])
+             (list (cons k1 v1) (cons k2 v2) k3+v3))))
+       '(((a . 1) (a . 1) (a . 1)) ((b . 2) (b . 2) (b . 2))))
 
 (check equal?
        (for/vector: ([i : Natural (in-range 3)]) 5)
diff --git a/typed-racket-test/succeed/hash-literal.rkt b/typed-racket-test/succeed/hash-literal.rkt
index 1c24f8e0..16290f16 100644
--- a/typed-racket-test/succeed/hash-literal.rkt
+++ b/typed-racket-test/succeed/hash-literal.rkt
@@ -2,3 +2,6 @@
 
 (define: x : (HashTable String String) #hash())
 (ann #hash() (HashTable String String))
+
+(define: x2 : (Immutable-HashTable String String) #hash())
+(ann #hash() (Immutable-HashTable String String))
diff --git a/typed-racket-test/succeed/pr12678.rkt b/typed-racket-test/succeed/pr12678.rkt
index d83186f3..10062682 100644
--- a/typed-racket-test/succeed/pr12678.rkt
+++ b/typed-racket-test/succeed/pr12678.rkt
@@ -7,3 +7,12 @@
     ([memo : (HashTable Natural String)  (make-immutable-hash empty)])
     ([i : Natural  (in-naturals)] [str : String  (in-list strs)])
   (hash-set memo i str))
+
+(let () ;;bg: same code should work with Immutable-Hash type
+  (define: memo2 : (Immutable-HashTable Natural String)  (make-immutable-hash empty))
+  (define strs2 '("Hello" "Goodbye"))
+
+  (for/fold: : (Immutable-HashTable Natural String)
+      ([memo2 : (Immutable-HashTable Natural String)  (make-immutable-hash empty)])
+      ([i : Natural  (in-naturals)] [str : String  (in-list strs2)])
+    (hash-set memo2 i str)))
diff --git a/typed-racket-test/succeed/pr241-variation-5.rkt b/typed-racket-test/succeed/pr241-variation-5.rkt
index ac9279cd..3b4db933 100644
--- a/typed-racket-test/succeed/pr241-variation-5.rkt
+++ b/typed-racket-test/succeed/pr241-variation-5.rkt
@@ -168,6 +168,7 @@
  [Log-Receiver (make-log-receiver (current-logger) 'info) choice-evt]
  [Logger (current-logger) (lambda (l) (log-level? l 'info))]
  [Module-Path "hello.rkt" module-path?]
+ [Mutable-HashTableTop (make-hash) (lambda (h) (hash-ref h 'a #f))]
  [Null '() length]
  [Output-Port (current-output-port) port?]
  [PRegexp #px"\\d\\d" (lambda (p) (regexp-match? p "013a"))]
@@ -192,6 +193,7 @@
  [UDP-Socket (udp-open-socket) udp-close]
  [VectorTop (vector 1 2 3) (lambda (x) (vector-ref x 0))]
  [Void (void) void?]
+ [Weak-HashTableTop (make-weak-hash) (lambda (h) (hash-ref h 'a #f))]
  [Will-Executor (make-will-executor) choice-evt]
 ))
 
@@ -247,7 +249,14 @@
   [Boxof (Boxof Integer) (box 3) (lambda (v) (add1 (unbox v)))]
   [Channelof (Channelof Integer) (make-channel) channel-try-get]
   [HashTable (HashTable Symbol String) (hash) (lambda (h) (hash-ref h 'a #f))]
+  [Immutable-HashTable (Immutable-HashTable Symbol String) (hash) (lambda (h) (hash-set h 'a "a"))]
   [Listof (Listof Integer) (list 1) (lambda (xs) (add1 (car xs)))]
+  [Mutable-HashTable (Mutable-HashTable Symbol String) (make-hash)
+   (lambda (h)
+     (hash-ref h 'a #f)
+     (with-handlers ([exn:fail:contract? void])
+       (hash-set! h 'a "a")
+       (error 'pr241 "mutable hashtable ~a incorrectly allowed to be set!" h)))]
   [Option (Option Integer) 1 add1]
   [Pair (Pair Integer Boolean) (cons 1 #t) (lambda (v) (add1 (car v)))]
   [Pairof (Pairof Integer Boolean) (cons 1 #f) (lambda (v) (add1 (car v)))]
@@ -255,6 +264,12 @@
   [Sequenceof (Sequenceof Natural) '(1 2 3) sequence->list]
   [Setof (Setof Integer) (set) set-empty?]
   [Sexpof (Sexpof Integer) (syntax->datum #'(1 2 3)) (lambda (xs) (add1 (car xs)))]
+  [Weak-HashTable (Weak-HashTable Symbol String) (make-weak-hash)
+   (lambda (h)
+     (hash-ref h 'a #f)
+     (with-handlers ([exn:fail:contract? void])
+       (hash-set! h 'a "a")
+       (error 'pr241 "weak hashtable ~a incorrectly allowed to be set!" h)))]
   [Vectorof (Vectorof Integer) (vector 1) (lambda (v) (add1 (vector-ref v 0)))]
 ))
 
diff --git a/typed-racket-test/succeed/pr390-variation-1.rkt b/typed-racket-test/succeed/pr390-variation-1.rkt
new file mode 100644
index 00000000..6e790eaa
--- /dev/null
+++ b/typed-racket-test/succeed/pr390-variation-1.rkt
@@ -0,0 +1,15 @@
+#lang typed/racket
+
+;; Reported by Matthew Eric Basset
+;; https://groups.google.com/forum/#!searchin/racket-users/weirdness%7Csort:date/racket-users/g6UmwgZWtzE/1czSRfk2AgAJ
+
+;; Works "as expected" on 6.5
+(void
+  (ann (hash 'a 1 'b "cat") (HashTable Any Any)))
+
+(define t* (hash 'a 1 'b "cat"))
+
+;; These `ann` do not work on 6.5, should work because `hash` makes an immutable table
+(void
+  (ann t* (HashTable Any Any))
+  (ann t* (HashTable Symbol (U String Integer))))
diff --git a/typed-racket-test/succeed/pr390-variation-2.rkt b/typed-racket-test/succeed/pr390-variation-2.rkt
new file mode 100644
index 00000000..a221f181
--- /dev/null
+++ b/typed-racket-test/succeed/pr390-variation-2.rkt
@@ -0,0 +1,130 @@
+#lang racket/base
+
+;; Test that immutable hash contracts run in low time/space
+
+;; The Racket program at the bottom of this file runs very slowly
+;;  without Immutable-HashTable types.
+;; Reported by John Clements
+;; https://groups.google.com/forum/#!searchin/racket-users/trie$20functions/racket-users/WBPCsdae5fs/J7CIOeV-CQAJ
+
+(module trie typed/racket
+  ;; Copied from pfds/trie, commit d4a8809b4d621dc3679d3473422a48d27b133a4f
+  ;;  then changed "HashTable" to "Immutable-HashTable"
+
+  (provide lookup bind trie insert Trie tries)
+
+  (require scheme/match)
+  (define-type-alias (Key A) (Listof A))
+
+  (define-struct: Mt ())
+  (define-struct: (A) Some ([elem : A]))
+
+  (define-type-alias (Option A) (U Mt (Some A)))
+
+  (define-struct: (K V) Trie ([opt : (Option V)]
+                              [map : (Immutable-HashTable K (Trie K V))]))
+
+  (: empty : (All (K V) (-> (Trie K V))))
+  (define (empty) 
+    (make-Trie (make-Mt) 
+               (ann (make-immutable-hash null) (Immutable-HashTable K (Trie K V)))))
+
+  (: lookup : (All (K V) ((Key K) (Trie K V) -> V)))
+  (define (lookup keys map)
+    (if (null? keys)
+        (let ([opt (Trie-opt map)])
+          (if (Mt? opt)
+              (error 'lookup "given key not found in the trie")
+              (Some-elem opt)))
+        (let ([fst (car keys)]
+              [hash (Trie-map map)])
+          (with-handlers
+              ([exn:fail? (lambda (error?) 
+                            (error 'lookup "given key not found in the trie"))])
+            (lookup (cdr keys) (hash-ref hash fst))))))
+
+  (: bind : (All (K V) ((Key K) V (Trie K V) -> (Trie K V))))
+  (define (bind lok v map)
+    (let ([hash (Trie-map map)]
+          [fst (car lok)]
+          [rst (cdr lok)]
+          [opt (Trie-opt map)])
+      (make-Trie opt (hash-set hash fst 
+                               (ann (with-handlers 
+                                        ([exn:fail? 
+                                          (lambda (error?) (build v rst))])
+                                      (bind rst v (hash-ref hash fst)))
+                                    (Trie K V))))))
+
+  (: build : (All (K V) (V (Listof K) -> (Trie K V))))
+  (define (build val lstk)
+    (if (null? lstk)
+        (make-Trie (make-Some val) 
+                   (ann (make-immutable-hash null) 
+                        (Immutable-HashTable K (Trie K V))))
+        (make-Trie (make-Mt) 
+                   (make-immutable-hash 
+                    (list (cons (car lstk) (build val (cdr lstk))))))))
+
+  (: trie : (All (K) ((Listof (Listof K)) -> (Trie K Integer))))
+  (define (trie lst)
+    (insert (get-vals lst) lst (ann (empty) (Trie K Integer))))
+
+  (: get-vals : (All (K) ((Listof (Listof K)) -> (Listof Integer))))
+  (define (get-vals lst)
+    (: local : (All (K) (Integer (Listof (Listof K)) -> (Listof Integer))))
+    (define (local ctr lstk)
+      (if (null? (cdr lstk))
+          (cons ctr null)
+          (cons ctr (local (add1 ctr) (cdr lstk)))))
+    (local 1 lst))
+
+  ;; While creating the tree, 
+  ;; if   (hash-ref hash k) throws an error, 
+  ;; then it means that that there is no entry for k. So build a new
+  ;;      Trie for rest of the key and create an entry for k. 
+  ;; else go deeper into the insert searching for the rest of the key.
+
+  (: insert : 
+     (All (K V) ((Listof V) (Listof (Listof K)) (Trie K V) -> (Trie K V))))
+  (define (insert lstv lstk tri)
+    (match (list lstv lstk)
+      [(list null null) tri]
+      [(list (cons v vs) (cons (cons k ks) rstk))
+       (let* ([hash (Trie-map tri)]
+              [tree (ann (with-handlers ([exn:fail? (lambda (error?) 
+                                                      (build v ks))])
+                           (go-deep (hash-ref hash k) ks v)) 
+                         (Trie K V))])
+         (insert vs rstk
+                 (make-Trie (Trie-opt tri) (hash-set hash k tree))))]))
+
+  (: tries : (All (K V) ((Listof V) (Listof (Listof K)) -> (Trie K V))))
+  (define (tries lstv lstk)
+    (insert lstv lstk (ann (empty) (Trie K V))))
+
+  ;; Uses the same trick as previous one does
+  (: go-deep : (All (K V) ((Trie K V) (Listof K) V -> (Trie K V))))
+  (define (go-deep tri lstk val)
+    (if (null? lstk)
+        (make-Trie (make-Some val) (Trie-map tri))
+        (let* ([hash (Trie-map tri)]
+               [k (car lstk)]
+               [ks (cdr lstk)]
+               [insert (ann (with-handlers
+                                ([exn:fail? (lambda (error?) (build val ks))])
+                              (go-deep (hash-ref hash k) ks val))
+                            (Trie K V))])
+          (make-Trie (Trie-opt tri) (hash-set hash k insert)))))
+) (require 'trie racket/sandbox)
+
+(define (main)
+  (define (rand-list)
+    (for/list ([i (in-range 128)])
+        (random 256)))
+  (define t (trie (list (rand-list))))
+  (bind (rand-list) 0 t)
+  (void))
+
+(call-with-limits 2 3
+  main)
diff --git a/typed-racket-test/succeed/pr390-variation-3.rkt b/typed-racket-test/succeed/pr390-variation-3.rkt
new file mode 100644
index 00000000..c9d1844e
--- /dev/null
+++ b/typed-racket-test/succeed/pr390-variation-3.rkt
@@ -0,0 +1,35 @@
+#lang typed/racket/base
+
+;; Test filters for hash types
+
+(: filter-HT (-> (HashTable Integer Integer) HashTableTop))
+(define (filter-HT h)
+  (cond
+   [(immutable? h)
+    (ann h (Immutable-HashTable Integer Integer))]
+   [(hash-weak? h)
+    (ann h (Weak-HashTable Integer Integer))]
+   [else
+    (ann h (Mutable-HashTable Integer Integer))]))
+
+(: filter-U (-> (U #f (HashTable Integer Integer)) Any))
+(define (filter-U maybe-ht)
+  (cond
+   [(immutable? maybe-ht)
+    (ann maybe-ht (Immutable-HashTable Integer Integer))]
+   [(and maybe-ht (hash-weak? maybe-ht))
+    (ann maybe-ht Weak-HashTableTop)]
+   [(hash? maybe-ht)
+    (ann maybe-ht Mutable-HashTableTop)]
+   [else
+    (ann maybe-ht #f)]))
+
+(void
+  (filter-HT (make-immutable-hash '((1 . 1))))
+  (filter-HT (make-hash '((1 . 1))))
+  (filter-HT (make-weak-hash '((1 . 1))))
+
+  (filter-U #f)
+  (filter-U (make-immutable-hash '((1 . 1))))
+  (filter-U (make-hash '((1 . 1))))
+  (filter-U (make-weak-hash '((1 . 1)))))
diff --git a/typed-racket-test/succeed/pr390-variation-4.rkt b/typed-racket-test/succeed/pr390-variation-4.rkt
new file mode 100644
index 00000000..34681b9f
--- /dev/null
+++ b/typed-racket-test/succeed/pr390-variation-4.rkt
@@ -0,0 +1,47 @@
+#lang typed/racket/base
+
+;; Test Hash Table functions with "complicated" types
+
+(require typed/rackunit)
+
+(test-case "hash-copy" ;; returns a mutable hash with same 'key-holding strength'
+  (check-pred hash?
+    (ann (hash-copy (make-immutable-hash)) Mutable-HashTableTop))
+  (check-pred hash?
+    (ann (hash-copy (make-immutable-hash '((1 . 1)))) (Mutable-HashTable Integer Integer)))
+
+  (check-pred hash?
+    (ann (hash-copy (make-hash '((1 . 1)))) (Mutable-HashTable Integer Integer)))
+  (check-pred hash?
+    (ann (hash-copy (make-hash)) Mutable-HashTableTop))
+
+  (check-pred hash-weak?
+    (ann (hash-copy (make-weak-hash '((1 . 1)))) (Weak-HashTable Integer Integer)))
+  (check-pred hash-weak?
+    (ann (hash-copy (make-weak-hash)) Weak-HashTableTop)))
+
+(test-case "hash-copy-clear" ;; returns hash with same mutability
+  (check-pred immutable?
+    (ann (hash-copy-clear (make-immutable-hash)) (Immutable-HashTable Any Any)))
+  (check-pred immutable?
+    (ann (hash-copy-clear (make-immutable-hash '((a . b)))) (Immutable-HashTable Symbol Symbol)))
+
+  (check-pred hash?
+    (ann (hash-copy-clear (make-hash)) Mutable-HashTableTop))
+  (check-pred hash?
+    (ann (hash-copy-clear (make-hash '((a . b)))) (Mutable-HashTable Symbol Symbol)))
+
+  (check-pred hash-weak?
+    (ann (hash-copy-clear (make-weak-hash)) Weak-HashTableTop))
+  (check-pred hash-weak?
+    (ann (hash-copy-clear (make-weak-hash '((a . b)))) (Weak-HashTable Symbol Symbol))))
+
+(test-case "hash-remove" ;; only for immutable hashtables, but the TR type allows mutable/weak
+  (check-pred immutable?
+    (ann (hash-remove (make-immutable-hash '((a . A))) 'a) (Immutable-HashTable Symbol Symbol)))
+
+  (check-exn exn:fail:contract?
+    (λ () (hash-remove (make-hash '((a . A))) 'a)))
+
+  (check-exn exn:fail:contract?
+    (λ () (hash-remove (make-weak-hash '((a . A))) 'a))))
diff --git a/typed-racket-test/succeed/pr390-variation-5.rkt b/typed-racket-test/succeed/pr390-variation-5.rkt
new file mode 100644
index 00000000..39e7ad16
--- /dev/null
+++ b/typed-racket-test/succeed/pr390-variation-5.rkt
@@ -0,0 +1,26 @@
+#lang racket/base
+
+;; Test contract generation
+;; - HashTable should make 1 contract, not an or/c
+;; - (U #f HashTable) should make an or/c with 2 things
+;; (This file only generates contracts, it doesn't check that they are not redundant.)
+
+(module u racket/base
+  (define u-hash (make-immutable-hash '((a . 1) (b . 2))))
+  (provide u-hash))
+
+(module t typed/racket
+  (require/typed (submod ".." u)
+    (u-hash (U Integer #f (Immutable-HashTable Symbol Integer) (Mutable-HashTable String String))))
+
+  (define t-hash : (HashTable Symbol Integer)
+    (make-immutable-hash '((a . 1) (b . 2))))
+  (provide u-hash t-hash))
+(require 't racket/contract)
+
+(void
+  (hash-ref u-hash 'a)
+  (hash-set u-hash 'c 3)
+
+  (hash-ref t-hash 'a)
+  (hash-set t-hash 'c 3))
diff --git a/typed-racket-test/unit-tests/infer-tests.rkt b/typed-racket-test/unit-tests/infer-tests.rkt
index 8885f04c..19891d50 100644
--- a/typed-racket-test/unit-tests/infer-tests.rkt
+++ b/typed-racket-test/unit-tests/infer-tests.rkt
@@ -111,7 +111,9 @@
    (pd-t (-thread-cell (-v a)) (b) (-thread-cell (-v a)) (-thread-cell (-v a)))
 
    (pd-t (-HT (-v a) (-v a)) (a) (-HT -Bottom -Bottom) (-HT Univ Univ))
-   (pd-t (-HT (-lst (-v a)) (-lst (-v a))) (a) (-HT -Bottom -Bottom) (-HT Univ Univ))
+   (pd-t (-HT (-lst (-v a)) (-lst (-v a))) (a)
+         (Un (-Immutable-HT (-lst -Bottom) (-lst -Bottom)) (-Mutable-HT -Bottom -Bottom) (-Weak-HT -Bottom -Bottom))
+         (Un (-Immutable-HT (-lst Univ) (-lst Univ)) (-Mutable-HT Univ Univ) (-Weak-HT Univ Univ)))
    (pd-t (-HT (-v a) (-v a)) (b) (-HT (-v a) (-v a)) (-HT (-v a) (-v a)))
 
    (pd-t (-Param (-v a) (-v b)) (a b) (-Param Univ -Bottom) (-Param -Bottom Univ))
diff --git a/typed-racket-test/unit-tests/remove-intersect-tests.rkt b/typed-racket-test/unit-tests/remove-intersect-tests.rkt
index 01574146..dece3d53 100644
--- a/typed-racket-test/unit-tests/remove-intersect-tests.rkt
+++ b/typed-racket-test/unit-tests/remove-intersect-tests.rkt
@@ -72,8 +72,17 @@
    [(-mu x (Un (Un -Number -String) (-pair -Number x)))
     (-mu x (Un (Un -Number -Symbol) (-pair -Number x)))
     (-mu x (Un -Number (-pair -Number x)))]
+   [(-Immutable-HT -String -Symbol)
+    (-HT -String -Symbol)
+    (-Immutable-HT -String -Symbol)]
+   [(-Mutable-HT -String -Symbol)
+    (-HT -String -Symbol)
+    (-Mutable-HT -String -Symbol)]
+   [(-Weak-HT -String -Symbol)
+    (-HT -String -Symbol)
+    (-Weak-HT -String -Symbol)]
    [(make-Listof (-mu x (Un -String (-HT -String x))))
-    (make-Listof -HashtableTop)
+    (make-Listof -HashTableTop)
     (make-Listof (-HT -String (-mu x (Un -String (-HT -String x)))))]))
 
 (define-syntax (remo-tests stx)
diff --git a/typed-racket-test/unit-tests/static-contract-optimizer-tests.rkt b/typed-racket-test/unit-tests/static-contract-optimizer-tests.rkt
index 9d75e8e3..fda559d9 100644
--- a/typed-racket-test/unit-tests/static-contract-optimizer-tests.rkt
+++ b/typed-racket-test/unit-tests/static-contract-optimizer-tests.rkt
@@ -133,15 +133,22 @@
       #:neg (vector/sc set?/sc))
 
     ;; HashTables
-    (check-optimize (hash/sc any/sc any/sc)
-      #:pos any/sc
-      #:neg hash?/sc)
-    (check-optimize (hash/sc none/sc any/sc)
-      #:pos (hash/sc none/sc any/sc)
-      #:neg (hash/sc none/sc any/sc))
-    (check-optimize (hash/sc any/sc none/sc)
-      #:pos (hash/sc any/sc none/sc)
-      #:neg (hash/sc any/sc none/sc))
+    (let ()
+      (define-syntax-rule (make-?hash/sc-check ctc flat-ctc)
+        (begin
+          (check-optimize (ctc any/sc any/sc)
+            #:pos any/sc
+            #:neg flat-ctc)
+          (check-optimize (ctc none/sc any/sc)
+            #:pos (ctc none/sc any/sc)
+            #:neg (ctc none/sc any/sc))
+          (check-optimize (ctc any/sc none/sc)
+            #:pos (ctc any/sc none/sc)
+            #:neg (ctc any/sc none/sc))))
+      (make-?hash/sc-check hash/sc hash?/sc)
+      (make-?hash/sc-check immutable-hash/sc immutable-hash?/sc)
+      (make-?hash/sc-check mutable-hash/sc mutable-hash?/sc)
+      (make-?hash/sc-check weak-hash/sc weak-hash?/sc))
 
     ;; And
     (check-optimize (and/sc set?/sc)
diff --git a/typed-racket-test/unit-tests/subtype-tests.rkt b/typed-racket-test/unit-tests/subtype-tests.rkt
index 10332148..2b5d526c 100644
--- a/typed-racket-test/unit-tests/subtype-tests.rkt
+++ b/typed-racket-test/unit-tests/subtype-tests.rkt
@@ -181,7 +181,12 @@
     [make-Async-Channel () #:top -Async-ChannelTop]
     [make-ThreadCell () #:top -ThreadCellTop]
     [make-Weak-Box () #:top -Weak-BoxTop]
-    [make-Hashtable () () #:top -HashtableTop]
+    [make-Immutable-HashTable () () #:top -HashTableTop]
+    [make-Mutable-HashTable () () #:top -HashTableTop]
+    [make-Mutable-HashTable () () #:top -Mutable-HashTableTop]
+    [make-Weak-HashTable () () #:top -HashTableTop]
+    [make-Weak-HashTable () () #:top -Weak-HashTableTop]
+    [make-HashTable () () #:top -HashTableTop]
     [make-Prompt-Tagof () () #:top -Prompt-TagTop]
     [make-Continuation-Mark-Keyof () #:top -Continuation-Mark-KeyTop])
    (subtyping-tests
diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt
index 32a5c3cd..ac063f2d 100644
--- a/typed-racket-test/unit-tests/typecheck-tests.rkt
+++ b/typed-racket-test/unit-tests/typecheck-tests.rkt
@@ -1050,10 +1050,10 @@
         [tc-e/t #'#&2 (-Syntax (-box (-Syntax -PosByte)))]
         [tc-e/t (ann #'#&2 (Syntaxof (Boxof (Syntaxof (U 2 'foo)))))
                 (-Syntax (-box (-Syntax (t:Un (-val 2) (-val 'foo)))))]
-        [tc-e/t #'#hash([1 . 1] [2 . 2]) (-Syntax (make-Hashtable -Int (-Syntax -PosByte)))]
+        [tc-e/t #'#hash([1 . 1] [2 . 2]) (-Syntax (-Immutable-HT -Int (-Syntax -PosByte)))]
         [tc-e/t (ann #'#hash([1 . 1] [2 . 2]) (Syntaxof (HashTable (U 1 2 'foo)
                                                                    (Syntaxof (U 1 2 'bar)))))
-                (-Syntax (make-Hashtable (t:Un (-val 1) (-val 2) (-val 'foo))
+                (-Syntax (make-HashTable (t:Un (-val 1) (-val 2) (-val 'foo))
                                          (-Syntax (t:Un (-val 1) (-val 2) (-val 'bar)))))]
         ;; syntax->list
         [tc-e (syntax->list #'(2 3 4)) (-lst (-Syntax -PosByte))]
@@ -1328,6 +1328,10 @@
               (-HT -Number -Number)]
         [tc-e #{(make-immutable-hash) :: (HashTable String Symbol)}
               (-HT -String -Symbol)]
+        [tc-e #{(make-hash) :: (Mutable-HashTable Number Number)}
+              (-Mutable-HT -Number -Number)]
+        [tc-e #{(make-immutable-hash) :: (Immutable-HashTable String Symbol)}
+              (-Immutable-HT -String -Symbol)]
         [tc-e (hash-has-key? (make-hash '((1 . 2))) 1) -Boolean]
 
         [tc-err (let: ([fact : (Number -> Number)
@@ -1539,7 +1543,7 @@
 
         (tc-e (boolean? #t) #:ret (tc-ret -Boolean -true-propset))
         (tc-e (boolean? 6) #:ret (tc-ret -Boolean -false-propset))
-        (tc-e (immutable? (cons 3 4)) -Boolean)
+        (tc-e (immutable? (cons 3 4)) #:ret (tc-ret -Boolean -false-propset))
 
         (tc-e (boolean=? #t false) -Boolean)
         (tc-e (symbol=? 'foo 'foo) -Boolean)
@@ -1712,7 +1716,7 @@
         (tc-e (syntax-position #'here) (-opt -PosInt))
         (tc-e (syntax-span #'here) (-opt -Nat))
         (tc-e (syntax-local-identifier-as-binding #'x) (-Syntax -Symbol))
-        (tc-e (syntax-debug-info #'x) -HashtableTop)
+        (tc-e (syntax-debug-info #'x) -HashTableTop)
         (tc-e (internal-definition-context-introduce (syntax-local-make-definition-context) #'x)
               (-Syntax (-val 'x)))
 
@@ -2433,8 +2437,8 @@
        [tc-e (assoc 3 '((a . 5) (b . 7))) (t:Un (-val #f) (-pair (one-of/c 'a 'b) -PosByte))]
        [tc-e (set-remove (set 1 2 3) 'a) (-set -PosByte)]
        ;; don't return HashTableTop
-       [tc-e (hash-remove #hash((a . 5) (b . 7)) 3) (-HT -Symbol -Integer)]
-       [tc-e (hash-remove #hash((a . 5) (b . 7)) 3) (-HT -Symbol -Integer)]
+       [tc-e (hash-remove #hash((a . 5) (b . 7)) 3) (-Immutable-HT -Symbol -Integer)]
+       [tc-e (hash-remove #hash((a . 5) (b . 7)) 3) (-Immutable-HT -Symbol -Integer)]
        ;; these should actually work
        [tc-e (vector-memq 3 #(a b c)) (t:Un (-val #f) -Index)]
        [tc-e (vector-memv 3 #(a b c)) (t:Un (-val #f) -Index)]
@@ -3997,16 +4001,17 @@
    (tc-l #"foo" -Bytes)
    [tc-l () -Null]
    [tc-l (3 . 4) (-pair -PosByte -PosByte)]
-   [tc-l #hash() (make-Hashtable Univ Univ)]
-   [tc-l #hash((1 . 2) (3 . 4)) (make-Hashtable -Integer -Integer)]
-   [tc-l #hasheq((a . q) (b . w)) (make-Hashtable -Symbol -Symbol)]
+   [tc-l #hash() (-Immutable-HT Univ Univ)]
+   [tc-l #hash() (-Immutable-HT Univ Univ)]
+   [tc-l #hash((1 . 2) (3 . 4)) (-Immutable-HT -Integer -Integer)]
+   [tc-l #hasheq((a . q) (b . w)) (-Immutable-HT -Symbol -Symbol)]
    [tc-l #hash{[:a . :b]}
-         (let ([rec-type (-mu X (make-Hashtable (t:Un -Symbol X) (t:Un -Symbol X)))])
-           (make-Hashtable (t:Un -Symbol rec-type) (t:Un -Symbol rec-type)))
-         #:expected (-mu X (make-Hashtable (t:Un -Symbol X) (t:Un -Symbol X)))]
+         (let ([rec-type (-mu X (-Immutable-HT (t:Un -Symbol X) (t:Un -Symbol X)))])
+           (-Immutable-HT (t:Un -Symbol rec-type) (t:Un -Symbol rec-type)))
+         #:expected (-mu X (-Immutable-HT (t:Un -Symbol X) (t:Un -Symbol X)))]
    [tc-l #hash{[:a . :b]}
-         (make-Hashtable (-val ':a) (-val ':b))
-         #:expected (t:Un (-val #f) (make-Hashtable (-val ':a) (-val ':b)))]
+         (-Immutable-HT (-val ':a) (-val ':b))
+         #:expected (t:Un (-val #f) (-Immutable-HT (-val ':a) (-val ':b)))]
    [tc-l #(:a :b)
          (-vec (t:Un (-val ':a) (-val ':b) (-mu X (-vec (t:Un (-val ':a) (-val ':b) X)))))
          #:expected (-mu X (-vec (t:Un (-val ':a) (-val ':b) X)))]