From 7424f9c8b0acbf03d717c75fdf08679b0ae84e54 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 2 Jun 2021 09:58:46 -0700
Subject: [PATCH] chore: remove `HashableUSize`

---
 src/Init/Prelude.lean               | 11 -------
 src/Lean/Data/SMap.lean             |  8 ++---
 src/Lean/Exception.lean             |  2 +-
 src/Lean/Expr.lean                  | 34 ++++++++++----------
 src/Lean/Level.lean                 | 12 +++----
 src/Lean/Util/MonadCache.lean       | 16 ++++-----
 src/Lean/Util/SCC.lean              |  4 +--
 src/Std/Data/HashMap.lean           | 38 +++++++++++-----------
 src/Std/Data/HashSet.lean           | 34 ++++++++++----------
 src/Std/Data/PersistentHashMap.lean | 50 ++++++++++++++---------------
 src/Std/Data/PersistentHashSet.lean |  6 ++--
 src/Std/ShareCommon.lean            |  6 ++--
 src/kernel/expr.cpp                 |  2 +-
 src/runtime/sharecommon.cpp         |  2 +-
 14 files changed, 107 insertions(+), 118 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index e2a178863a..e49640f52a 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1587,11 +1587,6 @@ instance nonBacktrackable : Backtrackable PUnit σ where
 
 end EStateM
 
-class HashableUSize (α : Sort u) where
-  hashUSize : α → USize
-
-export HashableUSize (hashUSize)
-
 class Hashable (α : Sort u) where
   hash : α → UInt64
 
@@ -1603,15 +1598,9 @@ constant UInt64.toUSize (u : UInt64) : USize
 @[extern c inline "(uint64_t)#1"]
 constant USize.toUInt64 (u : USize) : UInt64
 
-instance [Hashable α] : HashableUSize α where
-  hashUSize n := hash n |>.toUSize
-
 @[extern "lean_uint64_mix_hash"]
 constant mixHash (u₁ u₂ : UInt64) : UInt64
 
-@[extern "lean_usize_mix_hash"]
-constant mixUSizeHash (u₁ u₂ : USize) : USize
-
 @[extern "lean_string_hash"]
 protected constant String.hash (s : @& String) : UInt64
 
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index 9bb1cd68c6..07021ca686 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 α] [HashableUSize α] where
+structure SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
   stage₁ : Bool         := true
   map₁   : HashMap α β  := {}
   map₂   : PHashMap α β := {}
 
 namespace SMap
-variable {α : Type u} {β : Type v} [BEq α] [HashableUSize α]
+variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
 
 instance : Inhabited (SMap α β) := ⟨{}⟩
 def empty : SMap α β := {}
@@ -92,10 +92,10 @@ def toList (m : SMap α β) : List (α × β) :=
 
 end SMap
 
-def List.toSMap [BEq α] [HashableUSize α] (es : List (α × β)) : SMap α β :=
+def List.toSMap [BEq α] [Hashable α] (es : List (α × β)) : SMap α β :=
   es.foldl (init := {}) fun s (a, b) => s.insert a b
 
-instance {_ : BEq α} {_ : HashableUSize α} [Repr α] [Repr β] : Repr (SMap α β) where
+instance {_ : BEq α} {_ : Hashable α} [Repr α] [Repr β] : Repr (SMap α β) where
   reprPrec v prec := Repr.addAppParen (reprArg v.toList ++ ".toSMap") prec
 
 end Lean
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index 0f90ecca30..df2a590ed4 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 α] [HashableUSize α] [Monad m] [STWorld ω m] [MonadRecDepth m] : MonadRecDepth (MonadCacheT α β m) :=
+instance [BEq α] [Hashable α] [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 8481d68652..8dc107aac0 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -121,7 +121,7 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
   | BinderInfo.auxDecl        => 4
 
 @[inline] private def Expr.mkDataCore
-    (h : USize) (looseBVarRange : Nat)
+    (h : UInt64) (looseBVarRange : Nat)
     (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) (bi : BinderInfo)
     : Expr.Data :=
   if looseBVarRange > Nat.pow 2 24 - 1 then panic! "bound variable index is too big"
@@ -137,13 +137,13 @@ def BinderInfo.toUInt64 : BinderInfo → UInt64
       looseBVarRange.toUInt64.shiftLeft 40
     r
 
-def Expr.mkData (h : USize) (looseBVarRange : Nat := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data :=
+def Expr.mkData (h : UInt64) (looseBVarRange : Nat := 0) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool := false) : Expr.Data :=
   Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false BinderInfo.default
 
-def Expr.mkDataForBinder (h : USize) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
+def Expr.mkDataForBinder (h : UInt64) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam : Bool) (bi : BinderInfo) : Expr.Data :=
   Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam false bi
 
