fix: make sure instances created by class command are stored in the new DiscrTree

src/Init/Lean/Class.lean

@@ -147,7 +147,7 @@ registerAttribute {
 }
 
 -- TODO: delete
-@[export lean_add_instance]
+@[export lean_add_instance_old]
 def addGlobalInstanceOld (env : Environment) (instName : Name) : Except String Environment :=
 match env.find instName with
 | none      => Except.error ("unknown declaration '" ++ toString instName ++ "'")

src/Init/Lean/Meta/Instances.lean

@@ -34,6 +34,7 @@ withNewMCtxDepth $ do
   (_, _, type) ← forallMetaTelescopeReducing type;
   DiscrTree.mkPath type
 
+@[export lean_add_instance]
 def addGlobalInstance (env : Environment) (constName : Name) : IO Environment :=
 match env.find constName with
 | none => throw $ IO.userError "unknown constant"

src/library/class.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
+#include "util/io.h"
 #include "library/class.h"
 
 namespace lean {
@@ -13,7 +14,8 @@ extern "C" uint8 lean_is_instance(object* env, object* n);
 extern "C" object* lean_get_class_instances(object* env, object* n);
 extern "C" uint8 lean_is_out_param(object* e);
 extern "C" uint8 lean_has_out_params(object* env, object* n);
-extern "C" object* lean_add_instance(object* env, object* n);
+extern "C" object* lean_add_instance(object* env, object* n, object* w);
+extern "C" object* lean_add_instance_old(object* env, object* n);
 
 bool is_class_out_param(expr const & e) { return lean_is_out_param(e.to_obj_arg()); }
 bool has_class_out_params(environment const & env, name const & c) { return lean_has_out_params(env.to_obj_arg(), c.to_obj_arg()); }
@@ -23,7 +25,9 @@ names get_class_instances(environment const & env, name const & c) { return name
 
 environment add_instance(environment const & env, name const & n, bool persistent) {
     if (!persistent) throw exception("local instances have been disabled");
-    return get_except_value<environment>(lean_add_instance(env.to_obj_arg(), n.to_obj_arg()));
+    environment new_env = get_except_value<environment>(lean_add_instance_old(env.to_obj_arg(), n.to_obj_arg()));
+    new_env = get_io_result<environment>(lean_add_instance(new_env.to_obj_arg(), n.to_obj_arg(), io_mk_world()));
+    return new_env;
 }
 
 static name * g_anonymous_inst_name_prefix = nullptr;