diff --git a/src/Init/Data/Hashable.lean b/src/Init/Data/Hashable.lean
index f30dae0e72..1e7c328d4e 100644
--- a/src/Init/Data/Hashable.lean
+++ b/src/Init/Data/Hashable.lean
@@ -8,42 +8,42 @@ import Init.Data.UInt
 import Init.Data.String
 universes u
 
-instance : Hashable Nat where
-  hash n := USize.ofNat n
+instance : HashableUSize Nat where
+  hashUSize n := USize.ofNat n
 
-instance [Hashable α] [Hashable β] : Hashable (α × β) where
-  hash | (a, b) => mixUSizeHash (hash a) (hash b)
+instance [HashableUSize α] [HashableUSize β] : HashableUSize (α × β) where
+  hashUSize | (a, b) => mixUSizeHash (hashUSize a) (hashUSize b)
 
-instance : Hashable Bool where
-  hash
+instance : HashableUSize Bool where
+  hashUSize
     | true  => 11
     | false => 13
 
-protected def Option.hash [Hashable α] : Option α → USize
+protected def Option.hash [HashableUSize α] : Option α → USize
   | none   => 11
-  | some a => mixUSizeHash (hash a) 13
+  | some a => mixUSizeHash (hashUSize a) 13
 
-instance [Hashable α] : Hashable (Option α) where
-  hash
+instance [HashableUSize α] : HashableUSize (Option α) where
+  hashUSize
     | none   => 11
-    | some a => mixUSizeHash (hash a) 13
+    | some a => mixUSizeHash (hashUSize a) 13
 
-instance [Hashable α] : Hashable (List α) where
-  hash as := as.foldl (fun r a => mixUSizeHash r (hash a)) 7
+instance [HashableUSize α] : HashableUSize (List α) where
+  hashUSize as := as.foldl (fun r a => mixUSizeHash r (hashUSize a)) 7
 
-instance : Hashable UInt32 where
-  hash n := n.toUSize
+instance : HashableUSize UInt32 where
+  hashUSize n := n.toUSize
 
-instance : Hashable UInt64 where
-  hash n := n.toUSize
+instance : HashableUSize UInt64 where
+  hashUSize n := n.toUSize
 
-instance : Hashable USize where
-  hash n := n
+instance : HashableUSize USize where
+  hashUSize n := n
 
-instance : Hashable Int where
-  hash
+instance : HashableUSize Int where
+  hashUSize
     | Int.ofNat n => USize.ofNat (2 * n)
     | Int.negSucc n => USize.ofNat (2 * n + 1)
 
-instance (P : Prop) : Hashable P where
-  hash := Function.const P 0
+instance (P : Prop) : HashableUSize P where
+  hashUSize := Function.const P 0
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index ada35c1546..eb29853ac8 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1587,10 +1587,10 @@ instance nonBacktrackable : Backtrackable PUnit σ where
 
 end EStateM
 
-class Hashable (α : Sort u) where
-  hash : α → USize
+class HashableUSize (α : Sort u) where
+  hashUSize : α → USize
 
-export Hashable (hash)
+export HashableUSize (hashUSize)
 
 @[extern "lean_usize_mix_hash"]
 constant mixUSizeHash (u₁ u₂ : USize) : USize
@@ -1601,8 +1601,8 @@ constant mixUSizeHash (u₁ u₂ : USize) : USize
 @[extern "lean_string_hash"]
 protected constant String.hash (s : @& String) : USize
 
-instance : Hashable String where
-  hash := String.hash
+instance : HashableUSize String where
+  hashUSize := String.hash
 
 namespace Lean
 
@@ -1620,18 +1620,18 @@ protected def Name.hash : Name → USize
   | Name.str p s h => h
   | Name.num p v h => h
 
-instance : Hashable Name where
-  hash := Name.hash
+instance : HashableUSize Name where
+  hashUSize := Name.hash
 
 namespace Name
 
 @[export lean_name_mk_string]
 def mkStr (p : Name) (s : String) : Name :=
-  Name.str p s (mixUSizeHash (hash p) (hash s))
+  Name.str p s (mixUSizeHash (hashUSize p) (hashUSize s))
 
 @[export lean_name_mk_numeral]
 def mkNum (p : Name) (v : Nat) : Name :=
-  Name.num p v (mixUSizeHash (hash p) (dite (LT.lt v USize.size) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 (by decide))))
+  Name.num p v (mixUSizeHash (hashUSize p) (dite (LT.lt v USize.size) (fun h => USize.ofNatCore v h) (fun _ => USize.ofNat32 17 (by decide))))
 
 def mkSimple (s : String) : Name :=
   mkStr Name.anonymous s
diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean
index 8931dcb121..f3a03fa022 100644
--- a/src/Lean/Compiler/IR/Basic.lean
+++ b/src/Lean/Compiler/IR/Basic.lean
@@ -35,12 +35,12 @@ abbrev Index.lt (a b : Index) : Bool := a < b
 instance : BEq VarId := ⟨fun a b => a.idx == b.idx⟩
 instance : ToString VarId := ⟨fun a => "x_" ++ toString a.idx⟩
 instance : ToFormat VarId := ⟨fun a => toString a⟩
