diff --git a/doc/changes.md b/doc/changes.md
index 023a28819a..f1ebeefb2f 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -128,6 +128,9 @@ master branch (aka work in progress branch)
 
 *Changes*
 
+* Command `variable [io.interface]` is not needed anymore to use the `io` monad.
+  It is also easier to add new io primitives.
+
 * Replace `inout` modifier in type class declarations with `out_param` modifier.
   Reason: counterintuitive behavior in the type class resolution procedure.
   The result could depend on partial information available in the `inout`
diff --git a/leanpkg/leanpkg/git.lean b/leanpkg/leanpkg/git.lean
index 0924e6c4a0..e530042ede 100644
--- a/leanpkg/leanpkg/git.lean
+++ b/leanpkg/leanpkg/git.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 -/
 import leanpkg.lean_version system.io
-variable [io.interface]
 
 namespace leanpkg
 
diff --git a/leanpkg/leanpkg/main.lean b/leanpkg/leanpkg/main.lean
index 8f031c42b5..c6539ef282 100644
--- a/leanpkg/leanpkg/main.lean
+++ b/leanpkg/leanpkg/main.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 -/
 import leanpkg.resolve leanpkg.git
-variable [io.interface]
 
 namespace leanpkg
 
diff --git a/leanpkg/leanpkg/manifest.lean b/leanpkg/leanpkg/manifest.lean
index 2836532cb1..a222ae0442 100644
--- a/leanpkg/leanpkg/manifest.lean
+++ b/leanpkg/leanpkg/manifest.lean
@@ -95,7 +95,7 @@ match parser.run_string toml.File s with
 | sum.inl _ := none
 end
 
