diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index ad7edea6d..9070e4e6f 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -428,9 +428,10 @@ metavar_env::metavar_env(ro_metavar_env const & s):m_ptr(s.m_ptr) {
     if (m_ptr) m_ptr->inc_ref();
 }
 
-bool cached_metavar_env::update(optional<metavar_env> const & menv) {
+template<typename MEnv>
+bool cached_metavar_env_tpl<MEnv>::update(optional<MEnv> const & menv) {
     if (!menv) {
-        m_menv = none_menv();
+        m_menv = optional<MEnv>();
         if (m_timestamp != 0) {
             m_timestamp = 0;
             return true;
@@ -448,6 +449,8 @@ bool cached_metavar_env::update(optional<metavar_env> const & menv) {
         }
     }
 }
+template class cached_metavar_env_tpl<metavar_env>;
+template class cached_metavar_env_tpl<ro_metavar_env>;
 
 local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
     if (n == 0)
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index fd5fa5970..507fe8cde 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -221,6 +221,7 @@ public:
     metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
     friend bool is_eqp(metavar_env const & menv1, metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
     friend bool operator==(metavar_env const & menv1, metavar_env const & menv2) { return is_eqp(menv1, menv2); }
+    typedef metavar_env_cell * ptr;
 };
 
 SPECIALIZE_OPTIONAL_FOR_SMART_PTR(metavar_env)
@@ -263,6 +264,7 @@ public:
     metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
     friend bool is_eqp(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
     friend bool operator==(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return is_eqp(menv1, menv2); }
+    typedef metavar_env_cell const * ptr;
 };
 
 SPECIALIZE_OPTIONAL_FOR_SMART_PTR(ro_metavar_env)
@@ -272,29 +274,39 @@ inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env && e) { return optio
 inline optional<ro_metavar_env> const & to_ro_menv(optional<metavar_env> const & menv) { return reinterpret_cast<optional<ro_metavar_env> const &>(menv); }
 
 /**
-   \brief A cached weak reference to a metavariable environment + timestamp at the time of
-   the caching. This object may also cache optional references.
+   \brief Template for creating a cached reference to a metavariable
+   environment + timestamp at the time of the caching. This object may
+   also cache optional references.
+
+   We use this template for cached_metavar_env and cached_ro_metavar_env
 */
-class cached_metavar_env {
-    optional<metavar_env> m_menv;
-    unsigned              m_timestamp;
+template<typename MEnv>
+class cached_metavar_env_tpl {
+    optional<MEnv> m_menv;
+    unsigned       m_timestamp;
 public:
-    cached_metavar_env():m_timestamp(0) {}
-    void clear() { m_menv = none_menv(); m_timestamp = 0; }
+    cached_metavar_env_tpl():m_timestamp(0) {}
+    void clear() { m_menv = optional<MEnv>(); m_timestamp = 0; }
     /**
        \brief Updated the cached value with menv.
        Return true if menv is different from the the cached metavar_env, or if
        the timestamp is different.
     */
-    bool update(optional<metavar_env> const & menv);
-    bool update(metavar_env const & menv) { return update(some(menv)); }
+    bool update(optional<MEnv> const & menv);
+    bool update(MEnv const & menv) { return update(optional<MEnv>(menv)); }
     explicit operator bool() const { return static_cast<bool>(m_menv); }
-    optional<metavar_env> const & to_some_menv() const { return m_menv; }
-    optional<ro_metavar_env> const & to_some_ro_menv() const { return to_ro_menv(m_menv); }
-    metavar_env operator*() const { return *m_menv; }
-    metavar_env_cell * operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); }
+    optional<MEnv> const & to_some_menv() const { return m_menv; }
+    MEnv operator*() const { return *m_menv; }
+    typename MEnv::ptr operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); }
 };
 