-def Expr.mkDataForLet (h : USize) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
+def Expr.mkDataForLet (h : UInt64) (looseBVarRange : Nat) (hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet : Bool) : Expr.Data :=
   Expr.mkDataCore h looseBVarRange hasFVar hasExprMVar hasLevelMVar hasLevelParam nonDepLet BinderInfo.default
 
 open Expr
@@ -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 := hashUSize
+@[export lean_expr_hash] def hashEx : Expr → UInt64 := hash
 @[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 (hashUSize l))
+  Expr.lit l $ mkData (mixHash 3 (hash 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 (hashUSize n) (hashUSize lvls)) 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
+  Expr.const n lvls $ mkData (mixHash 5 $ mixHash (hash n) (hash 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 $ hashUSize idx) (idx+1)
+  Expr.bvar idx $ mkData (mixHash 7 $ hash idx) (idx+1)
 
 def mkSort (lvl : Level) : Expr :=
-  Expr.sort lvl $ mkData (mixUSizeHash 11 $ hashUSize lvl) 0 false false lvl.hasMVar lvl.hasParam
+  Expr.sort lvl $ mkData (mixHash 11 $ hash lvl) 0 false false lvl.hasMVar lvl.hasParam
 
 def mkFVar (fvarId : FVarId) : Expr :=
-  Expr.fvar fvarId $ mkData (mixUSizeHash 13 $ hashUSize fvarId) 0 true
+  Expr.fvar fvarId $ mkData (mixHash 13 $ hash fvarId) 0 true
 
 def mkMVar (fvarId : MVarId) : Expr :=
-  Expr.mvar fvarId $ mkData (mixUSizeHash 17 $ hashUSize fvarId) 0 false true
+  Expr.mvar fvarId $ mkData (mixHash 17 $ hash fvarId) 0 false true
 
 def mkMData (d : MData) (e : Expr) : Expr :=
-  Expr.mdata d e $ mkData (mixUSizeHash 19 $ hashUSize e) e.looseBVarRange e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
+  Expr.mdata d e $ mkData (mixHash 19 $ hash 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 (hashUSize s) $ mixUSizeHash (hashUSize i) (hashUSize e))
+  Expr.proj s i e $ mkData (mixHash 23 $ mixHash (hash s) $ mixHash (hash i) (hash 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 (hashUSize f) (hashUSize a))
+  Expr.app f a $ mkData (mixHash 29 $ mixHash (hash f) (hash 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 (hashUSize t) (hashUSize b))
+  Expr.lam x t b $ mkDataForBinder (mixHash 31 $ mixHash (hash t) (hash 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 (hashUSize t) (hashUSize b))
+  Expr.forallE x t b $ mkDataForBinder (mixHash 37 $ mixHash (hash t) (hash 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 (hashUSize t) $ mixUSizeHash (hashUSize v) (hashUSize b))
+  Expr.letE x t v b $ mkDataForLet (mixHash 41 $ mixHash (hash t) $ mixHash (hash v) (hash b))
     (Nat.max (Nat.max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1))
     (t.hasFVar || v.hasFVar || b.hasFVar)
     (t.hasExprMVar || v.hasExprMVar || b.hasExprMVar)
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index a826616921..b1b8c31072 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -42,7 +42,7 @@ def Level.Data.hasMVar (c : Level.Data) : Bool :=
 def Level.Data.hasParam (c : Level.Data) : Bool :=
   ((c.shiftRight 33).land 1) == 1
 
-def Level.mkData (h : USize) (depth : Nat) (hasMVar hasParam : Bool) : Level.Data :=
+def Level.mkData (h : UInt64) (depth : Nat) (hasMVar hasParam : Bool) : Level.Data :=
   if depth > Nat.pow 2 24 - 1 then panic! "universe level depth is too big"
   else
     let r : UInt64 := h.toUInt32.toUInt64 + hasMVar.toUInt64.shiftLeft 32 + hasParam.toUInt64.shiftLeft 33 + depth.toUInt64.shiftLeft 40
@@ -94,21 +94,21 @@ def levelZero :=
   Level.zero $ mkData 2221 0 false false
 
 def mkLevelMVar (mvarId : Name) :=
-  Level.mvar mvarId $ mkData (mixUSizeHash 2237 $ hashUSize mvarId) 0 true false
+  Level.mvar mvarId $ mkData (mixHash 2237 $ hash mvarId) 0 true false
 
 def mkLevelParam (name : Name) :=
-  Level.param name $ mkData (mixUSizeHash 2239 $ hashUSize name) 0 false true
+  Level.param name $ mkData (mixHash 2239 $ hash name) 0 false true
 
 def mkLevelSucc (u : Level) :=
-  Level.succ u $ mkData (mixUSizeHash 2243 $ hashUSize u) (u.depth + 1) u.hasMVar u.hasParam
+  Level.succ u $ mkData (mixHash 2243 $ hash u) (u.depth + 1) u.hasMVar u.hasParam
 
 def mkLevelMax (u v : Level) :=
-  Level.max u v $ mkData (mixUSizeHash 2251 $ mixUSizeHash (hashUSize u) (hashUSize v)) (Nat.max u.depth v.depth + 1)
+  Level.max u v $ mkData (mixHash 2251 $ mixHash (hash u) (hash 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 (hashUSize u) (hashUSize v)) (Nat.max u.depth v.depth + 1)
+  Level.imax u v $ mkData (mixHash 2267 $ mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
      (u.hasMVar || v.hasMVar)
      (u.hasParam || v.hasParam)
 
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index 7dd40544ca..8b507d0837 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 α] [HashableUSize α] where
+class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [Hashable α] where
   getCache    : m (HashMap α β)
   modifyCache : (HashMap α β → HashMap α β) → m Unit
 
 namespace MonadHashMapCacheAdapter
 
-@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
+@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do
   let c ← getCache
   pure (c.find? a)
 
-@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
+@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
   modifyCache fun s => s.insert a b
 
-instance {α β : Type} {m : Type → Type} [BEq α] [HashableUSize α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
+instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
   findCached? := MonadHashMapCacheAdapter.findCached?
   cache       := MonadHashMapCacheAdapter.cache
 
 end MonadHashMapCacheAdapter
 
-def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [HashableUSize α] := StateRefT (HashMap α β) m
+def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [Hashable α] := StateRefT (HashMap α β) m
 
 namespace MonadCacheT
 
-variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [HashableUSize α] [MonadLiftT (ST ω) m] [Monad m]
+variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [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 α] [HashableUSize α] := StateT (HashMap α β) m
+def MonadStateCacheT (α β : Type) (m : Type → Type) [BEq α] [Hashable α] := StateT (HashMap α β) m
 
 namespace MonadStateCacheT
 
-variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [HashableUSize α] [MonadLiftT (ST ω) m] [Monad m]
+variable {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [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 f63bd0f0df..887e2926d9 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 α] [HashableUSize α]
+variable (α : Type) [BEq α] [Hashable α]
 
 structure Data where
   index?   : Option Nat := none
@@ -30,7 +30,7 @@ structure State where
 abbrev M := StateM (State α)
 end
 
-variable {α : Type} [BEq α] [HashableUSize α]
+variable {α : Type} [BEq α] [Hashable α]
 
 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 4571ed1268..b0d76a8eab 100644
--- a/src/Std/Data/HashMap.lean
+++ b/src/Std/Data/HashMap.lean
@@ -31,8 +31,8 @@ variable {α : Type u} {β : Type v}
 def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
   ⟨u % n, USize.modn_lt _ h⟩
 
-@[inline] def reinsertAux (hashFn : α → USize) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
-  let ⟨i, h⟩ := mkIdx data.property (hashFn a)
+@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashMapBucket α β) (a : α) (b : β) : HashMapBucket α β :=
+  let ⟨i, h⟩ := mkIdx data.property (hashFn a |>.toUSize)
   data.update i (AssocList.cons a b (data.val.uget i h)) h
 
 @[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashMapBucket α β) (d : δ) (f : δ → α → β → m δ) : m δ :=
@@ -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 α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
+def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     (buckets.val.uget i h).findEntry? a
 
-def find? [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Option β :=
+def find? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     (buckets.val.uget i h).find? a
 
-def contains [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : Bool :=
+def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     (buckets.val.uget i h).contains a
 
 -- TODO: remove `partial` by using well-founded recursion
-partial def moveEntries [HashableUSize α] (i : Nat) (source : Array (AssocList α β)) (target : HashMapBucket α β) : HashMapBucket α β :=
+partial def moveEntries [Hashable α] (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 hashUSize) target
+     let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target
 
-def expand [HashableUSize α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
+def expand [Hashable α] (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 α] [HashableUSize α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
+def insert [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β :=
   match m with
   | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     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 α] [HashableUSize α] (m : HashMapImp α β) (a : α) (b : β)
       else
         expand size' buckets'
 
-def erase [BEq α] [HashableUSize α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
+def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β :=
   match m with
   | ⟨ size, buckets ⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     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 α] [HashableUSize α] : HashMapImp α β → Prop where
+inductive WellFormed [BEq α] [Hashable α] : 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 α] [HashableUSize α] :=
+def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
   { m : HashMapImp α β // m.WellFormed }
 
 open Std.HashMapImp
 
-def mkHashMap {α : Type u} {β : Type v} [BEq α] [HashableUSize α] (nbuckets := 8) : HashMap α β :=
+def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8) : HashMap α β :=
   ⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩
 
 namespace HashMap
-variable {α : Type u} {β : Type v} [BEq α] [HashableUSize α]
+variable {α : Type u} {β : Type v} [BEq α] [Hashable α]
 
 instance : Inhabited (HashMap α β) where
   default := mkHashMap
diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean
index e7ec3ad4b9..875816169e 100644
--- a/src/Std/Data/HashSet.lean
+++ b/src/Std/Data/HashSet.lean
@@ -30,8 +30,8 @@ variable {α : Type u}
 def mkIdx {n : Nat} (h : n > 0) (u : USize) : { u : USize // u.toNat < n } :=
   ⟨u % n, USize.modn_lt _ h⟩
 
-@[inline] def reinsertAux (hashFn : α → USize) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
-  let ⟨i, h⟩ := mkIdx data.property (hashFn a)
+@[inline] def reinsertAux (hashFn : α → UInt64) (data : HashSetBucket α) (a : α) : HashSetBucket α :=
+  let ⟨i, h⟩ := mkIdx data.property (hashFn a |>.toUSize)
   data.update i (a :: data.val.uget i h) h
 
 @[inline] def foldBucketsM {δ : Type w} {m : Type w → Type w} [Monad m] (data : HashSetBucket α) (d : δ) (f : δ → α → m δ) : m δ :=
@@ -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 α] [HashableUSize α] (m : HashSetImp α) (a : α) : Option α :=
+def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     (buckets.val.uget i h).find? (fun a' => a == a')
 
-def contains [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : Bool :=
+def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool :=
   match m with
   | ⟨_, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     (buckets.val.uget i h).contains a
 
 -- TODO: remove `partial` by using well-founded recursion
-partial def moveEntries [HashableUSize α] (i : Nat) (source : Array (List α)) (target : HashSetBucket α) : HashSetBucket α :=
+partial def moveEntries [Hashable α] (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 hashUSize) target
+     let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target
 
-def expand [HashableUSize α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
+def expand [Hashable α] (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 α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp α :=
+def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
   match m with
   | ⟨size, buckets⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     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 α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp
       then { size := size', buckets := buckets' }
       else expand size' buckets'
 
-def erase [BEq α] [HashableUSize α] (m : HashSetImp α) (a : α) : HashSetImp α :=
+def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α :=
   match m with
   | ⟨ size, buckets ⟩ =>
-    let ⟨i, h⟩ := mkIdx buckets.property (hashUSize a)
+    let ⟨i, h⟩ := mkIdx buckets.property (hash a |>.toUSize)
     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 α] [HashableUSize α] : HashSetImp α → Prop where
+inductive WellFormed [BEq α] [Hashable α] : 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 α] [HashableUSize α] :=
+def HashSet (α : Type u) [BEq α] [Hashable α] :=
   { m : HashSetImp α // m.WellFormed }
 
 open HashSetImp
 
-def mkHashSet {α : Type u} [BEq α] [HashableUSize α] (nbuckets := 8) : HashSet α :=
+def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α :=
   ⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩
 
 namespace HashSet
-variable {α : Type u} [BEq α] [HashableUSize α]
+variable {α : Type u} [BEq α] [Hashable α]
 
 instance : Inhabited (HashSet α) where
   default := mkHashSet
diff --git a/src/Std/Data/PersistentHashMap.lean b/src/Std/Data/PersistentHashMap.lean
index f7cb670e69..58526b5b27 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 α] [HashableUSize α] where
+structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] where
   root    : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray
   size    : Nat                        := 0
 
-abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [HashableUSize α] := PersistentHashMap α β
+abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β
 
 namespace PersistentHashMap
 variable {α : Type u} {β : Type v}
 
-def empty [BEq α] [HashableUSize α] : PersistentHashMap α β := {}
+def empty [BEq α] [Hashable α] : PersistentHashMap α β := {}
 
-def isEmpty [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : Bool :=
+def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool :=
   m.size == 0
 
-instance [BEq α] [HashableUSize α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩
+instance [BEq α] [Hashable α] : 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 α] [HashableUSize α] : Node α β → USize → USize → α → β → Node α β
+partial def insertAux [BEq α] [Hashable α] : 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 α] [HashableUSize α] : Node α β → USize → USi
           if h : i < keys.size then
             let k := keys.get ⟨i, h⟩
             let v := vals.get ⟨i, heq ▸ h⟩
-            let h := hashUSize k
+            let h := hash k |>.toUSize
             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 α] [HashableUSize α] : Node α β → USize → USi
         if k == k' then Entry.entry k v
         else Entry.ref $ mkCollisionNode k' v' k v
 
-def insert [BEq α] [HashableUSize α] : PersistentHashMap α β → α → β → PersistentHashMap α β
-  | { root := n, size := sz }, k, v => { root := insertAux n (hashUSize k) 1 k v, size := sz + 1 }
+def insert [BEq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β
+  | { root := n, size := sz }, k, v => { root := insertAux n (hash k |>.toUSize) 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 α] [HashableUSize α] : PersistentHashMap α β → α → Option β
-  | { root := n, .. }, k => findAux n (hashUSize k) k
+def find? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option β
+  | { root := n, .. }, k => findAux n (hash k |>.toUSize) k
 
-@[inline] def getOp [BEq α] [HashableUSize α] (self : PersistentHashMap α β) (idx : α) : Option β :=
+@[inline] def getOp [BEq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β :=
   self.find? idx
 
-@[inline] def findD [BEq α] [HashableUSize α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
+@[inline] def findD [BEq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
 
-@[inline] def find! [BEq α] [HashableUSize α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β :=
+@[inline] def find! [BEq α] [Hashable α] [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 α] [HashableUSize α] : PersistentHashMap α β → α → Option (α × β)
-  | { root := n, .. }, k => findEntryAux n (hashUSize k) k
+def findEntry? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β)
+  | { root := n, .. }, k => findEntryAux n (hash k |>.toUSize) 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 α] [HashableUSize α] : PersistentHashMap α β → α → Bool
-  | { root := n, .. }, k => containsAux n (hashUSize k) k
+def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool
+  | { root := n, .. }, k => containsAux n (hash k |>.toUSize) 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 α] [HashableUSize α] : PersistentHashMap α β → α → PersistentHashMap α β
+def erase [BEq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β
   | { root := n, size := sz }, k =>
-    let h := hashUSize k
+    let h := hash k |>.toUSize
     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 α] [HashableUSize α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
+@[specialize] def foldlM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (init : σ) : m σ :=
   foldlMAux f map.root init
 
-@[specialize] def forM [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
+@[specialize] def forM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit :=
   map.foldlM (fun _ => f) ⟨⟩
 
-@[specialize] def foldl [BEq α] [HashableUSize α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
+@[specialize] def foldl [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (init : σ) : σ :=
   Id.run $ map.foldlM f init
 end
 
-def toList [BEq α] [HashableUSize α] (m : PersistentHashMap α β) : List (α × β) :=
+def toList [BEq α] [Hashable α] (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 α] [HashableUSize α] (m : PersistentHashMap α β) : Stats :=
+def stats [BEq α] [Hashable α] (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 9a7fff20ca..e5de05e8ca 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 α] [HashableUSize α] where
+structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] where
   (set : PersistentHashMap α Unit)
 
-abbrev PHashSet (α : Type u) [BEq α] [HashableUSize α] := PersistentHashSet α
+abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α
 
 namespace PersistentHashSet
 
-variable {α : Type u} [BEq α] [HashableUSize α]
+variable {α : Type u} [BEq α] [Hashable α]
 
 @[inline] def isEmpty (s : PersistentHashSet α) : Bool :=
   s.set.isEmpty
diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean
index 42c1c6604a..0da14f9e70 100644
--- a/src/Std/ShareCommon.lean
+++ b/src/Std/ShareCommon.lean
@@ -23,14 +23,14 @@ abbrev Object : Type := NonScalar
 unsafe def Object.ptrEq (a b : Object) : Bool :=
   ptrAddrUnsafe a == ptrAddrUnsafe b
 
-unsafe def Object.ptrHash (a : Object) : USize :=
-  ptrAddrUnsafe a
+unsafe abbrev Object.ptrHash (a : Object) : UInt64 :=
+  ptrAddrUnsafe a |>.toUInt64
 
 @[extern "lean_sharecommon_eq"]
 unsafe constant Object.eq (a b : @& Object) : Bool
 
 @[extern "lean_sharecommon_hash"]
-unsafe constant Object.hash (a : @& Object) : USize
+unsafe constant Object.hash (a : @& Object) : UInt64
 
 unsafe def ObjectMap : Type := @HashMap Object Object ⟨Object.ptrEq⟩ ⟨Object.ptrHash⟩
 unsafe def ObjectSet : Type := @HashSet Object ⟨Object.eq⟩ ⟨Object.hash⟩
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 50a9df8b6e..577481ea33 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -78,7 +78,7 @@ binder_info binding_info(expr const & e) { return static_cast<binder_info>(lean_
 extern "C" object * lean_lit_type(obj_arg e);
 expr lit_type(literal const & lit) { return expr(lean_lit_type(lit.to_obj_arg())); }
 
-extern "C" usize lean_expr_hash(obj_arg e);
+extern "C" uint64_t lean_expr_hash(obj_arg e);
 unsigned hash(expr const & e) { return lean_expr_hash(e.to_obj_arg()); }
 
 extern "C" uint8 lean_expr_has_fvar(obj_arg e);
diff --git a/src/runtime/sharecommon.cpp b/src/runtime/sharecommon.cpp
index a749d22e9b..5a1545c41f 100644
--- a/src/runtime/sharecommon.cpp
+++ b/src/runtime/sharecommon.cpp
@@ -25,7 +25,7 @@ extern "C" uint8 lean_sharecommon_eq(b_obj_arg o1, b_obj_arg o2) {
     return memcmp(reinterpret_cast<char*>(o1) + header_sz, reinterpret_cast<char*>(o2) + header_sz, sz1 - header_sz) == 0;
 }
 
-extern "C" usize lean_sharecommon_hash(b_obj_arg o) {
+extern "C" uint64_t lean_sharecommon_hash(b_obj_arg o) {
     lean_assert(!lean_is_scalar(o));
     size_t sz = lean_object_byte_size(o);
     size_t header_sz = sizeof(lean_object);