-def from_file [io.interface] (fn : string) : io manifest := do
+def from_file (fn : string) : io manifest := do
 cnts ← io.fs.read_file fn,
 toml ←
   (match parser.run toml.File cnts with
diff --git a/leanpkg/leanpkg/proc.lean b/leanpkg/leanpkg/proc.lean
index 1a84b0f890..921e71b2f6 100644
--- a/leanpkg/leanpkg/proc.lean
+++ b/leanpkg/leanpkg/proc.lean
@@ -5,7 +5,6 @@ Author: Gabriel Ebner
 -/
 import system.io leanpkg.toml
 open io io.proc
-variable [io.interface]
 
 namespace leanpkg
 
diff --git a/leanpkg/leanpkg/resolve.lean b/leanpkg/leanpkg/resolve.lean
index 4f0489a6f5..a8d28f66f4 100644
--- a/leanpkg/leanpkg/resolve.lean
+++ b/leanpkg/leanpkg/resolve.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 -/
 import leanpkg.manifest system.io leanpkg.proc leanpkg.git
-variable [io.interface]
 
 namespace leanpkg
 
diff --git a/library/system/io.lean b/library/system/io.lean
index c23ac72c73..d8bab91544 100644
--- a/library/system/io.lean
+++ b/library/system/io.lean
@@ -3,131 +3,65 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
 -/
-import data.buffer
+import system.io_interface
 
-inductive io.error
-| other     : string → io.error
-| sys       : nat → io.error
+/- The following constants have a builtin implementation -/
+constant io_core : Type → Type → Type
+@[instance] constant monad_io_impl             : monad_io io_core
+@[instance] constant monad_io_terminal_impl    : monad_io_terminal io_core
+@[instance] constant monad_io_file_system_impl : monad_io_file_system io_core
+@[instance] constant monad_io_environment_impl : monad_io_environment io_core
+@[instance] constant monad_io_process_impl     : monad_io_process io_core
 
-structure io.terminal (m : Type → Type → Type) :=
-(put_str     : string → m io.error unit)
-(get_line    : m io.error string)
-(cmdline_args : list string)
+instance io_core_is_monad (e : Type) : monad (io_core e) :=
+monad_io_is_monad io_core e
 
-inductive io.mode
-| read | write | read_write | append
+instance io_core_is_monad_fail : monad_fail (io_core io.error) :=
+monad_io_is_monad_fail io_core
 
-structure io.file_system (handle : Type) (m : Type → Type → Type) :=
-/- Remark: in Haskell, they also provide  (Maybe TextEncoding) and  NewlineMode -/
-(mk_file_handle : string → io.mode → bool → m io.error handle)
-(is_eof         : handle → m io.error bool)
-(flush          : handle → m io.error unit)
-(close          : handle → m io.error unit)
-(read           : handle → nat → m io.error char_buffer)
-(write          : handle → char_buffer → m io.error unit)
-(get_line       : handle → m io.error char_buffer)
-(stdin          : m io.error handle)
-(stdout         : m io.error handle)
-(stderr         : m io.error handle)
-
-structure io.environment (m : Type → Type → Type) :=
-(get_env : string → m io.error (option string))
--- we don't provide set_env as it is (thread-)unsafe (at least with glibc)
-(get_cwd : m io.error string)
-(set_cwd : string → m io.error unit)
-
-inductive io.process.stdio
-| piped
-| inherit
-| null
-
-structure io.process.spawn_args :=
-/- Command name. -/
-(cmd : string)
-/- Arguments for the process -/
-(args : list string := [])
-/- Configuration for the process' stdin handle. -/
-(stdin := stdio.inherit)
-/- Configuration for the process' stdout handle. -/
-(stdout := stdio.inherit)
-/- Configuration for the process' stderr handle. -/
-(stderr := stdio.inherit)
-/- Working directory for the process. -/
-(cwd : option string := none)
-/- Environment variables for the process. -/
-(env : list (string × option string) := [])
-
-structure io.process (handle : Type) (m : Type → Type → Type) :=
-(child : Type) (stdin : child → handle) (stdout : child → handle) (stderr : child → handle)
-(spawn : io.process.spawn_args → m io.error child)
-(wait : child → m io.error nat)
-
-class io.interface :=
-(m        : Type → Type → Type)
-(monad    : Π e, monad (m e))
-(catch    : Π e₁ e₂ α, m e₁ α → (e₁ → m e₂ α) → m e₂ α)
-(fail     : Π e α, e → m e α)
-(iterate  : Π e α, α → (α → m e (option α)) → m e α)
--- Primitive Types
-(handle   : Type)
--- Interface Extensions
-(term     : io.terminal m)
-(fs       : io.file_system handle m)
-(process  : io.process handle m)
-(env      : io.environment m)
-
-variable [ioi : io.interface]
-include ioi
-
-def io_core (e : Type) (α : Type) :=
-io.interface.m e α
+instance io_core_is_alternative : alternative (io_core io.error) :=
+monad_io_is_alternative io_core
 
 @[reducible] def io (α : Type) :=
 io_core io.error α
 
-instance io_core_is_monad (e : Type) : monad (io_core e) :=
-io.interface.monad e
-
-protected def io.fail {α : Type} (s : string) : io α :=
-io.interface.fail io.error α (io.error.other s)
-
-instance : monad_fail io :=
-{ fail := @io.fail _, ..io_core_is_monad io.error }
-
 namespace io
+/- Remark: the following definitions can be generalized and defined for any (m : Type -> Type -> Type)
+   that implements the required type classes. However, the generalized versions are very inconvenient to use,
+   (example: `#eval io.put_str "hello world"` does not work because we don't have enough information to infer `m`.).
+-/
 def iterate {e α} (a : α) (f : α → io_core e (option α)) : io_core e α :=
-interface.iterate e α a f
+monad_io.iterate e α a f
 
 def forever {e} (a : io_core e unit) : io_core e unit :=
 iterate () $ λ _, a >> return (some ())
 
+-- TODO(Leo): delete after we merge #1881
 def catch {e₁ e₂ α} (a : io_core e₁ α) (b : e₁ → io_core e₂ α) : io_core e₂ α :=
-interface.catch e₁ e₂ α a b
+monad_io.catch e₁ e₂ α a b
 
 def finally {α e} (a : io_core e α) (cleanup : io_core e unit) : io_core e α := do
 res ← catch (sum.inr <$> a) (return ∘ sum.inl),
 cleanup,
 match res with
 | sum.inr res := return res
-| sum.inl error := io.interface.fail _ _ error
+| sum.inl error := monad_io.fail _ _ _ error
 end
 
-instance : alternative io :=
-{ orelse := λ _ a b, catch a (λ _, b),
-  failure := λ _, io.fail "failure",
-  ..interface.monad _ }
+protected def fail {α : Type} (s : string) : io α :=
+monad_io.fail io_core _ _ (io.error.other s)
 
 def put_str : string → io unit :=
-interface.term.put_str
+monad_io_terminal.put_str io_core
 
 def put_str_ln (s : string) : io unit :=
 put_str s >> put_str "\n"
 
 def get_line : io string :=
-interface.term.get_line
+monad_io_terminal.get_line io_core
 
 def cmdline_args : io (list string) :=
-return interface.term.cmdline_args
+return (monad_io_terminal.cmdline_args io_core)
 
 def print {α} [has_to_string α] (s : α) : io unit :=
 put_str ∘ to_string $ s
@@ -136,50 +70,50 @@ def print_ln {α} [has_to_string α] (s : α) : io unit :=
 print s >> put_str "\n"
 
 def handle : Type :=
-interface.handle
+monad_io.handle io_core
 
 def mk_file_handle (s : string) (m : mode) (bin : bool := ff) : io handle :=
-interface.fs.mk_file_handle s m bin
+monad_io_file_system.mk_file_handle io_core s m bin
 
 def stdin : io handle :=
-interface.fs.stdin
+monad_io_file_system.stdin io_core
 
 def stderr : io handle :=
-interface.fs.stderr
+monad_io_file_system.stderr io_core
 
 def stdout : io handle :=
-interface.fs.stdout
+monad_io_file_system.stdout io_core
 
 namespace env
 
 def get (env_var : string) : io (option string) :=
-interface.env.get_env env_var
+monad_io_environment.get_env io_core env_var
 
 /-- get the current working directory -/
 def get_cwd : io string :=
-interface.env.get_cwd
+monad_io_environment.get_cwd io_core
 
 /-- set the current working directory -/
 def set_cwd (cwd : string) : io unit :=
-interface.env.set_cwd cwd
+monad_io_environment.set_cwd io_core cwd
 
 end env
 
 namespace fs
 def is_eof : handle → io bool :=
-interface.fs.is_eof
+monad_io_file_system.is_eof
 
 def flush : handle → io unit :=
-interface.fs.flush
+monad_io_file_system.flush
 
 def close : handle → io unit :=
-interface.fs.close
+monad_io_file_system.close
 
 def read : handle → nat → io char_buffer :=
-interface.fs.read
+monad_io_file_system.read
 
 def write : handle → char_buffer → io unit :=
-interface.fs.write
+monad_io_file_system.write
 
 def get_char (h : handle) : io char :=
 do b ← read h 1,
@@ -187,7 +121,7 @@ do b ← read h 1,
    else io.fail "get_char failed"
 
 def get_line : handle → io char_buffer :=
-interface.fs.get_line
+monad_io_file_system.get_line
 
 def put_char (h : handle) (c : char) : io unit :=
 write h (mk_buffer.push_back c)
@@ -214,12 +148,24 @@ do h ← mk_file_handle s io.mode.read bin,
 end fs
 
 namespace proc
-def child : Type := interface.process.child
-def child.stdin : child → handle := interface.process.stdin
-def child.stdout : child → handle := interface.process.stdout
-def child.stderr : child → handle := interface.process.stderr
-def spawn (p : io.process.spawn_args) : io child := interface.process.spawn p
-def wait (c : child) : io nat := interface.process.wait c
+def child : Type :=
+monad_io_process.child io_core
+
+def child.stdin : child → handle :=
+monad_io_process.stdin
+
+def child.stdout : child → handle :=
+monad_io_process.stdout
+
+def child.stderr : child → handle :=
+monad_io_process.stderr
+
+def spawn (p : io.process.spawn_args) : io child :=
+monad_io_process.spawn io_core p
+
+def wait (c : child) : io nat :=
+monad_io_process.wait c
+
 end proc
 
 end io
@@ -238,8 +184,7 @@ format.print (to_fmt a)
 /-- Run the external process specified by `args`.
 
     The process will run to completion with its output captured by a pipe, and
-    read into `string` which is then returned.
--/
+    read into `string` which is then returned. -/
 def io.cmd (args : io.process.spawn_args) : io string :=
 do child ← io.proc.spawn { stdout := io.process.stdio.piped, ..args },
   buf ← io.fs.read_to_end child.stdout,
@@ -247,6 +192,5 @@ do child ← io.proc.spawn { stdout := io.process.stdio.piped, ..args },
   when (exitv ≠ 0) $ io.fail $ "process exited with status " ++ repr exitv,
   return buf.to_string
 
-omit ioi
 /-- Lift a monadic `io` action into the `tactic` monad. -/
-meta constant tactic.run_io {α : Type} : (Π ioi : io.interface, @io ioi α) → tactic α
+meta constant tactic.run_io {α : Type} : io α → tactic α
diff --git a/library/system/io_interface.lean b/library/system/io_interface.lean
new file mode 100644
index 0000000000..ecf3defc98
--- /dev/null
+++ b/library/system/io_interface.lean
@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import data.buffer
+
+inductive io.error
+| other     : string → io.error
+| sys       : nat → io.error
+
+inductive io.mode
+| read | write | read_write | append
+
+inductive io.process.stdio
+| piped
+| inherit
+| null
+
+structure io.process.spawn_args :=
+/- Command name. -/
+(cmd : string)
+/- Arguments for the process -/
+(args : list string := [])
+/- Configuration for the process' stdin handle. -/
+(stdin := stdio.inherit)
+/- Configuration for the process' stdout handle. -/
+(stdout := stdio.inherit)
+/- Configuration for the process' stderr handle. -/
+(stderr := stdio.inherit)
+/- Working directory for the process. -/
+(cwd : option string := none)
+/- Environment variables for the process. -/
+(env : list (string × option string) := [])
+
+class monad_io (m : Type → Type → Type) :=
+[monad    : Π e, monad (m e)]
+-- TODO(Leo): use monad_except after it is merged
+(catch    : Π e₁ e₂ α, m e₁ α → (e₁ → m e₂ α) → m e₂ α)
+(fail     : Π e α, e → m e α)
+(iterate  : Π e α, α → (α → m e (option α)) → m e α)
+-- Primitive Types
+(handle   : Type)
+
+class monad_io_terminal (m : Type → Type → Type) :=
+(put_str      : string → m io.error unit)
+(get_line     : m io.error string)
+(cmdline_args : list string)
+
+open monad_io (handle)
+
+class monad_io_file_system (m : Type → Type → Type) [monad_io m] :=
+/- Remark: in Haskell, they also provide  (Maybe TextEncoding) and  NewlineMode -/
+(mk_file_handle : string → io.mode → bool → m io.error (handle m))
+(is_eof         : (handle m) → m io.error bool)
+(flush          : (handle m) → m io.error unit)
+(close          : (handle m) → m io.error unit)
+(read           : (handle m) → nat → m io.error char_buffer)
+(write          : (handle m) → char_buffer → m io.error unit)
+(get_line       : (handle m) → m io.error char_buffer)
+(stdin          : m io.error (handle m))
+(stdout         : m io.error (handle m))
+(stderr         : m io.error (handle m))
+
+class monad_io_environment (m : Type → Type → Type) :=
+(get_env : string → m io.error (option string))
+-- we don't provide set_env as it is (thread-)unsafe (at least with glibc)
+(get_cwd : m io.error string)
+(set_cwd : string → m io.error unit)
+
+class monad_io_process (m : Type → Type → Type) [monad_io m] :=
+(child  : Type)
+(stdin  : child → (handle m))
+(stdout : child → (handle m))
+(stderr : child → (handle m))
+(spawn  : io.process.spawn_args → m io.error child)
+(wait   : child → m io.error nat)
+
+instance monad_io_is_monad (m : Type → Type → Type) (e : Type) [monad_io m] : monad (m e) :=
+monad_io.monad m e
+
+instance monad_io_is_monad_fail (m : Type → Type → Type) [monad_io m] : monad_fail (m io.error) :=
+{ fail := λ α s, monad_io.fail _ _ _ (io.error.other s),
+  ..monad_io.monad m io.error }
+
+instance monad_io_is_alternative (m : Type → Type → Type) [monad_io m] : alternative (m io.error) :=
+{ orelse  := λ α a b, monad_io.catch _ _ _ a (λ _, b),
+  failure := λ α, monad_io.fail _ _ _ (io.error.other "failure"),
+  ..monad_io.monad m io.error }
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 4175e4b39a..ebd0f1c8ae 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -487,7 +487,6 @@ static environment eval_cmd(parser & p) {
 
     auto run = [&] {
         eval_helper fn(new_env, p.get_options(), fn_name);
-        fn.dependency_injection();
         try {
             if (!fn.try_exec()) {
                 auto r = fn.invoke_fn();
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 6f98110dc9..cae0b58c2b 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -176,6 +176,12 @@ name const * g_int_zero_ne_neg_of_ne = nullptr;
 name const * g_int_decidable_linear_ordered_comm_group = nullptr;
 name const * g_interactive_param_desc = nullptr;
 name const * g_interactive_parse = nullptr;
+name const * g_io_core = nullptr;
+name const * g_monad_io_impl = nullptr;
+name const * g_monad_io_terminal_impl = nullptr;
+name const * g_monad_io_file_system_impl = nullptr;
+name const * g_monad_io_environment_impl = nullptr;
+name const * g_monad_io_process_impl = nullptr;
 name const * g_io = nullptr;
 name const * g_io_interface = nullptr;
 name const * g_is_associative = nullptr;
@@ -558,6 +564,12 @@ void initialize_constants() {
     g_int_decidable_linear_ordered_comm_group = new name{"int", "decidable_linear_ordered_comm_group"};
     g_interactive_param_desc = new name{"interactive", "param_desc"};
     g_interactive_parse = new name{"interactive", "parse"};
+    g_io_core = new name{"io_core"};
+    g_monad_io_impl = new name{"monad_io_impl"};
+    g_monad_io_terminal_impl = new name{"monad_io_terminal_impl"};
+    g_monad_io_file_system_impl = new name{"monad_io_file_system_impl"};
+    g_monad_io_environment_impl = new name{"monad_io_environment_impl"};
+    g_monad_io_process_impl = new name{"monad_io_process_impl"};
     g_io = new name{"io"};
     g_io_interface = new name{"io", "interface"};
     g_is_associative = new name{"is_associative"};
@@ -941,6 +953,12 @@ void finalize_constants() {
     delete g_int_decidable_linear_ordered_comm_group;
     delete g_interactive_param_desc;
     delete g_interactive_parse;
+    delete g_io_core;
+    delete g_monad_io_impl;
+    delete g_monad_io_terminal_impl;
+    delete g_monad_io_file_system_impl;
+    delete g_monad_io_environment_impl;
+    delete g_monad_io_process_impl;
     delete g_io;
     delete g_io_interface;
     delete g_is_associative;
@@ -1323,6 +1341,12 @@ name const & get_int_zero_ne_neg_of_ne_name() { return *g_int_zero_ne_neg_of_ne;
 name const & get_int_decidable_linear_ordered_comm_group_name() { return *g_int_decidable_linear_ordered_comm_group; }
 name const & get_interactive_param_desc_name() { return *g_interactive_param_desc; }
 name const & get_interactive_parse_name() { return *g_interactive_parse; }
+name const & get_io_core_name() { return *g_io_core; }
+name const & get_monad_io_impl_name() { return *g_monad_io_impl; }
+name const & get_monad_io_terminal_impl_name() { return *g_monad_io_terminal_impl; }
+name const & get_monad_io_file_system_impl_name() { return *g_monad_io_file_system_impl; }
+name const & get_monad_io_environment_impl_name() { return *g_monad_io_environment_impl; }
+name const & get_monad_io_process_impl_name() { return *g_monad_io_process_impl; }
 name const & get_io_name() { return *g_io; }
 name const & get_io_interface_name() { return *g_io_interface; }
 name const & get_is_associative_name() { return *g_is_associative; }
diff --git a/src/library/constants.h b/src/library/constants.h
index a2d7bfc999..b3e56461ae 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -178,6 +178,12 @@ name const & get_int_zero_ne_neg_of_ne_name();
 name const & get_int_decidable_linear_ordered_comm_group_name();
 name const & get_interactive_param_desc_name();
 name const & get_interactive_parse_name();
+name const & get_io_core_name();
+name const & get_monad_io_impl_name();
+name const & get_monad_io_terminal_impl_name();
+name const & get_monad_io_file_system_impl_name();
+name const & get_monad_io_environment_impl_name();
+name const & get_monad_io_process_impl_name();
 name const & get_io_name();
 name const & get_io_interface_name();
 name const & get_is_associative_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 6d4e8f774e..5189f5030b 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -171,6 +171,12 @@ int.zero_ne_neg_of_ne
 int.decidable_linear_ordered_comm_group
 interactive.param_desc
 interactive.parse
+io_core
+monad_io_impl
+monad_io_terminal_impl
+monad_io_file_system_impl
+monad_io_environment_impl
+monad_io_process_impl
 io
 io.interface
 is_associative
diff --git a/src/library/eval_helper.cpp b/src/library/eval_helper.cpp
index e7042a1589..3c484149ed 100644
--- a/src/library/eval_helper.cpp
+++ b/src/library/eval_helper.cpp
@@ -22,28 +22,6 @@ eval_helper::eval_helper(environment const & env, options const & opts, name con
     } else {
         throw exception(sstream() << "no vm declaration found for " << m_fn);
     }
-
-    m_io_iface = m_tc.push_local(
-            "_vm_io_iface", mk_constant(get_io_interface_name(), {}),
-            mk_inst_implicit_binder_info());
-}
-
-void eval_helper::dependency_injection() {
-    while (is_pi(m_ty)) {
-        auto arg_ty = m_tc.whnf(binding_domain(m_ty));
-        optional<expr> arg;
-
-        if (is_constant(get_app_fn(arg_ty), get_io_interface_name())) {
-            m_args.push_back(mk_io_interface(m_cmdline_args));
-            arg = m_io_iface;
-        }
-
-        if (arg) {
-            m_ty = m_tc.whnf(instantiate(binding_body(m_ty), *arg));
-        } else {
-            break;
-        }
-    }
 }
 
 vm_obj eval_helper::invoke_fn() {
@@ -57,7 +35,7 @@ vm_obj eval_helper::invoke_fn() {
 }
 
 optional<vm_obj> eval_helper::try_exec_io() {
-    if (is_constant(get_app_fn(m_ty), get_io_name()) && app_arg(app_fn(m_ty)) == m_io_iface) {
+    if (is_app_of(m_ty, get_io_name(), 1)) {
         m_args.push_back(mk_vm_simple(0)); // "world state"
         auto r = invoke_fn();
         if (auto error = is_io_error(r)) {
diff --git a/src/library/eval_helper.h b/src/library/eval_helper.h
index 40c408aff5..5505ba8450 100644
--- a/src/library/eval_helper.h
+++ b/src/library/eval_helper.h
@@ -30,8 +30,6 @@ class eval_helper {
     expr m_ty;
     unsigned m_arity;
 
-    expr m_io_iface;
-
 public:
     eval_helper(environment const & env, options const & opts, name const & fn);
 
@@ -39,7 +37,6 @@ public:
         m_cmdline_args = cmdline_args;
     }
 
-    void dependency_injection();
     vm_obj invoke_fn();
 
     expr const & get_type() const { return m_ty; }
diff --git a/src/library/noncomputable.cpp b/src/library/noncomputable.cpp
index 16dc455a76..d95b7ee2aa 100644
--- a/src/library/noncomputable.cpp
+++ b/src/library/noncomputable.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/fingerprint.h"
 #include "library/trace.h"
 #include "library/quote.h"
+#include "library/constants.h"
 // TODO(Leo): move inline attribute declaration to library
 #include "library/compiler/inliner.h"
 namespace lean {
@@ -61,6 +62,17 @@ struct noncomputable_modification : public modification {
     }
 };
 
+// TODO(Leo): implement better support for extending this set of builtin constants
+static bool is_builtin_extra(name const & n) {
+    return
+        n == get_io_core_name() ||
+        n == get_monad_io_impl_name() ||
+        n == get_monad_io_terminal_impl_name() ||
+        n == get_monad_io_file_system_impl_name() ||
+        n == get_monad_io_environment_impl_name() ||
+        n == get_monad_io_process_impl_name();
+}
+
 static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, name const & n) {
     environment const & env = tc.env();
     if (ext.m_noncomputable.contains(n))
@@ -71,7 +83,7 @@ static bool is_noncomputable(type_checker & tc, noncomputable_ext const & ext, n
     } else if (d.is_axiom() && !tc.is_prop(d.get_type())) {
         return true;
     } else if (d.is_constant_assumption()) {
-        return !env.is_builtin(d.get_name()) && !tc.is_prop(d.get_type());
+        return !env.is_builtin(d.get_name()) && !tc.is_prop(d.get_type()) && !is_builtin_extra(d.get_name());
     } else {
         return false;
     }
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index a290497f4e..17af55e167 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -791,7 +791,7 @@ vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const &
 }
 
 vm_obj tactic_run_io(vm_obj const &, vm_obj const & a, vm_obj const & s) {
-    vm_obj r = invoke(a, mk_io_interface(), mk_vm_unit());
+    vm_obj r = invoke(a, mk_vm_unit());
     if (optional<vm_obj> a = is_io_result(r)) {
         return tactic::mk_success(*a, tactic::to_state(s));
     } else {
diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
index 01a063a108..2a5c2abe3f 100644
--- a/src/library/vm/vm_io.cpp
+++ b/src/library/vm/vm_io.cpp
@@ -24,6 +24,10 @@ Author: Leonardo de Moura
 #include "library/vm/vm_list.h"
 
 namespace lean {
+vm_obj io_core(vm_obj const &, vm_obj const &) {
+    return mk_vm_unit();
+}
+
 vm_obj mk_io_result(vm_obj const & r) {
     return mk_vm_constructor(0, 1, &r);
 }
@@ -59,22 +63,6 @@ static vm_obj cmdline_args_to_obj(std::vector<std::string> const & ss) {
     return to_obj(objs);
 }
 
-/*
-structure io.terminal (m : Type → Type → Type) :=
-(put_str     : string → m io.error unit)
-(get_line    : m io.error string)
-(cmdline_args : list string)
-*/
-static vm_obj mk_terminal(std::vector<std::string> const & cmdline_args) {
-    constexpr size_t num_fields = 3;
-    vm_obj fields[num_fields] = {
-        mk_native_closure(io_put_str),
-        mk_native_closure(io_get_line),
-        cmdline_args_to_obj(cmdline_args),
-    };
-    return mk_vm_constructor(0, num_fields, fields);
-}
-
 struct vm_handle : public vm_external {
     handle_ref m_handle;
     vm_handle(handle_ref const & h):m_handle(h) {}
@@ -272,19 +260,21 @@ static vm_obj fs_stderr(vm_obj const &) {
 }
 
 /*
-(mk_file_handle : string → io.mode → bool → m io.error handle)
-(is_eof         : handle → m io.error bool)
-(flush          : handle → m io.error unit)
-(close          : handle → m io.error unit)
-(read           : handle → nat → m io.error char_buffer)
-(write          : handle → char_buffer → m io.error unit)
-(get_line       : handle → m io.error char_buffer)
-(stdin          : m io.error handle)
-(stdout         : m io.error handle)
-(stderr         : m io.error handle)
+class monad_io_file_system (m : Type → Type → Type) [monad_io m] :=
+/- Remark: in Haskell, they also provide  (Maybe TextEncoding) and  NewlineMode -/
+(mk_file_handle : string → io.mode → bool → m io.error (handle m))
+(is_eof         : (handle m) → m io.error bool)
+(flush          : (handle m) → m io.error unit)
+(close          : (handle m) → m io.error unit)
+(read           : (handle m) → nat → m io.error string)
+(write          : (handle m) → string → m io.error unit)
+(get_line       : (handle m) → m io.error string)
+(stdin          : m io.error (handle m))
+(stdout         : m io.error (handle m))
+(stderr         : m io.error (handle m))
 */
-static vm_obj mk_fs() {
-    vm_obj fields[11] = {
+static vm_obj monad_io_file_system_impl () {
+    return mk_vm_constructor(0, {
         mk_native_closure(fs_mk_file_handle),
         mk_native_closure(fs_is_eof),
         mk_native_closure(fs_flush),
@@ -294,9 +284,7 @@ static vm_obj mk_fs() {
         mk_native_closure(fs_get_line),
         mk_native_closure(fs_stdin),
         mk_native_closure(fs_stdout),
-        mk_native_closure(fs_stderr)
-    };
-    return mk_vm_constructor(0, 11, fields);
+        mk_native_closure(fs_stderr)});
 }
 
 stdio to_stdio(vm_obj const & o) {
@@ -370,15 +358,15 @@ static vm_obj io_process_wait(vm_obj const & ch, vm_obj const &) {
 }
 
 /*
-structure io.process (Err : Type) (handle : Type) (m : Type → Type → Type) :=
-  (child        : Type)
-  (stdin        : child -> handle)
-  (stdout       : child -> handle)
-  (stderr       : child -> handle)
-  (spawn        : process → m Err child)
-  (wait         : child -> m Err nat)
+class monad_io_process (m : Type → Type → Type) [monad_io m] :=
+(child  : Type)
+(stdin  : child → (handle m))
+(stdout : child → (handle m))
+(stderr : child → (handle m))
+(spawn  : io.process.spawn_args → m io.error child)
+(wait   : child → m io.error nat)
 */
-static vm_obj mk_process() {
+static vm_obj monad_io_process_impl() {
     return mk_vm_constructor(0, {
         mk_native_closure([] (vm_obj const & c) { return to_obj(to_child(c)->get_stdin()); }),
         mk_native_closure([] (vm_obj const & c) { return to_obj(to_child(c)->get_stdout()); }),
@@ -466,13 +454,13 @@ static vm_obj io_set_cwd(vm_obj const & cwd, vm_obj const &) {
 }
 
 /*
-structure io.environment (m : Type → Type → Type) :=
+class monad_io_environment (m : Type → Type → Type) :=
 (get_env : string → m io.error (option string))
 -- we don't provide set_env as it is (thread-)unsafe (at least with glibc)
 (get_cwd : m io.error string)
 (set_cwd : string → m io.error unit)
 */
-static vm_obj mk_io_env() {
+vm_obj monad_io_environment_impl() {
     return mk_vm_constructor(0, {
             mk_native_closure(io_get_env),
             mk_native_closure(io_get_cwd),
@@ -481,35 +469,37 @@ static vm_obj mk_io_env() {
 }
 
 /*
-class io.interface :=
-(m        : Type → Type → Type)
-(monad    : Π e, monad (m e))
+class monad_io (m : Type → Type → Type) :=
+[monad    : Π e, monad (m e)]
+-- TODO(Leo): use monad_except after it is merged
 (catch    : Π e₁ e₂ α, m e₁ α → (e₁ → m e₂ α) → m e₂ α)
 (fail     : Π e α, e → m e α)
 (iterate  : Π e α, α → (α → m e (option α)) → m e α)
 -- Primitive Types
 (handle   : Type)
--- Interface Extensions
-(term     : io.terminal m)
-(fs       : io.file_system handle m)
-(process  : io.process io.error handle m)
-(env      : io.environment _)
 */
-vm_obj mk_io_interface(std::vector<std::string> const & cmdline_args) {
+vm_obj monad_io_impl() {
     return mk_vm_constructor(0, {
         mk_native_closure(io_monad),
         mk_native_closure(io_catch),
         mk_native_closure(io_fail),
-        mk_native_closure(io_iterate),
-        mk_terminal(cmdline_args),
-        mk_fs(),
-        mk_process(),
-        mk_io_env(),
-    });
+        mk_native_closure(io_iterate)});
+    /* field handle is erased */
 }
 
-vm_obj mk_io_interface() {
-    return mk_io_interface({});
+static std::vector<std::string> * g_cmdline_args = nullptr;
+
+/*
+class monad_io_terminal (m : Type → Type → Type) :=
+(put_str      : string → m io.error unit)
+(get_line     : m io.error string)
+(cmdline_args : list string)
+*/
+static vm_obj monad_io_terminal_impl() {
+    return mk_vm_constructor(0, {
+            mk_native_closure(io_put_str),
+            mk_native_closure(io_get_line),
+            cmdline_args_to_obj(*g_cmdline_args)});
 }
 
 optional<vm_obj> is_io_result(vm_obj const & o) {
@@ -542,8 +532,16 @@ std::string io_error_to_string(vm_obj const & o) {
 }
 
 void initialize_vm_io() {
+    DECLARE_VM_BUILTIN(name("io_core"), io_core);
+    DECLARE_VM_BUILTIN(name("monad_io_impl"), monad_io_impl);
+    DECLARE_VM_BUILTIN(name("monad_io_terminal_impl"), monad_io_terminal_impl);
+    DECLARE_VM_BUILTIN(name("monad_io_file_system_impl"), monad_io_file_system_impl);
+    DECLARE_VM_BUILTIN(name("monad_io_environment_impl"), monad_io_environment_impl);
+    DECLARE_VM_BUILTIN(name("monad_io_process_impl"), monad_io_process_impl);
+    g_cmdline_args = new std::vector<std::string>();
 }
 
 void finalize_vm_io() {
+    delete g_cmdline_args;
 }
 }
diff --git a/src/library/vm/vm_io.h b/src/library/vm/vm_io.h
index 07a487dfbb..e232d85d67 100644
--- a/src/library/vm/vm_io.h
+++ b/src/library/vm/vm_io.h
@@ -12,8 +12,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 vm_obj mk_io_result(vm_obj const & r);
-vm_obj mk_io_interface();
-vm_obj mk_io_interface(std::vector<std::string> const & cmdline_args);
 /* The io monad produces a result object, or an error.
    If `o` is a result, then we return the result value. */
 optional<vm_obj> is_io_result(vm_obj const & o);
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 611dae96fe..c96941a80f 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -580,7 +580,6 @@ int main(int argc, char ** argv) {
             scope_trace_env scope2(main_env, main_opts, tc);
 
             try {
-                fn.dependency_injection();
                 if (fn.try_exec()) {
                     return 0;
                 } else {
diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean
index 5cb6567e05..06f5837eaa 100644
--- a/tests/lean/run/check_constants.lean
+++ b/tests/lean/run/check_constants.lean
@@ -176,6 +176,12 @@ run_cmd script_check_id `int.zero_ne_neg_of_ne
 run_cmd script_check_id `int.decidable_linear_ordered_comm_group
 run_cmd script_check_id `interactive.param_desc
 run_cmd script_check_id `interactive.parse
+run_cmd script_check_id `io_core
+run_cmd script_check_id `monad_io_impl
+run_cmd script_check_id `monad_io_terminal_impl
+run_cmd script_check_id `monad_io_file_system_impl
+run_cmd script_check_id `monad_io_environment_impl
+run_cmd script_check_id `monad_io_process_impl
 run_cmd script_check_id `io
 run_cmd script_check_id `io.interface
 run_cmd script_check_id `is_associative