-instance : Hashable VarId := ⟨fun a => hash a.idx⟩
+instance : HashableUSize VarId := ⟨fun a => hashUSize a.idx⟩
 
 instance : BEq JoinPointId := ⟨fun a b => a.idx == b.idx⟩
 instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩
 instance : ToFormat JoinPointId := ⟨fun a => toString a⟩
-instance : Hashable JoinPointId := ⟨fun a => hash a.idx⟩
+instance : HashableUSize JoinPointId := ⟨fun a => hashUSize a.idx⟩
 
 abbrev MData := KVMap
 abbrev MData.empty : MData := {}
diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean
index 716ff40c08..4cdf9f439b 100644
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -20,8 +20,8 @@ def beq : Key → Key → Bool
 instance : BEq Key := ⟨beq⟩
 
 def getHash : Key → USize
-  | (f, x) => mixUSizeHash (hash f) (hash x)
-instance : Hashable Key := ⟨getHash⟩
+  | (f, x) => mixUSizeHash (hashUSize f) (hashUSize x)
+instance : HashableUSize Key := ⟨getHash⟩
 end OwnedSet
 
 open OwnedSet (Key) in
@@ -41,10 +41,10 @@ inductive Key where
   deriving BEq
 
 def getHash : Key → USize
-  | Key.decl n  => hash n
-  | Key.jp n id => mixUSizeHash (hash n) (hash id)
+  | Key.decl n  => hashUSize n
+  | Key.jp n id => mixUSizeHash (hashUSize n) (hashUSize id)
 
-instance : Hashable Key := ⟨getHash⟩
+instance : HashableUSize Key := ⟨getHash⟩
 end ParamMap
 
 open ParamMap (Key)
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index 07021ca686..9bb1cd68c6 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -27,13 +27,13 @@ open Std (HashMap PHashMap)
      that an entry was "removed" from the hashtable.
    - We do not need additional bookkeeping for extracting the local entries.
 -/
-structure SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+structure SMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] where
   stage₁ : Bool         := true
   map₁   : HashMap α β  := {}
   map₂   : PHashMap α β := {}
 
 namespace SMap
-variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+variable {α : Type u} {β : Type v} [BEq α] [HashableUSize α]
 
 instance : Inhabited (SMap α β) := ⟨{}⟩
 def empty : SMap α β := {}
@@ -92,10 +92,10 @@ def toList (m : SMap α β) : List (α × β) :=
 
 end SMap
 
-def List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
+def List.toSMap [BEq α] [HashableUSize α] (es : List (α × β)) : SMap α β :=
   es.foldl (init := {}) fun s (a, b) => s.insert a b
 
-instance {_ : BEq α} {_ : Hashable α} [Repr α] [Repr β] : Repr (SMap α β) where
+instance {_ : BEq α} {_ : HashableUSize α} [Repr α] [Repr β] : Repr (SMap α β) where
   reprPrec v prec := Repr.addAppParen (reprArg v.toList ++ ".toSMap") prec
 
 end Lean
diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean
index f49fa67726..9f5f5cc723 100644
--- a/src/Lean/Elab/Deriving/Hashable.lean
+++ b/src/Lean/Elab/Deriving/Hashable.lean
@@ -61,9 +61,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
   let binders    := header.binders
   if ctx.usePartial then
     -- TODO(Dany): Get rid of this code branch altogether once we have well-founded recursion
