diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index ea942751c2..9629747929 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -56,20 +56,20 @@ def write' (a : array α) (i : nat) (v : α) : array α :=
 if h : i < a.sz then a.write ⟨i, h⟩ v else a
 
 /- TODO: add builtin -/
-def uread (a : array α) (i : usize) (h : i.val < a.sz) : α :=
-a.read ⟨i.val, h⟩
+def uread (a : array α) (i : usize) (h : i.to_nat < a.sz) : α :=
+a.read ⟨i.to_nat, h⟩
 
 /- TODO: add builtin -/
-def uwrite (a : array α) (i : usize) (v : α) (h : i.val < a.sz) : array α :=
-a.write ⟨i.val, h⟩ v
+def uwrite (a : array α) (i : usize) (v : α) (h : i.to_nat < a.sz) : array α :=
+a.write ⟨i.to_nat, h⟩ v
 
 /- TODO: add builtin -/
 def uread' [inhabited α] (a : array α) (i : usize) : α :=
-if h : i.val < a.sz then a.read ⟨i.val, h⟩ else default α
+if h : i.to_nat < a.sz then a.read ⟨i.to_nat, h⟩ else default α
 
 /- TODO: add builtin -/
 def uwrite' (a : array α) (i : usize) (v : α) : array α :=
-if h : i.val < a.sz then a.write ⟨i.val, h⟩ v else a
+if h : i.to_nat < a.sz then a.write ⟨i.to_nat, h⟩ v else a
 
 /- TODO: mark as builtin -/
 def push (a : array α) (v : α) : array α :=
diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean
index dbdc56d7f5..40e12b0247 100644
--- a/library/init/data/hashmap/basic.lean
+++ b/library/init/data/hashmap/basic.lean
@@ -11,7 +11,7 @@ universes u v w
 def bucket_array (α : Type u) (β : α → Type v) :=
 { b : array (list (Σ a, β a)) // b.sz > 0 }
 
-def bucket_array.uwrite {α : Type u} {β : α → Type v} (data : bucket_array α β) (i : usize) (d : list (Σ a, β a)) (h : i.val < data.val.sz) : bucket_array α β :=
+def bucket_array.uwrite {α : Type u} {β : α → Type v} (data : bucket_array α β) (i : usize) (d : list (Σ a, β a)) (h : i.to_nat < data.val.sz) : bucket_array α β :=
 ⟨ data.val.uwrite i d h,
   calc (data.val.uwrite i d h).sz = data.val.sz : array.sz_write_eq _ _ _
                      ...          > 0           : data.property ⟩
@@ -35,8 +35,8 @@ let n := if nbuckets = 0 then 8 else nbuckets in
 namespace hashmap_imp
 variables {α : Type u} {β : α → Type v}
 
-def mk_idx {n : nat} (h : n > 0) (u : usize) : { u : usize // u.val < n } :=
-⟨u %ₙ n, fin.modn_lt _ h⟩
+def mk_idx {n : nat} (h : n > 0) (u : usize) : { u : usize // u.to_nat < n } :=
+⟨u %ₙ n, usize.modn_lt _ h⟩
 
 def reinsert_aux (hash_fn : α → usize) (data : bucket_array α β) (a : α) (b : β a) : bucket_array α β :=
 let ⟨i, h⟩ := mk_idx data.property (hash_fn a) in
diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean
index ef94099cab..ce2d58e5ef 100644
--- a/library/init/data/repr.lean
+++ b/library/init/data/repr.lean
@@ -130,10 +130,10 @@ instance : has_repr string.iterator :=
 instance (n : nat) : has_repr (fin n) :=
 ⟨λ f, repr (fin.val f)⟩
 
-instance : has_repr uint16 := ⟨λ n, repr (fin.val n)⟩
-instance : has_repr uint32 := ⟨λ n, repr (fin.val n)⟩
-instance : has_repr uint64 := ⟨λ n, repr (fin.val n)⟩
-instance : has_repr usize  := ⟨λ n, repr (fin.val n)⟩
+instance : has_repr uint16 := ⟨λ n, repr n.to_nat⟩
+instance : has_repr uint32 := ⟨λ n, repr n.to_nat⟩
+instance : has_repr uint64 := ⟨λ n, repr n.to_nat⟩
+instance : has_repr usize  := ⟨λ n, repr n.to_nat⟩
 
 def char.repr (c : char) : string :=
 repr c
diff --git a/library/init/data/to_string.lean b/library/init/data/to_string.lean
index f630f26222..568a57e1b1 100644
--- a/library/init/data/to_string.lean
+++ b/library/init/data/to_string.lean
@@ -53,13 +53,13 @@ instance (n : nat) : has_to_string (fin n) :=
 ⟨λ f, to_string (fin.val f)⟩
 
 instance : has_to_string uint16 :=
-⟨λ n, to_string (fin.val n)⟩
+⟨λ n, to_string n.to_nat⟩
 
 instance : has_to_string uint32 :=
-⟨λ n, to_string (fin.val n)⟩
+⟨λ n, to_string n.to_nat⟩
 
 instance : has_to_string uint64 :=
-⟨λ n, to_string (fin.val n)⟩
+⟨λ n, to_string n.to_nat⟩
 
 instance {α : Type u} [has_to_string α] : has_to_string (option α) :=
 ⟨λ o, match o with | none := "none" | (some a) := "(some " ++ to_string a ++ ")"⟩
diff --git a/library/init/data/uint.lean b/library/init/data/uint.lean
index f8f4075acc..e8a384045a 100644
--- a/library/init/data/uint.lean
+++ b/library/init/data/uint.lean
@@ -57,8 +57,10 @@ instance : has_le uint64    := ⟨fin.le⟩
 instance : inhabited uint64 := ⟨0⟩
 
 def uint16.of_nat (n : nat) : uint16 := fin.of_nat n
-def uint16.to_nat (u : uint16) : nat := fin.val u
+def uint16.to_nat (u : uint16) : nat := u.val
 def uint32.of_nat (n : nat) : uint32 := fin.of_nat n
-def uint32.to_nat (u : uint32) : nat := fin.val u
+def uint32.to_nat (u : uint32) : nat := u.val
 def uint64.of_nat (n : nat) : uint64 := fin.of_nat n
-def uint64.to_nat (u : uint64) : nat := fin.val u
+def uint64.to_nat (u : uint64) : nat := u.val
+
+attribute [irreducible] uint16 uint32 uint64
diff --git a/library/init/data/usize.lean b/library/init/data/usize.lean
index a9cfed5f96..a7c6105551 100644
--- a/library/init/data/usize.lean
+++ b/library/init/data/usize.lean
@@ -19,6 +19,9 @@ nat.pos_pow_of_pos _ (nat.zero_lt_bit0 nat.one_ne_zero)
 def usize.of_nat (a : nat) : usize :=
 ⟨a % usize_sz, nat.mod_lt _ usize_sz_pos⟩
 
+def usize.to_nat (u : usize) : nat :=
+u.val
+
 instance : has_zero usize  := ⟨usize.of_nat 0⟩
 instance : has_one usize   := ⟨usize.of_nat 1⟩
 instance : has_add usize   := ⟨fin.add⟩
@@ -30,3 +33,8 @@ instance : has_div usize   := ⟨fin.div⟩
 instance : has_lt usize    := ⟨fin.lt⟩
 instance : has_le usize    := ⟨fin.le⟩
 instance : inhabited usize := ⟨0⟩
+
+theorem usize.modn_lt {m : nat} (u : usize) (h : m > 0) : (u %ₙ m).val < m :=
+fin.modn_lt u h
+
+attribute [irreducible] usize
diff --git a/library/init/meta/has_reflect.lean b/library/init/meta/has_reflect.lean
index f293143928..1fc70864c8 100644
--- a/library/init/meta/has_reflect.lean
+++ b/library/init/meta/has_reflect.lean
@@ -9,7 +9,7 @@ import init.meta.expr init.util
 @[reducible] meta def {u} has_reflect (α : Sort u) := Π a : α, reflected a
 
 section
-local attribute [semireducible] reflected
+local attribute [semireducible] reflected uint32 uint64
 
 meta instance nat.reflect : has_reflect ℕ
 | n := if n = 0 then `(0 : ℕ)
@@ -22,7 +22,6 @@ meta instance uint32.reflect : has_reflect uint32
 
 meta instance uint64.reflect : has_reflect uint64
 | ⟨n, pr⟩ := `(uint64.of_nat n)
-
 end
 
 /- Instances that [derive] depends on. All other basic instances are defined at the end of
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index 4b8d64bbd8..99d3fad5d0 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -578,7 +578,7 @@ private meta def is_case_simple_tag : tag → bool
 | _                    := ff
 
 private meta def is_case_tag : tag → option nat
-| (name.mk_numeral n `_case :: _) := some n.val
+| (name.mk_numeral n `_case :: _) := some n.to_nat
 | _                               := none
 
 private meta def tag_match (t : tag) (pre : list name) : bool :=
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 66e80be6e6..92af0f780e 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -1982,8 +1982,7 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) {
     try {
         expr t1 = infer(mvar);
         expr t2 = infer(new_v);
-        /* TODO(Leo): check whether using transparency_mode::All hurts performance.
-           We use Semireducible to make sure we will not fail an unification step
+        /* We use Semireducible to make sure we will not fail an unification step
                    ?m := t
            because we cannot establish that the types of ?m and t are definitionally equal
            due to the current transparency setting.
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 3809bf15c8..f9d9dfa1fc 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -795,7 +795,7 @@ public:
         transparency_scope m_transparency_scope;
         zeta_scope         m_zeta_scope;
         relaxed_scope(type_context_old & ctx):
-            m_transparency_scope(ctx, transparency_mode::All),
+            m_transparency_scope(ctx, transparency_mode::Semireducible),
             m_zeta_scope(ctx, true) {}
     };
 
diff --git a/tests/lean/run/type_class_performance1.lean b/tests/lean/run/type_class_performance1.lean
new file mode 100644
index 0000000000..83ca3fd037
--- /dev/null
+++ b/tests/lean/run/type_class_performance1.lean
@@ -0,0 +1,20 @@
+#print usize
+
+set_option pp.all true
+set_option trace.class_instances true
+set_option trace.type_context.is_def_eq true
+set_option trace.type_context.is_def_eq_detail true
+
+def foo1 (a b : uint64) : bool :=
+a = b
+
+
+#exit
+def foo2 (a b : uint16) : bool :=
+a = b
+
+def foo3 (a b : uint32) : bool :=
+a = b
+
+def foo4 (a b : usize) : bool :=
+a = b