diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
index f5ca987dda..6ba9f3e78c 100644
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -35,6 +35,7 @@ other Regular definitions used in a definition.
 Remark: the hint only affects performance. */
 enum class reducibility_hints_kind { Opaque, Abbreviation, Regular };
 class reducibility_hints : public object_ref {
+    reducibility_hints(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit reducibility_hints(object * r):object_ref(r) {}
 public:
     static reducibility_hints mk_opaque() { return reducibility_hints(box(static_cast<unsigned>(reducibility_hints_kind::Opaque))); }
@@ -48,7 +49,7 @@ public:
     bool is_regular() const { return kind() == reducibility_hints_kind::Regular; }
     unsigned get_height() const { return is_regular() ? cnstr_scalar<unsigned>(raw(), 0) : 0; }
     void serialize(serializer & s) const { s.write_object(raw()); }
-    static reducibility_hints deserialize(deserializer & d) { object * o = d.read_object(); inc(o); return reducibility_hints(o); }
+    static reducibility_hints deserialize(deserializer & d) { return reducibility_hints(d.read_object(), true); }
 };
 
 inline serializer & operator<<(serializer & s, reducibility_hints const & l) { l.serialize(s); return s; }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 213d435cdd..cc8b0352a5 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -45,7 +45,7 @@ inline bool is_rec(binder_info bi) { return bi == binder_info::Rec; }
 /* Expression literal values */
 enum class literal_kind { Nat, String };
 class literal : public object_ref {
-    explicit literal(object * o):object_ref(o) { inc(o); }
+    explicit literal(b_obj_arg o, bool b):object_ref(o, b) {}
 public:
     explicit literal(char const * v);
     explicit literal(unsigned v);
@@ -62,7 +62,7 @@ public:
     friend bool operator<(literal const & a, literal const & b);
 
     void serialize(serializer & s) const { s.write_object(raw()); }
-    static literal deserialize(deserializer & d) { return literal(d.read_object()); }
+    static literal deserialize(deserializer & d) { return literal(d.read_object(), true); }
 };
 inline bool operator!=(literal const & a, literal const & b) { return !(a == b); }
 inline serializer & operator<<(serializer & s, literal const & l) { l.serialize(s); return s; }
@@ -91,7 +91,7 @@ inductive expr
 */
 enum class expr_kind { BVar, FVar, MVar, Sort, Const, App, Lambda, Pi, Let, Lit, MData, Proj, Quote };
 class expr : public object_ref {
-    explicit expr(object * o):object_ref(o) { inc(o); }
+    explicit expr(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit expr(object_ref && o):object_ref(o) {}
 
     friend expr mk_lit(literal const & lit);
@@ -118,7 +118,7 @@ public:
 
     friend bool is_eqp(expr const & e1, expr const & e2) { return e1.raw() == e2.raw(); }
     void serialize(serializer & s) const { s.write_object(raw()); }
-    static expr deserialize(deserializer & d) { return expr(d.read_object()); }
+    static expr deserialize(deserializer & d) { return expr(d.read_object(), true); }
 };
 
 typedef list_ref<expr> exprs;
diff --git a/src/kernel/level.h b/src/kernel/level.h
index c623656343..bfd9783855 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -36,7 +36,7 @@ class level : public object_ref {
     friend level mk_max_imax(level_kind k, level const & l1, level const & l2);
     friend level mk_univ_param(name const & n);
     friend level mk_univ_mvar(name const & n);
-    explicit level(object * o):object_ref(o) { inc(o); }
+    explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit level(object_ref && o):object_ref(o) {}
 public:
     /** \brief Universe zero */
@@ -51,7 +51,7 @@ public:
 
     friend bool is_eqp(level const & l1, level const & l2) { return l1.raw() == l2.raw(); }
     void serialize(serializer & s) const { s.write_object(raw()); }
-    static level deserialize(deserializer & d) { return level(d.read_object()); }
+    static level deserialize(deserializer & d) { return level(d.read_object(), true); }
 
     bool is_zero() const { lean_assert((kind() == level_kind::Zero) == is_scalar(raw())); return is_scalar(raw()); }
     bool is_succ() const { return kind() == level_kind::Succ; }
diff --git a/src/util/kvmap.h b/src/util/kvmap.h
index daa452277a..e8f3acc456 100644
--- a/src/util/kvmap.h
+++ b/src/util/kvmap.h
@@ -19,7 +19,7 @@ inductive data_value
 | of_name   (v : name)
 */
 class data_value : public object_ref {
-    explicit data_value(object * o):object_ref(o) { inc(o); }
+    data_value(b_obj_arg o, bool b):object_ref(o, b) {}
 public:
     data_value(char const * v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::String), mk_string(v))) {}
     data_value(string_ref const & v):object_ref(mk_cnstr(static_cast<unsigned>(data_value_kind::String), v.raw())) { inc(v.raw()); }
@@ -33,7 +33,7 @@ public:
     data_value & operator=(data_value && other) { object_ref::operator=(other); return *this; }
 
     void serialize(serializer & s) const { s.write_object(raw()); }
-    static data_value deserialize(deserializer & d) { return data_value(d.read_object()); }
+    static data_value deserialize(deserializer & d) { return data_value(d.read_object(), true); }
 
     data_value_kind kind() const { return static_cast<data_value_kind>(cnstr_tag(raw())); }
     string_ref const & get_string() const { lean_assert(kind() == data_value_kind::String); return static_cast<string_ref const &>(cnstr_obj_ref(*this, 0)); }
diff --git a/src/util/list_ref.h b/src/util/list_ref.h
index fe391767f8..28be10c9e6 100644
--- a/src/util/list_ref.h
+++ b/src/util/list_ref.h
@@ -13,7 +13,7 @@ template<typename T> T const & head(object * o) { return static_cast<T const &>(
 /* Wrapper for manipulating Lean lists in C++ */
 template<typename T>
 class list_ref : public object_ref {
-    explicit list_ref(object * o):object_ref(o) { inc(o); }
+    list_ref(b_obj_arg o, bool b):object_ref(o, b) {}
 public:
     list_ref():object_ref(box(0)) {}
     explicit list_ref(T const & a):object_ref(mk_cnstr(1, a.raw(), box(0))) { inc(a.raw()); }
@@ -46,7 +46,7 @@ public:
 
     friend bool is_eqp(list_ref const & l1, list_ref const & l2) { return l1.raw() == l2.raw(); }
     void serialize(serializer & s) const { s.write_object(raw()); }
-    static list_ref deserialize(deserializer & d) { return list_ref(d.read_object()); }
+    static list_ref deserialize(deserializer & d) { return list_ref(d.read_object(), true); }
 
     /** \brief Structural equality. */
     friend bool operator==(list_ref const & l1, list_ref const & l2) {
diff --git a/src/util/name.h b/src/util/name.h
index 0008b4b5eb..998898e3ab 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -55,10 +55,12 @@ public:
     static int cmp_core(object * o1, object * o2);
     size_t size_core(bool unicode) const;
 private:
+    name(b_obj_arg r, bool b):object_ref(r, b) {}
     friend name read_name(deserializer & d);
     explicit name(object_ref && r):object_ref(r) {}
 public:
     name():object_ref(box(static_cast<unsigned>(name_kind::ANONYMOUS))) {}
+    name(obj_arg o):object_ref(o) {}
     name(name const & prefix, char const * name);
     name(name const & prefix, unsigned k);
     name(name const & prefix, nat const & n);
@@ -74,7 +76,6 @@ public:
        name <tt>foo::bla::tst</tt>.
     */
     name(std::initializer_list<char const *> const & l);
-    explicit name(object * r):object_ref(r) { inc(r); }
     static name const & anonymous();
     /**
         \brief Create a unique internal name that is not meant to exposed
@@ -233,7 +234,7 @@ struct name_pair_quick_cmp {
 typedef std::function<bool(name const &)> name_predicate; // NOLINT
 
 inline serializer & operator<<(serializer & s, name const & n) { n.serialize(s); return s; }
-inline name read_name(deserializer & d) { return name(d.read_object()); }
+inline name read_name(deserializer & d) { return name(d.read_object(), true); }
 inline deserializer & operator>>(deserializer & d, name & n) { n = read_name(d); return d; }
 
 /** \brief Return true if it is a lean internal name, i.e., the name starts with a `_` */
diff --git a/src/util/nat.h b/src/util/nat.h
index 7c1ace1a3e..1ff2de1ca7 100644
--- a/src/util/nat.h
+++ b/src/util/nat.h
@@ -11,7 +11,8 @@ Author: Leonardo de Moura
 namespace lean {
 /* Wrapper for manipulating Lean runtime nat values in C++. */
 class nat : public object_ref {
-    nat(object * o, bool):object_ref(o) {}
+    nat(b_obj_arg o, bool b):object_ref(o, b) {}
+    explicit nat(obj_arg o):object_ref(o) {}
     static nat wrap(object * o) { return nat(o, true); }
 public:
     nat():object_ref(box(0)) {}
@@ -25,7 +26,6 @@ public:
     }
     nat(nat const & other):object_ref(other) {}
     nat(nat && other):object_ref(other) {}
-    explicit nat(object * o):object_ref(o) {}
 
     nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
     nat & operator=(nat && other) { object_ref::operator=(other); return *this; }
@@ -55,10 +55,11 @@ public:
     friend nat operator/(nat const & a, nat const & b)   { return wrap(nat_div(a.raw(), b.raw())); }
     friend nat operator%(nat const & a, nat const & b)   { return wrap(nat_mod(a.raw(), b.raw())); }
     void serialize(serializer & s) const { s.write_object(raw()); }
+    static nat deserialize(deserializer & d) { return nat(d.read_object(), true); }
 };
 
 inline serializer & operator<<(serializer & s, nat const & n) { n.serialize(s); return s; }
-inline nat read_nat(deserializer & d) { return nat(d.read_object()); }
+inline nat read_nat(deserializer & d) { return nat::deserialize(d); }
 inline deserializer & operator>>(deserializer & d, nat & n) { n = read_nat(d); return d; }
 inline std::ostream & operator<<(std::ostream & out, nat const & n) { out << n.to_mpz(); return out; }
 };
diff --git a/src/util/object_ref.h b/src/util/object_ref.h
index 405179841a..6f20cb7b93 100644
--- a/src/util/object_ref.h
+++ b/src/util/object_ref.h
@@ -14,7 +14,8 @@ class object_ref {
     object * m_obj;
 public:
     object_ref():m_obj(box(0)) {}
-    explicit object_ref(object * o):m_obj(o) { lean_assert(is_scalar(o) || !is_heap_obj(o) || get_rc(o) > 0); }
+    explicit object_ref(obj_arg o):m_obj(o) { lean_assert(is_scalar(o) || !is_heap_obj(o) || get_rc(o) > 0); }
+    object_ref(b_obj_arg o, bool):m_obj(o) { inc(o); }
     object_ref(object_ref const & s):m_obj(s.m_obj) { inc(m_obj); }
     object_ref(object_ref && s):m_obj(s.m_obj) { s.m_obj = box(0); }
     ~object_ref() { dec(m_obj); }
diff --git a/src/util/pair_ref.h b/src/util/pair_ref.h
index d4a1ddefb1..ac9723a71f 100644
--- a/src/util/pair_ref.h
+++ b/src/util/pair_ref.h
@@ -11,7 +11,7 @@ namespace lean {
 /* Wrapper for manipulating Lean pairs in C++ */
 template<typename T1, typename T2>
 class pair_ref : public object_ref {
-    explicit pair_ref(object * o):object_ref(o) { inc(o); }
+    explicit pair_ref(b_obj_arg o, bool b):object_ref(o, b) {}
 public:
     pair_ref(T1 const & a, T2 const & b):object_ref(mk_cnstr(0, a.raw(), b.raw())) { inc(a.raw()); inc(b.raw()); }
     pair_ref(pair_ref const & other):object_ref(other) {}
@@ -23,7 +23,7 @@ public:
     T2 const & snd() const { return static_cast<T2 const &>(cnstr_obj_ref(*this, 1)); }
 
     void serialize(serializer & s) const { s.write_object(raw()); }
-    static pair_ref deserialize(deserializer & d) { return pair_ref(d.read_object()); }
+    static pair_ref deserialize(deserializer & d) { return pair_ref(d.read_object(), true); }
 };
 
 template<typename T1, typename T2> bool operator==(pair_ref<T1, T2> const & a, pair_ref<T1, T2> const & b) {