-    `(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term) 
+    `(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term) 
+    `(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : USize := $body:term)
 
 def mkHashFuncs (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]
@@ -86,5 +86,5 @@ def mkHashableHandler (declNames : Array Name) : CommandElabM Bool := do
     return false
 
 builtin_initialize
-  registerBuiltinDerivingHandler ``Hashable mkHashableHandler
-  registerTraceClass `Elab.Deriving.hashable
\ No newline at end of file
+  registerBuiltinDerivingHandler ``HashableUSize mkHashableHandler
+  registerTraceClass `Elab.Deriving.hashable
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index df2a590ed4..0f90ecca30 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -78,7 +78,7 @@ instance [Monad m] [MonadRecDepth m] : MonadRecDepth (ReaderT ρ m) where
 instance [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m) :=
   inferInstanceAs (MonadRecDepth (ReaderT _ _))
 
-instance [BEq α] [Hashable α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m) :=
+instance [BEq α] [HashableUSize α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m) :=
   inferInstanceAs (MonadRecDepth (StateRefT' _ _ _))
 
 @[inline] def withIncRecDepth [Monad m] [MonadError m] [MonadRecDepth m] (x : m α) : m α := do
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 95c6edd303..1ed0f81af8 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -14,10 +14,10 @@ inductive Literal where
   deriving Inhabited, BEq
 
 protected def Literal.hash : Literal → USize
-  | Literal.natVal v => hash v
-  | Literal.strVal v => hash v
+  | Literal.natVal v => hashUSize v
+  | Literal.strVal v => hashUSize v
 
-instance : Hashable Literal := ⟨Literal.hash⟩
+instance : HashableUSize Literal := ⟨Literal.hash⟩
 
 def Literal.lt : Literal → Literal → Bool
   | Literal.natVal _,  Literal.strVal _  => true
@@ -47,7 +47,7 @@ def BinderInfo.isExplicit : BinderInfo → Bool
   | BinderInfo.instImplicit   => false
   | _                         => true
 
-instance : Hashable BinderInfo := ⟨BinderInfo.hash⟩
+instance : HashableUSize BinderInfo := ⟨BinderInfo.hash⟩
 
 def BinderInfo.isInstImplicit : BinderInfo → Bool
   | BinderInfo.instImplicit => true
@@ -201,7 +201,7 @@ def ctorName : Expr → String
 protected def hash (e : Expr) : USize :=
   e.data.hash
 
-instance : Hashable Expr := ⟨Expr.hash⟩
+instance : HashableUSize Expr := ⟨Expr.hash⟩
 
 def hasFVar (e : Expr) : Bool :=
   e.data.hasFVar
@@ -225,7 +225,7 @@ def looseBVarRange (e : Expr) : Nat :=
 def binderInfo (e : Expr) : BinderInfo :=
   e.data.binderInfo
 
-@[export lean_expr_hash] def hashEx : Expr → USize := hash
+@[export lean_expr_hash] def hashEx : Expr → USize := hashUSize
 @[export lean_expr_has_fvar] def hasFVarEx : Expr → Bool := hasFVar
 @[export lean_expr_has_expr_mvar] def hasExprMVarEx : Expr → Bool := hasExprMVar
 @[export lean_expr_has_level_mvar] def hasLevelMVarEx : Expr → Bool := hasLevelMVar
@@ -237,7 +237,7 @@ def binderInfo (e : Expr) : BinderInfo :=
 end Expr
 
 def mkLit (l : Literal) : Expr :=
-  Expr.lit l $ mkData (mixUSizeHash 3 (hash l))
+  Expr.lit l $ mkData (mixUSizeHash 3 (hashUSize l))
 
 def mkNatLit (n : Nat) : Expr :=
   mkLit (Literal.natVal n)
@@ -246,7 +246,7 @@ def mkStrLit (s : String) : Expr :=
   mkLit (Literal.strVal s)
 
 def mkConst (n : Name) (lvls : List Level := []) : Expr :=
-  Expr.const n lvls $ mkData (mixUSizeHash 5 $ mixUSizeHash (hash n) (hash lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
+  Expr.const n lvls $ mkData (mixUSizeHash 5 $ mixUSizeHash (hashUSize n) (hashUSize lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
 
 def Literal.type : Literal → Expr
   | Literal.natVal _ => mkConst `Nat
@@ -256,26 +256,26 @@ def Literal.type : Literal → Expr
 def Literal.typeEx : Literal → Expr := Literal.type
 
 def mkBVar (idx : Nat) : Expr :=
-  Expr.bvar idx $ mkData (mixUSizeHash 7 $ hash idx) (idx+1)
+  Expr.bvar idx $ mkData (mixUSizeHash 7 $ hashUSize idx) (idx+1)
 
 def mkSort (lvl : Level) : Expr :=
