diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index 8f3ba79376..3b9948077f 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -390,7 +390,7 @@ class tactic_dsimplify_fn : public dsimplify_core_fn {
             m_s = *new_s;
             m_ctx.set_mctx(m_s.mctx());
             m_defeq_canonizer.set_state(m_s.dcs());
-            vm_obj p   = cfield(r, 0);
+            vm_obj p   = tactic::get_result_value(r);
             m_a        = cfield(p, 0);
             vm_obj p1  = cfield(p, 1);
             expr new_e = to_expr(cfield(p1, 0));
diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index 361bfc214b..16e19827d4 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -1140,7 +1140,7 @@ class vm_simplify_fn : public simplify_ext_core_fn {
             m_s = *new_s;
             m_ctx.set_mctx(m_s.mctx());
             m_defeq_canonizer.set_state(m_s.dcs());
-            vm_obj t = cfield(r, 0);
+            vm_obj t = tactic::get_result_value(r);
             /* t : A × expr × option expr × bool */
             m_a        = cfield(t, 0);
             vm_obj t1  = cfield(t, 1);
diff --git a/src/library/tactic/smt/congruence_tactics.cpp b/src/library/tactic/smt/congruence_tactics.cpp
index b7e79ccd32..64d743b4ea 100644
--- a/src/library/tactic/smt/congruence_tactics.cpp
+++ b/src/library/tactic/smt/congruence_tactics.cpp
@@ -186,21 +186,21 @@ vm_obj cc_state_internalize(vm_obj const & ccs, vm_obj const & e, vm_obj const &
 vm_obj cc_state_is_eqv(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) {
     cc_state_proc({
             bool r = cc.is_eqv(to_expr(e1), to_expr(e2));
-            return tactic::mk_success(mk_vm_bool(r), s);
+            return tactic::mk_result(mk_vm_bool(r), s);
         });
 }
 
 vm_obj cc_state_is_not_eqv(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) {
     cc_state_proc({
             bool r = cc.is_not_eqv(to_expr(e1), to_expr(e2));
-            return tactic::mk_success(mk_vm_bool(r), s);
+            return tactic::mk_result(mk_vm_bool(r), s);
         });
 }
 
 vm_obj cc_state_eqv_proof(vm_obj const & ccs, vm_obj const & e1, vm_obj const & e2, vm_obj const & _s) {
     cc_state_proc({
             if (optional<expr> r = cc.get_proof(to_expr(e1), to_expr(e2))) {
-                return tactic::mk_success(to_obj(*r), s);
+                return tactic::mk_result(to_obj(*r), s);
             } else {
                 return tactic::mk_exception("cc_state.eqv_proof failed to build proof", s);
             }
@@ -210,7 +210,7 @@ vm_obj cc_state_eqv_proof(vm_obj const & ccs, vm_obj const & e1, vm_obj const &
 vm_obj cc_state_proof_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) {
     cc_state_proc({
             if (optional<expr> r = cc.get_eq_proof(to_expr(e), mk_true())) {
-                return tactic::mk_success(to_obj(mk_of_eq_true(cc.ctx(), *r)), s);
+                return tactic::mk_result(to_obj(mk_of_eq_true(cc.ctx(), *r)), s);
             } else {
                 return tactic::mk_exception("cc_state.get_proof_for failed to build proof", s);
             }
@@ -220,7 +220,7 @@ vm_obj cc_state_proof_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _
 vm_obj cc_state_refutation_for(vm_obj const & ccs, vm_obj const & e, vm_obj const & _s) {
     cc_state_proc({
             if (optional<expr> r = cc.get_eq_proof(to_expr(e), mk_false())) {
-                return tactic::mk_success(to_obj(mk_not_of_eq_false(cc.ctx(), *r)), s);
+                return tactic::mk_result(to_obj(mk_not_of_eq_false(cc.ctx(), *r)), s);
             } else {
                 return tactic::mk_exception("cc_state.get_refutation_for failed to build proof", s);
             }
@@ -230,7 +230,7 @@ vm_obj cc_state_refutation_for(vm_obj const & ccs, vm_obj const & e, vm_obj cons
 vm_obj cc_state_proof_for_false(vm_obj const & ccs, vm_obj const & _s) {
     cc_state_proc({
             if (auto pr = cc.get_inconsistency_proof()) {
-                return tactic::mk_success(to_obj(*pr), s);
+                return tactic::mk_result(to_obj(*pr), s);
             } else {
                 return tactic::mk_exception("cc_state.false_proof failed, state is not inconsistent", s);
             }
diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp
index 2df3c41893..56b9456cdd 100644
--- a/src/library/tactic/smt/smt_state.cpp
+++ b/src/library/tactic/smt/smt_state.cpp
@@ -141,12 +141,8 @@ vm_obj to_obj(smt_goal const & s) {
     return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_smt_goal))) vm_smt_goal(s));
 }
 
-vm_obj tactic_result_to_smt_tactic_result(vm_obj const & r, vm_obj const & ss) {
-    return tactic::mk_result(mk_vm_pair(tactic::get_result_value(r), ss), tactic::get_result_state(r));
-}
-
 vm_obj mk_smt_tactic_success(vm_obj const & a, vm_obj const & ss, vm_obj const & ts) {
-    return mk_vm_constructor(0, mk_vm_pair(a, ss), ts);
+    return tactic::mk_result(mk_vm_pair(a, ss), ts);
 }
 
 vm_obj mk_smt_tactic_success(vm_obj const & ss, vm_obj const & ts) {
@@ -157,6 +153,10 @@ vm_obj mk_smt_tactic_success(vm_obj const & ss, tactic_state const & ts) {
     return mk_smt_tactic_success(ss, to_obj(ts));
 }
 
+vm_obj tactic_success_to_smt_tactic_success(vm_obj const & r, vm_obj const & ss) {
+    return mk_smt_tactic_success(tactic::get_result_value(r), ss, tactic::get_result_state(r));
+}
+
 /* Remove auxiliary definitions introduced by the equation compiler.
    Reason: ematching will close the goal by instantiating them.
    Then later, the equation compiler will fail to eliminate this application
@@ -518,7 +518,7 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s
     }
     if (is_nil(ss)) {
         /* There is no SMT state associated with any goal. */
-        return tactic_result_to_smt_tactic_result(r1, ss);
+        return tactic_success_to_smt_tactic_success(r1, ss);
     }
     /* We only handle the common cases:
        1) goals is of the form (a_1, a_2, ..., a_m)
@@ -538,17 +538,17 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s
     vm_obj new_ts = tactic::get_result_state(r1);
     if (is_eqp(tactic::to_state(ts), tactic::to_state(new_ts))) {
         /* The tactic_state was not modified */
-        return tactic_result_to_smt_tactic_result(r1, ss);
+        return tactic_success_to_smt_tactic_success(r1, ss);
     }
     list<expr> goals          = tactic::to_state(ts).goals();
     list<expr> new_goals      = tactic::to_state(new_ts).goals();
     if (goals == new_goals) {
         /* Set of goals did not change. */
-        return tactic_result_to_smt_tactic_result(r1, ss);
+        return tactic_success_to_smt_tactic_success(r1, ss);
     }
     if (!new_goals) {
         /* There are no new goals */
-        return tactic_result_to_smt_tactic_result(r1, mk_vm_nil());
+        return tactic_success_to_smt_tactic_success(r1, mk_vm_nil());
     }
     if (!goals) {
         return tactic::mk_exception("failed to lift tactic to smt_tactic, there were no goals to be solved", tactic::to_state(ts));
@@ -557,12 +557,12 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s
         /* Main goal was solved */
         /* remove one SMT goal */
         vm_obj new_ss = tail(ss);
-        return tactic_result_to_smt_tactic_result(r1, new_ss);
+        return tactic_success_to_smt_tactic_success(r1, new_ss);
     }
     metavar_context const & mctx = tactic::to_state(new_ts).mctx();
     if (tail(new_goals) == tail(goals) && same_hyps(mctx, head(new_goals), head(goals))) {
         /* The set of hypotheses in the main goal did not change */
-        return tactic_result_to_smt_tactic_result(r1, ss);
+        return tactic_success_to_smt_tactic_success(r1, ss);
     }
     vm_obj new_ss = ss;
     while (true) {
@@ -571,7 +571,7 @@ vm_obj tactic_to_smt_tactic(vm_obj const &, vm_obj const & tac, vm_obj const & s
                                        tactic::to_state(ts));
         }
         if (tail(new_goals) == tail(goals)) {
-            return tactic_result_to_smt_tactic_result(r1, new_ss);
+            return tactic_success_to_smt_tactic_success(r1, new_ss);
         }
         /* copy smt state */
         new_ss = mk_vm_cons(head(new_ss), new_ss);
diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp
index de51233f92..94886722b7 100644
--- a/src/library/tactic/user_attribute.cpp
+++ b/src/library/tactic/user_attribute.cpp
@@ -283,7 +283,7 @@ vm_obj user_attribute_get_cache_core(vm_obj const &, vm_obj const &, vm_obj cons
         result = invoke(cache_handler, to_obj(to_list(instances)), to_obj(s0));
         was_updated = get_vm_state().env_was_updated();
     }
-    if (tactic::is_success(result)) {
+    if (tactic::is_result_success(result)) {
         if (!was_updated) {
             user_attr_cache::entry entry;
             entry.m_env         = env;
@@ -291,15 +291,14 @@ vm_obj user_attribute_get_cache_core(vm_obj const &, vm_obj const &, vm_obj cons
             entry.m_dep_fingerprints = map2<unsigned>(deps, [&](name const & n) {
                     return get_attribute(env, n).get_fingerprint(env);
                 });
-            entry.m_val = cfield(result, 0);
+            entry.m_val = tactic::get_result_value(result);
             cache.m_cache.erase(attr.get_name());
             cache.m_cache.insert(mk_pair(attr.get_name(), entry));
             return tactic::mk_success(entry.m_val, s);
         } else {
             lean_trace("user_attributes_cache", tout() << "did not cache result for [" << attr.get_name() << "] "
                        "because VM environment has been updated with temporary declarations\n";);
-            vm_obj r = cfield(result, 0);
-            return tactic::mk_success(r, s);
+            return tactic::mk_success(tactic::get_result_value(result), s);
         }
     } else {
         return result;
diff --git a/src/library/vm/interaction_state.h b/src/library/vm/interaction_state.h
index 56e960272b..b993e65578 100644
--- a/src/library/vm/interaction_state.h
+++ b/src/library/vm/interaction_state.h
@@ -39,6 +39,9 @@ struct interaction_monad {
     static bool is_silent_exception(vm_obj const & ex);
     static vm_obj mk_result(vm_obj const & a, vm_obj const & s);
     static bool is_result_exception(vm_obj const & r);
+    static vm_obj get_exception_message(vm_obj const & r);
+    static vm_obj get_exception_pos(vm_obj const & r);
+    static vm_obj get_exception_state(vm_obj const & r);
     static bool is_result_success(vm_obj const & r);
     static vm_obj get_result_value(vm_obj const & r);
     static vm_obj get_result_state(vm_obj const & r);
diff --git a/src/library/vm/interaction_state_imp.h b/src/library/vm/interaction_state_imp.h
index a6781ab0f0..72cee2af0a 100644
--- a/src/library/vm/interaction_state_imp.h
+++ b/src/library/vm/interaction_state_imp.h
@@ -26,6 +26,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_list.h"
 #include "library/vm/vm_option.h"
+#include "library/vm/vm_pos_info.h"
 #include "library/compiler/vm_compiler.h"
 
 namespace lean {
@@ -89,6 +90,24 @@ bool interaction_monad<State>::is_result_exception(vm_obj const & r) {
     return is_constructor(r) && cidx(r) == 1;
 }
 
+template<typename State>
+vm_obj interaction_monad<State>::get_exception_message(vm_obj const & r) {
+    lean_assert(is_result_exception(r));
+    return cfield(r, 0);
+}
+
+template<typename State>
+vm_obj interaction_monad<State>::get_exception_pos(vm_obj const & r) {
+    lean_assert(is_result_exception(r));
+    return cfield(r, 1);
+}
+
+template<typename State>
+vm_obj interaction_monad<State>::get_exception_state(vm_obj const & r) {
+    lean_assert(is_result_exception(r));
+    return cfield(r, 2);
+}
+
 template<typename State>
 bool interaction_monad<State>::is_result_success(vm_obj const & r) {
     return is_constructor(r) && cidx(r) == 0;
@@ -113,7 +132,7 @@ vm_obj interaction_monad<State>::mk_success(vm_obj const & a, State const & s) {
 
 template<typename State>
 vm_obj interaction_monad<State>::mk_success(State const & s) {
-    return mk_success(mk_vm_unit(), s);
+    return mk_result(mk_vm_unit(), s);
 }
 
 template<typename State>
@@ -133,8 +152,8 @@ vm_obj interaction_monad<State>::mk_exception(vm_obj const & fn, vm_obj const &
 
 template<typename State>
 vm_obj interaction_monad<State>::update_exception_state(vm_obj const & ex, State const & s) {
-    lean_assert(!is_success(ex));
-    return mk_vm_constructor(1, cfield(ex, 0), cfield(ex, 1), to_obj(s));
+    lean_assert(is_result_exception(ex));
+    return mk_exception(get_exception_message(ex), get_exception_pos(ex), s);
 }
 
 template<typename State>
@@ -186,20 +205,20 @@ void interaction_monad<State>::report_exception(vm_state & S, vm_obj const & r)
 template<typename State>
 auto interaction_monad<State>::is_success(vm_obj const & r) -> optional<State> {
     if (is_result_success(r))
-        return some(to_state(cfield(r, 1)));
+        return some(to_state(get_result_state(r)));
     return {};
 }
 
 template<typename State>
 auto interaction_monad<State>::is_exception(vm_state & S, vm_obj const & ex) -> optional<exception_info> {
-    if (is_result_exception(ex) && !is_none(cfield(ex, 0))) {
-        vm_obj fmt = S.invoke(get_some_value(cfield(ex, 0)), mk_vm_unit());
+    if (is_result_exception(ex) && !is_none(get_exception_message(ex))) {
+        vm_obj fmt = S.invoke(get_some_value(get_exception_message(ex)), mk_vm_unit());
         optional<pos_info> p;
-        if (!is_none(cfield(ex, 1))) {
-            auto vm_p = get_some_value(cfield(ex, 1));
-            p = some(mk_pair(to_unsigned(cfield(vm_p, 0)), to_unsigned(cfield(vm_p, 1))));
+        if (!is_none(get_exception_pos(ex))) {
+            auto vm_p = get_some_value(get_exception_pos(ex));
+            p = some(to_pos_info(vm_p));
         }
-        return optional<exception_info>(to_format(fmt), p, to_state(cfield(ex, 2)));
+        return optional<exception_info>(to_format(fmt), p, to_state(get_exception_state(ex)));
     } else {
         return {};
     }