diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 2f91975504..77393080cd 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2826,7 +2826,7 @@ void elaborator::assign_field_mvar(name const & S_fname, expr const & mvar,
 
 class unfold_projections_visitor : public replace_visitor {
 private:
-    type_context m_ctx;
+    type_context & m_ctx;
 protected:
     expr visit_app(expr const & e) override {
         expr e2 = replace_visitor::visit_app(e);
@@ -2837,7 +2837,7 @@ protected:
         return e2;
     }
 public:
-    unfold_projections_visitor(const type_context & ctx): m_ctx(ctx) {}
+    unfold_projections_visitor(type_context & ctx): m_ctx(ctx) {}
 };
 
 /* Predicated variant of `lean::instantiate_mvars`. It does not support delayed abstractions or universe mvars. */
@@ -3071,7 +3071,7 @@ expr elaborator::visit_structure_instance(expr const & e, optional<expr> const &
                 // Example: `functor.map (functor.mk ?p1 ?m1 ?m2...) => ?m1`
                 auto reduce_and_check_deps = [&](expr & e) {
                     if (use_subobjects)
-                        e = unfold_projections_visitor(m_env)(e);
+                        e = unfold_projections_visitor(m_ctx)(e);
                     expr t = e;
                     name_set deps;
                     expr pretty = replace(t, [&](expr const & e) {
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index e172f0f28e..aba66542ce 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -203,8 +203,8 @@ static optional<tactic_state> apply(type_context & ctx, expr e, apply_cfg const
     if ((cfg.m_unify && !ctx.unify(e_type, target)) ||
         (!cfg.m_unify && !ctx.match(e_type, target))) {
         if (out_error_obj) {
+            auto pp_ctx = ::lean::mk_pp_ctx(ctx.env(), s.get_options(), ctx.mctx(), ctx.lctx());
             auto thunk = [=]() {
-                auto pp_ctx = ::lean::mk_pp_ctx(ctx.env(), s.get_options(), ctx.mctx(), ctx.lctx());
                 format msg = format("invalid apply tactic, failed to ");
                 if (cfg.m_unify)
                     msg += format("unify");
diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h
index 651823da2b..df87c6783c 100644
--- a/src/library/tactic/simplify.h
+++ b/src/library/tactic/simplify.h
@@ -76,7 +76,7 @@ class simplify_core_fn {
 protected:
     typedef expr_struct_map<simp_result> simplify_cache;
 
-    type_context              m_ctx;
+    type_context &            m_ctx;
     defeq_canonizer           m_defeq_canonizer;
     name                      m_rel;
     simp_lemmas               m_slss;
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index d62d8ef392..197d3a6ef3 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -356,7 +356,8 @@ type_context::type_context(type_context_cache_ptr const & ptr, metavar_context c
 }
 
 type_context::~type_context() {
-    if (m_cache_manager)
+    // note: m_cache may have been moved out
+    if (m_cache_manager && m_cache)
         m_cache_manager->recycle(m_cache);
 }
 
diff --git a/src/library/type_context.h b/src/library/type_context.h
index e83abd24f1..f8a18b0841 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -700,12 +700,16 @@ public:
     type_context(environment const & env, options const & o, local_context const & lctx,
                  transparency_mode m = transparency_mode::Reducible):
         type_context(env, o, metavar_context(), lctx, m) {}
-    type_context(environment const & env, transparency_mode m = transparency_mode::Reducible):
+    explicit type_context(environment const & env, transparency_mode m = transparency_mode::Reducible):
         type_context(env, options(), metavar_context(), local_context(), m) {}
     type_context(environment const & env, options const & o, transparency_mode m = transparency_mode::Reducible):
         type_context(env, o, metavar_context(), local_context(), m) {}
     type_context(environment const & env, options const & o, metavar_context const & mctx, local_context const & lctx,
                  type_context_cache_manager & manager, transparency_mode m = transparency_mode::Reducible);
+    type_context(type_context const &) = delete;
+    type_context(type_context &&) = default;
+    type_context & operator=(type_context const &) = delete;
+    type_context & operator=(type_context &&) = default;
     virtual ~type_context();
 
     virtual environment const & env() const override { return m_cache->m_env; }
diff --git a/tests/lean/structure_instance_bug3.lean.expected.out b/tests/lean/structure_instance_bug3.lean.expected.out
index 07a7faf06f..9c32b2beda 100644
--- a/tests/lean/structure_instance_bug3.lean.expected.out
+++ b/tests/lean/structure_instance_bug3.lean.expected.out
@@ -3,8 +3,3 @@ structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field
 structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field 'bind' was not provided
 structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field 'pure_bind' was not provided
 structure_instance_bug3.lean:1:23: error: invalid structure value { ... }, field 'bind_assoc' was not provided
-structure_instance_bug3.lean:1:23: error: unexpected field 'map_pure'
-given field value
-  λ (α β : Type ?) (g : α → β) (x : α), eq.trans (eq.symm (?m_1 g (⁇ α x))) (⁇ α β x (⁇ β ∘ g))
-expected field value
-  ?m_1