-  Expr.sort lvl $ mkData (mixUSizeHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam
+  Expr.sort lvl $ mkData (mixUSizeHash 11 $ hashUSize lvl) 0 false false lvl.hasMVar lvl.hasParam
 
 def mkFVar (fvarId : FVarId) : Expr :=
-  Expr.fvar fvarId $ mkData (mixUSizeHash 13 $ hash fvarId) 0 true
+  Expr.fvar fvarId $ mkData (mixUSizeHash 13 $ hashUSize fvarId) 0 true
 
 def mkMVar (fvarId : MVarId) : Expr :=
-  Expr.mvar fvarId $ mkData (mixUSizeHash 17 $ hash fvarId) 0 false true
+  Expr.mvar fvarId $ mkData (mixUSizeHash 17 $ hashUSize fvarId) 0 false true
 
 def mkMData (d : MData) (e : Expr) : Expr :=
-  Expr.mdata d e $ mkData (mixUSizeHash 19 $ hash e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
+  Expr.mdata d e $ mkData (mixUSizeHash 19 $ hashUSize e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
 
 def mkProj (s : Name) (i : Nat) (e : Expr) : Expr :=
-  Expr.proj s i e $ mkData (mixUSizeHash 23 $ mixUSizeHash (hash s) $ mixUSizeHash (hash i) (hash e))
+  Expr.proj s i e $ mkData (mixUSizeHash 23 $ mixUSizeHash (hashUSize s) $ mixUSizeHash (hashUSize i) (hashUSize e))
       e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
 
 def mkApp (f a : Expr) : Expr :=
-  Expr.app f a $ mkData (mixUSizeHash 29 $ mixUSizeHash (hash f) (hash a))
+  Expr.app f a $ mkData (mixUSizeHash 29 $ mixUSizeHash (hashUSize f) (hashUSize a))
     (Nat.max f.looseBVarRange a.looseBVarRange)
     (f.hasFVar || a.hasFVar)
     (f.hasExprMVar || a.hasExprMVar)
@@ -284,7 +284,7 @@ def mkApp (f a : Expr) : Expr :=
 
 def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
   -- let x := x.eraseMacroScopes
-  Expr.lam x t b $ mkDataForBinder (mixUSizeHash 31 $ mixUSizeHash (hash t) (hash b))
+  Expr.lam x t b $ mkDataForBinder (mixUSizeHash 31 $ mixUSizeHash (hashUSize t) (hashUSize b))
     (Nat.max t.looseBVarRange (b.looseBVarRange - 1))
     (t.hasFVar || b.hasFVar)
     (t.hasExprMVar || b.hasExprMVar)
@@ -294,7 +294,7 @@ def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
 
 def mkForall (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
   -- let x := x.eraseMacroScopes
-  Expr.forallE x t b $ mkDataForBinder (mixUSizeHash 37 $ mixUSizeHash (hash t) (hash b))
+  Expr.forallE x t b $ mkDataForBinder (mixUSizeHash 37 $ mixUSizeHash (hashUSize t) (hashUSize b))
     (Nat.max t.looseBVarRange (b.looseBVarRange - 1))
     (t.hasFVar || b.hasFVar)
     (t.hasExprMVar || b.hasExprMVar)
@@ -312,7 +312,7 @@ def mkSimpleThunk (type : Expr) : Expr :=
 
 def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr :=
   -- let x := x.eraseMacroScopes
-  Expr.letE x t v b $ mkDataForLet (mixUSizeHash 41 $ mixUSizeHash (hash t) $ mixUSizeHash (hash v) (hash b))
+  Expr.letE x t v b $ mkDataForLet (mixUSizeHash 41 $ mixUSizeHash (hashUSize t) $ mixUSizeHash (hashUSize v) (hashUSize b))
     (Nat.max (Nat.max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1))
     (t.hasFVar || v.hasFVar || b.hasFVar)
     (t.hasExprMVar || v.hasExprMVar || b.hasExprMVar)
@@ -719,7 +719,7 @@ protected def hash : ExprStructEq → USize
   | ⟨e⟩ => e.hash
 
 instance : BEq ExprStructEq := ⟨ExprStructEq.beq⟩
-instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩
+instance : HashableUSize ExprStructEq := ⟨ExprStructEq.hash⟩
 instance : ToString ExprStructEq := ⟨fun e => toString e.val⟩
 
 end ExprStructEq
diff --git a/src/Lean/HeadIndex.lean b/src/Lean/HeadIndex.lean
index 6eb688e136..fa7bf42d47 100644
--- a/src/Lean/HeadIndex.lean
+++ b/src/Lean/HeadIndex.lean
@@ -21,16 +21,16 @@ inductive HeadIndex where
 namespace HeadIndex
 
 protected def HeadIndex.hash : HeadIndex → USize
-  | fvar fvarId         => mixUSizeHash 11 $ hash fvarId
-  | mvar mvarId         => mixUSizeHash 13 $ hash mvarId
-  | const constName     => mixUSizeHash 17 $ hash constName
-  | proj structName idx => mixUSizeHash 19 $ mixUSizeHash (hash structName) (hash idx)
-  | lit litVal          => mixUSizeHash 23 $ hash litVal
+  | fvar fvarId         => mixUSizeHash 11 $ hashUSize fvarId
+  | mvar mvarId         => mixUSizeHash 13 $ hashUSize mvarId
+  | const constName     => mixUSizeHash 17 $ hashUSize constName
+  | proj structName idx => mixUSizeHash 19 $ mixUSizeHash (hashUSize structName) (hashUSize idx)
+  | lit litVal          => mixUSizeHash 23 $ hashUSize litVal
   | sort                => 29
   | lam                 => 31
   | forallE             => 37
 
-instance : Hashable HeadIndex := ⟨HeadIndex.hash⟩
+instance : HashableUSize HeadIndex := ⟨HeadIndex.hash⟩
 
 end HeadIndex
 
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 98d53f560b..b40013739a 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -72,7 +72,7 @@ namespace Level
 protected def hash (u : Level) : USize :=
   u.data.hash
 
-instance : Hashable Level := ⟨Level.hash⟩
+instance : HashableUSize Level := ⟨Level.hash⟩
 
 def depth (u : Level) : Nat :=
   u.data.depth.toNat
@@ -94,21 +94,21 @@ def levelZero :=
   Level.zero $ mkData 2221 0 false false
 
 def mkLevelMVar (mvarId : Name) :=
-  Level.mvar mvarId $ mkData (mixUSizeHash 2237 $ hash mvarId) 0 true false
+  Level.mvar mvarId $ mkData (mixUSizeHash 2237 $ hashUSize mvarId) 0 true false
 
 def mkLevelParam (name : Name) :=
-  Level.param name $ mkData (mixUSizeHash 2239 $ hash name) 0 false true
+  Level.param name $ mkData (mixUSizeHash 2239 $ hashUSize name) 0 false true
 
 def mkLevelSucc (u : Level) :=
-  Level.succ u $ mkData (mixUSizeHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam
+  Level.succ u $ mkData (mixUSizeHash 2243 $ hashUSize u) (u.depth + 1) u.hasMVar u.hasParam
 
 def mkLevelMax (u v : Level) :=
-  Level.max u v $ mkData (mixUSizeHash 2251 $ mixUSizeHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
+  Level.max u v $ mkData (mixUSizeHash 2251 $ mixUSizeHash (hashUSize u) (hashUSize v)) (Nat.max u.depth v.depth + 1)
      (u.hasMVar || v.hasMVar)
      (u.hasParam || v.hasParam)
 
 def mkLevelIMax (u v : Level) :=
-  Level.imax u v $ mkData (mixUSizeHash 2267 $ mixUSizeHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
+  Level.imax u v $ mkData (mixUSizeHash 2267 $ mixUSizeHash (hashUSize u) (hashUSize v)) (Nat.max u.depth v.depth + 1)
      (u.hasMVar || v.hasMVar)
      (u.hasParam || v.hasParam)
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index b82b050c0f..7e6183d74a 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -80,8 +80,8 @@ structure InfoCacheKey where
   deriving Inhabited, BEq
 
 namespace InfoCacheKey
-instance : Hashable InfoCacheKey :=
-  ⟨fun ⟨transparency, expr, nargs⟩ => mixUSizeHash (hash transparency) <| mixUSizeHash (hash expr) (hash nargs)⟩
+instance : HashableUSize InfoCacheKey :=
+  ⟨fun ⟨transparency, expr, nargs⟩ => mixUSizeHash (hashUSize transparency) <| mixUSizeHash (hashUSize expr) (hashUSize nargs)⟩
 end InfoCacheKey
 
 open Std (PersistentArray PersistentHashMap)
diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean
index d301e5847a..655893cf99 100644
--- a/src/Lean/Meta/DiscrTreeTypes.lean
+++ b/src/Lean/Meta/DiscrTreeTypes.lean
@@ -21,14 +21,14 @@ inductive Key where
   deriving Inhabited, BEq
 
 protected def Key.hash : Key → USize
-  | Key.const n a => mixUSizeHash 5237 $ mixUSizeHash (hash n) (hash a)
-  | Key.fvar n a  => mixUSizeHash 3541 $ mixUSizeHash (hash n) (hash a)
-  | Key.lit v     => mixUSizeHash 1879 $ hash v
+  | Key.const n a => mixUSizeHash 5237 $ mixUSizeHash (hashUSize n) (hashUSize a)
+  | Key.fvar n a  => mixUSizeHash 3541 $ mixUSizeHash (hashUSize n) (hashUSize a)
+  | Key.lit v     => mixUSizeHash 1879 $ hashUSize v
   | Key.star      => 7883
   | Key.other     => 2411
   | Key.arrow     => 17
 
-instance : Hashable Key := ⟨Key.hash⟩
+instance : HashableUSize Key := ⟨Key.hash⟩
 
 inductive Trie (α : Type) where
   | node (vs : Array α) (children : Array (Key × Trie α)) : Trie α
diff --git a/src/Lean/Meta/TransparencyMode.lean b/src/Lean/Meta/TransparencyMode.lean
index 4d07fc9ddb..7988bccadc 100644
--- a/src/Lean/Meta/TransparencyMode.lean
+++ b/src/Lean/Meta/TransparencyMode.lean
@@ -17,7 +17,7 @@ def hash : TransparencyMode → USize
   | reducible => 13
   | instances => 17
 
-instance : Hashable TransparencyMode := ⟨hash⟩
+instance : HashableUSize TransparencyMode := ⟨hash⟩
 
 def lt : TransparencyMode → TransparencyMode → Bool
   | reducible, default   => true
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index 8b507d0837..7dd40544ca 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -33,30 +33,30 @@ open Std (HashMap)
 
 /-- Adapter for implementing `MonadCache` interface using `HashMap`s.
     We just have to specify how to extract/modify the `HashMap`. -/
-class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [Hashable α] where
+class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [HashableUSize α] where
   getCache    : m (HashMap α β)
   modifyCache : (HashMap α β → HashMap α β) → m Unit
 
 namespace MonadHashMapCacheAdapter
 
-@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
+@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
   let c ← getCache
   pure (c.find? a)
 
-@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
+@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
   modifyCache fun s => s.insert a b
 
-instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
+instance {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
   findCached? := MonadHashMapCacheAdapter.findCached?
   cache       := MonadHashMapCacheAdapter.cache
 
 end MonadHashMapCacheAdapter
 
-def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [Hashable α] := StateRefT (HashMap α β) m
+def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [HashableUSize α] := StateRefT (HashMap α β) m
 
 namespace MonadCacheT
 
-variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
+variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [HashableUSize α] [MonadLiftT (ST ω) m] [Monad m]
 
 instance  : MonadHashMapCacheAdapter α β (MonadCacheT α β m) where
   getCache := (get : StateRefT' ..)
@@ -75,11 +75,11 @@ instance [MonadRef m] : MonadRef (MonadCacheT α β m) := inferInstanceAs (Monad
 end MonadCacheT
 
 /- Similar to `MonadCacheT`, but using `StateT` instead of `StateRefT` -/
-def MonadStateCacheT (α β : Type) (m : Type → Type) [BEq α] [Hashable α] := StateT (HashMap α β) m
+def MonadStateCacheT (α β : Type) (m : Type → Type) [BEq α] [HashableUSize α] := StateT (HashMap α β) m
 
 namespace MonadStateCacheT
 
-variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
+variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [HashableUSize α] [MonadLiftT (ST ω) m] [Monad m]
 
 instance  : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) where
   getCache := (get : StateT ..)
diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean
index 887e2926d9..f63bd0f0df 100644
--- a/src/Lean/Util/SCC.lean
+++ b/src/Lean/Util/SCC.lean
@@ -14,7 +14,7 @@ namespace Lean.SCC
 open Std
 
 section
-variable (α : Type) [BEq α] [Hashable α]
+variable (α : Type) [BEq α] [HashableUSize α]
 
 structure Data where
   index?   : Option Nat := none
@@ -30,7 +30,7 @@ structure State where
 abbrev M := StateM (State α)
 end
 
-variable {α : Type} [BEq α] [Hashable α]
+variable {α : Type} [BEq α] [HashableUSize α]
 
 private def getDataOf (a : α) : M α Data := do
   let s ← get
diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean
index 5b4a852247..4571ed1268 100644
--- a/src/Std/Data/HashMap.lean
+++ b/src/Std/Data/HashMap.lean
@@ -53,46 +53,46 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
 @[inline] def forM {m : Type w → Type w} [Monad m] (f : α → β → m PUnit) (h : HashMapImp α β) : m PUnit :=
   forBucketsM h.buckets f
 
-def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
+def findEntry? [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     (buckets.val.uget i h).findEntry? a
 
-def find? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
+def find? [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Option β :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     (buckets.val.uget i h).find? a
 
-def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
+def contains [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Bool :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     (buckets.val.uget i h).contains a
 
 -- TODO: remove `partial` by using well-founded recursion
-partial def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
+partial def moveEntries [HashableUSize α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
   if h : i < source.size then
      let idx : Fin source.size := ⟨i, h⟩
      let es  : AssocList α β   := source.get idx
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
      let source                := source.set idx AssocList.nil
-     let target                := es.foldl (reinsertAux hash) target
+     let target                := es.foldl (reinsertAux hashUSize) target
      moveEntries (i+1) source target
   else target
 
-def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
+def expand [HashableUSize α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let nbuckets := buckets.val.size * 2
   have : nbuckets > 0 := Nat.mulPos buckets.property (by decide)
   let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, by simp; assumption⟩
   { size    := size,
     buckets := moveEntries 0 buckets.val new_buckets }
 
-def insert [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
+def insert [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
   match m with
   | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     let bkt    := buckets.val.uget i h
     if bkt.contains a then
       ⟨size, buckets.update i (bkt.replace a b) h⟩
@@ -104,31 +104,31 @@ def insert [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : Has
       else
         expand size' buckets'
 
-def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
+def erase [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
   match m with
   | ⟨ size, buckets ⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     let bkt    := buckets.val.uget i h
     if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
     else m
 
-inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop where
+inductive WellFormed [BEq α] [HashableUSize α] : HashMapImp α β → Prop where
   | mkWff     : ∀ n,                    WellFormed (mkHashMapImp n)
   | insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b)
   | eraseWff  : ∀ m a,   WellFormed m → WellFormed (erase m a)
 
 end HashMapImp
 
-def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
+def HashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] :=
   { m : HashMapImp α β // m.WellFormed }
 
 open Std.HashMapImp
 
-def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8) : HashMap α β :=
+def mkHashMap {α : Type u} {β : Type v} [BEq α] [HashableUSize α] (nbuckets := 8) : HashMap α β :=
   ⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩
 
 namespace HashMap
-variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
+variable {α : Type u} {β : Type v} [BEq α] [HashableUSize α]
 
 instance : Inhabited (HashMap α β) where
   default := mkHashMap
diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean
index 913fd4a9f2..e7ec3ad4b9 100644
--- a/src/Std/Data/HashSet.lean
+++ b/src/Std/Data/HashSet.lean
@@ -46,40 +46,40 @@ def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
 @[inline] def fold {δ : Type w} (f : δ → α → δ) (d : δ) (m : HashSetImp α) : δ :=
   foldBuckets m.buckets d f
 
-def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
+def find? [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : Option α :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     (buckets.val.uget i h).find? (fun a' => a == a')
 
-def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
+def contains [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : Bool :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     (buckets.val.uget i h).contains a
 
 -- TODO: remove `partial` by using well-founded recursion
-partial def moveEntries [Hashable α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
+partial def moveEntries [HashableUSize α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
   if h : i < source.size then
      let idx : Fin source.size := ⟨i, h⟩
      let es  : List α   := source.get idx
      -- We remove `es` from `source` to make sure we can reuse its memory cells when performing es.foldl
      let source                := source.set idx []
-     let target                := es.foldl (reinsertAux hash) target
+     let target                := es.foldl (reinsertAux hashUSize) target
      moveEntries (i+1) source target
   else target
 
-def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
+def expand [HashableUSize α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
   let nbuckets := buckets.val.size * 2
   have : nbuckets > 0 := Nat.mulPos buckets.property (by decide)
   let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], by rw [Array.size_mkArray]; assumption⟩
   { size    := size,
     buckets := moveEntries 0 buckets.val new_buckets }
 
-def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
+def insert [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp α :=
   match m with
   | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     let bkt    := buckets.val.uget i h
     if bkt.contains a
     then ⟨size, buckets.update i (bkt.replace a a) h⟩
@@ -90,31 +90,31 @@ def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :
       then { size := size', buckets := buckets' }
       else expand size' buckets'
 
-def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
+def erase [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp α :=
   match m with
   | ⟨ size, buckets ⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hash a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
     let bkt    := buckets.val.uget i h
     if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩
     else m
 
-inductive WellFormed [BEq α] [Hashable α] : HashSetImp α → Prop where
+inductive WellFormed [BEq α] [HashableUSize α] : HashSetImp α → Prop where
   | mkWff     : ∀ n,                  WellFormed (mkHashSetImp n)
   | insertWff : ∀ m a, WellFormed m → WellFormed (insert m a)
   | eraseWff  : ∀ m a, WellFormed m → WellFormed (erase m a)
 
 end HashSetImp
 
-def HashSet (α : Type u) [BEq α] [Hashable α] :=
+def HashSet (α : Type u) [BEq α] [HashableUSize α] :=
   { m : HashSetImp α // m.WellFormed }
 
 open HashSetImp
 
-def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α :=
+def mkHashSet {α : Type u} [BEq α] [HashableUSize α] (nbuckets := 8) : HashSet α :=
   ⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩
 
 namespace HashSet
-variable {α : Type u} [BEq α] [Hashable α]
+variable {α : Type u} [BEq α] [HashableUSize α]
 
 instance : Inhabited (HashSet α) where
   default := mkHashSet
diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean
index 15a864b6ac..f7cb670e69 100644
--- a/src/Std/Data/PersistentHashMap.lean
+++ b/src/Std/Data/PersistentHashMap.lean
@@ -31,21 +31,21 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) :=
 
 end PersistentHashMap
 
-structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
+structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] where
   root    : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
   size    : Nat                        := 0
 
-abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
+abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] := PersistentHashMap α β
 
 namespace PersistentHashMap
 variable {α : Type u} {β : Type v}
 
-def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
+def empty [BEq α] [HashableUSize α] : PersistentHashMap α β := {}
 
-def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
+def isEmpty [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : Bool :=
   m.size == 0
 
-instance [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
+instance [BEq α] [HashableUSize α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
 
 def mkEmptyEntries {α β} : Node α β :=
   Node.entries mkEmptyEntriesArray
@@ -98,7 +98,7 @@ def mkCollisionNode (k₁ : α) (v₁ : β) (k₂ : α) (v₂ : β) : Node α β
   let vs := (vs.push v₁).push v₂
   Node.collision ks vs rfl
 
-partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β
+partial def insertAux [BEq α] [HashableUSize α] : Node α β → USize → USize → α → β → Node α β
   | Node.collision keys vals heq, _, depth, k, v =>
     let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v
     if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val
@@ -109,7 +109,7 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize 
           if h : i < keys.size then
             let k := keys.get ⟨i, h⟩
             let v := vals.get ⟨i, heq ▸ h⟩
-            let h := hash k
+            let h := hashUSize k
             let h := div2Shift h (shift * (depth - 1))
             traverse (i+1) (insertAux entries h depth k v)
           else
@@ -125,8 +125,8 @@ partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize 
         if k == k' then Entry.entry k v
         else Entry.ref $ mkCollisionNode k' v' k v
 
-def insert [BEq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β
-  | { root := n, size := sz }, k, v => { root := insertAux n (hash k) 1 k v, size := sz + 1 }
+def insert [BEq α] [HashableUSize α] : PersistentHashMap α β → α → β → PersistentHashMap α β
+  | { root := n, size := sz }, k, v => { root := insertAux n (hashUSize k) 1 k v, size := sz + 1 }
 
 partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Option β :=
   if h : i < keys.size then
@@ -144,16 +144,16 @@ partial def findAux [BEq α] : Node α β → USize → α → Option β
     | Entry.entry k' v => if k == k' then some v else none
   | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k
 
-def find? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option β
-  | { root := n, .. }, k => findAux n (hash k) k
+def find? [BEq α] [HashableUSize α] : PersistentHashMap α β → α → Option β
+  | { root := n, .. }, k => findAux n (hashUSize k) k
 
-@[inline] def getOp [BEq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β :=
+@[inline] def getOp [BEq α] [HashableUSize α] (self : PersistentHashMap α β) (idx : α) : Option β :=
   self.find? idx
 
-@[inline] def findD [BEq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
+@[inline] def findD [BEq α] [HashableUSize α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 
-@[inline] def find! [BEq α] [Hashable α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
+@[inline] def find! [BEq α] [HashableUSize α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
   match m.find? a with
   | some b => b
   | none   => panic! "key is not in the map"
@@ -174,8 +174,8 @@ partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α 
     | Entry.entry k' v => if k == k' then some (k', v) else none
   | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k
 
-def findEntry? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β)
-  | { root := n, .. }, k => findEntryAux n (hash k) k
+def findEntry? [BEq α] [HashableUSize α] : PersistentHashMap α β → α → Option (α × β)
+  | { root := n, .. }, k => findEntryAux n (hashUSize k) k
 
 partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) (i : Nat) (k : α) : Bool :=
   if h : i < keys.size then
@@ -193,8 +193,8 @@ partial def containsAux [BEq α] : Node α β → USize → α → Bool
     | Entry.entry k' v => k == k'
   | Node.collision keys vals heq, _, k => containsAtAux keys vals heq 0 k
 
-def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
-  | { root := n, .. }, k => containsAux n (hash k) k
+def contains [BEq α] [HashableUSize α] : PersistentHashMap α β → α → Bool
+  | { root := n, .. }, k => containsAux n (hashUSize k) k
 
 partial def isUnaryEntries (a : Array (Entry α β (Node α β))) (i : Nat) (acc : Option (α × β)) : Option (α × β) :=
   if h : i < a.size then
@@ -240,9 +240,9 @@ partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bo
         | none        => (Node.entries (entries.set! j (Entry.ref newNode)), true)
         | some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true)
 
-def erase [BEq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
+def erase [BEq α] [HashableUSize α] : PersistentHashMap α β → α → PersistentHashMap α β
   | { root := n, size := sz }, k =>
-    let h := hash k
+    let h := hashUSize k
     let (n, del) := eraseAux n h k
     { root := n, size := if del then sz - 1 else sz }
 
@@ -267,17 +267,17 @@ variable {σ : Type w}
     | Entry.ref node  => foldlMAux f node acc)
     acc
 
-@[specialize] def foldlM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
+@[specialize] def foldlM [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
   foldlMAux f map.root init
 
-@[specialize] def forM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
+@[specialize] def forM [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
   map.foldlM (fun _ => f) ⟨⟩
 
-@[specialize] def foldl [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
+@[specialize] def foldl [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
   Id.run $ map.foldlM f init
 end
 
-def toList [BEq α] [Hashable α] (m : PersistentHashMap α β) : List (α × β) :=
+def toList [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : List (α × β) :=
   m.foldl (init := []) fun ps k v => (k, v) :: ps
 
 structure Stats where
@@ -304,7 +304,7 @@ partial def collectStats : Node α β → Stats → Nat → Stats
       | Entry.entry _ _ => stats)
       stats
 
-def stats [BEq α] [Hashable α] (m : PersistentHashMap α β) : Stats :=
+def stats [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : Stats :=
   collectStats m.root {} 1
 
 def Stats.toString (s : Stats) : String :=
diff --git a/src/Std/Data/PersistentHashSet.lean b/src/Std/Data/PersistentHashSet.lean
index e5de05e8ca..9a7fff20ca 100644
--- a/src/Std/Data/PersistentHashSet.lean
+++ b/src/Std/Data/PersistentHashSet.lean
@@ -8,14 +8,14 @@ import Std.Data.PersistentHashMap
 namespace Std
 universes u v
 
-structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] where
+structure PersistentHashSet (α : Type u) [BEq α] [HashableUSize α] where
   (set : PersistentHashMap α Unit)
 
-abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α
+abbrev PHashSet (α : Type u) [BEq α] [HashableUSize α] := PersistentHashSet α
 
 namespace PersistentHashSet
 
-variable {α : Type u} [BEq α] [Hashable α]
+variable {α : Type u} [BEq α] [HashableUSize α]
 
 @[inline] def isEmpty (s : PersistentHashSet α) : Bool :=
   s.set.isEmpty