+class cached_metavar_env : public cached_metavar_env_tpl<metavar_env> {
+public:
+    optional<ro_metavar_env> const & to_some_ro_menv() const { return to_ro_menv(to_some_menv()); }
+};
+
+typedef cached_metavar_env_tpl<ro_metavar_env> cached_ro_metavar_env;
+
 /**
    \brief Apply the changes in \c lctx to \c a.
 */
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index 4b3d6f2bb..965553755 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -78,7 +78,7 @@ class normalizer::imp {
 
     ro_environment::weak_ref m_env;
     context                  m_ctx;
-    cached_metavar_env       m_menv;
+    cached_ro_metavar_env    m_menv;
     cache                    m_cache;
     bool                     m_unfold_opaque;
     unsigned                 m_max_depth;
@@ -87,11 +87,11 @@ class normalizer::imp {
     ro_environment env() const { return ro_environment(m_env); }
 
     expr instantiate(expr const & e, unsigned n, expr const * s) {
-        return ::lean::instantiate(e, n, s, m_menv.to_some_ro_menv());
+        return ::lean::instantiate(e, n, s, m_menv.to_some_menv());
     }
 
     expr add_lift(expr const & m, unsigned s, unsigned n) {
-        return ::lean::add_lift(m, s, n, m_menv.to_some_ro_menv());
+        return ::lean::add_lift(m, s, n, m_menv.to_some_menv());
     }
 
     expr lookup(value_stack const & s, unsigned i) {
@@ -338,7 +338,7 @@ public:
         m_unfold_opaque  = false;
     }
 
-    expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, bool unfold_opaque) {
+    expr operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv, bool unfold_opaque) {
         if (m_unfold_opaque != unfold_opaque)
             m_cache.clear();
         m_unfold_opaque = unfold_opaque;
@@ -356,14 +356,14 @@ normalizer::normalizer(ro_environment const & env, unsigned max_depth):m_ptr(new
 normalizer::normalizer(ro_environment const & env):normalizer(env, std::numeric_limits<unsigned>::max()) {}
 normalizer::normalizer(ro_environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {}
 normalizer::~normalizer() {}
-expr normalizer::operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, bool unfold_opaque) {
+expr normalizer::operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv, bool unfold_opaque) {
     return (*m_ptr)(e, ctx, menv, unfold_opaque);
 }
-expr normalizer::operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque) {
-    return operator()(e, ctx, some_menv(menv), unfold_opaque);
+expr normalizer::operator()(expr const & e, context const & ctx, ro_metavar_env const & menv, bool unfold_opaque) {
+    return operator()(e, ctx, some_ro_menv(menv), unfold_opaque);
 }
 expr normalizer::operator()(expr const & e, context const & ctx, bool unfold_opaque) {
-    return operator()(e, ctx, none_menv(), unfold_opaque);
+    return operator()(e, ctx, none_ro_menv(), unfold_opaque);
 }
 void normalizer::clear() { m_ptr->clear(); }
 
diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h
index ebbc46fa7..5b19900b2 100644
--- a/src/kernel/normalizer.h
+++ b/src/kernel/normalizer.h
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 namespace lean {
 class environment;
 class options;
-class metavar_env;
+class ro_metavar_env;
 /** \brief Functional object for normalizing expressions */
 class normalizer {
     class imp;
@@ -24,8 +24,8 @@ public:
     normalizer(ro_environment const & env, options const & opts);
     ~normalizer();
 
-    expr operator()(expr const & e, context const & ctx, optional<metavar_env> const & menv, bool unfold_opaque = false);
-    expr operator()(expr const & e, context const & ctx, metavar_env const & menv, bool unfold_opaque = false);
+    expr operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv, bool unfold_opaque = false);
+    expr operator()(expr const & e, context const & ctx, ro_metavar_env const & menv, bool unfold_opaque = false);
     expr operator()(expr const & e, context const & ctx = context(), bool unfold_opaque = false);
 
     void clear();
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 9276e1846..1e6362a7e 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -48,7 +48,7 @@ class type_checker::imp {
     expr lower_free_vars(expr const & e, unsigned s, unsigned n) { return ::lean::lower_free_vars(e, s, n, m_menv.to_some_ro_menv()); }
     expr instantiate_with_closed(expr const & e, expr const & v) { return ::lean::instantiate_with_closed(e, v, m_menv.to_some_ro_menv()); }
     expr instantiate(expr const & e, expr const & v) { return ::lean::instantiate(e, v, m_menv.to_some_ro_menv()); }
-    expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque); }
+    expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { return m_normalizer(e, ctx, m_menv.to_some_ro_menv(), unfold_opaque); }
 
     expr check_type(expr const & e, expr const & s, context const & ctx) {
         if (is_type(e) || is_bool(e))