diff --git a/library/init/lean/declaration.lean b/library/init/lean/declaration.lean
index fb398a4dcb..c4c48dfc51 100644
--- a/library/init/lean/declaration.lean
+++ b/library/init/lean/declaration.lean
@@ -166,5 +166,11 @@ def hints : ConstantInfo → ReducibilityHints
 | defnInfo {hints := r, ..} => r
 | _                         => ReducibilityHints.opaque
 
+@[extern "lean_instantiate_type_lparams"]
+constant instantiateTypeUnivParams (c : ConstantInfo) (ls : List Level) : Expr := default _
+
+@[extern "lean_instantiate_value_lparams"]
+constant instantiateValueUnivParams (c : ConstantInfo) (ls : List Level) : Expr := default _
+
 end ConstantInfo
 end Lean
diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index a37405749e..aa4c5cabda 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -245,7 +245,8 @@ MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_type_univ_cache, LEAN_INST_UNIV_
 MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_value_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
 
 expr instantiate_type_lparams(constant_info const & info, levels const & ls) {
-    lean_assert(info.get_num_lparams() == length(ls));
+    if (info.get_num_lparams() != length(ls))
+        lean_panic("#universes mismatch at instantiateTypeUnivParams");
     if (is_nil(ls) || !has_param_univ(info.get_type()))
         return info.get_type();
     instantiate_univ_cache & cache = get_type_univ_cache();
@@ -257,7 +258,8 @@ expr instantiate_type_lparams(constant_info const & info, levels const & ls) {
 }
 
 expr instantiate_value_lparams(constant_info const & info, levels const & ls) {
-    lean_assert(info.get_num_lparams() == length(ls));
+    if (info.get_num_lparams() != length(ls))
+        lean_panic("#universes mismatch at instantiateValueUnivParams");
     if (is_nil(ls) || !has_param_univ(info.get_value()))
         return info.get_value();
     instantiate_univ_cache & cache = get_value_univ_cache();
@@ -268,6 +270,18 @@ expr instantiate_value_lparams(constant_info const & info, levels const & ls) {
     return r;
 }
 
+extern "C" object * lean_instantiate_type_lparams(object * info0, object * ls0) {
+    constant_info const & a = reinterpret_cast<constant_info const &>(info0);
+    levels const & ls = reinterpret_cast<levels const &>(ls0);
+    return instantiate_type_lparams(a, ls).steal();
+}
+
+extern "C" object * lean_instantiate_value_lparams(object * info0, object * ls0) {
+    constant_info const & a = reinterpret_cast<constant_info const &>(info0);
+    levels const & ls = reinterpret_cast<levels const &>(ls0);
+    return instantiate_value_lparams(a, ls).steal();
+}
+
 void clear_instantiate_cache() {
     get_type_univ_cache().clear();
     get_value_univ_cache().clear();
diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean
new file mode 100644
index 0000000000..6d40aa9162
--- /dev/null
+++ b/tests/lean/run/instuniv.lean
@@ -0,0 +1,14 @@
+import init.lean
+open Lean
+
+def tst : IO Unit :=
+do env ← importModules [`init.data.array.default];
+   match env.find `Array.foldl with
+   | some info => do
+     IO.println (info.instantiateTypeUnivParams [Level.zero, Level.zero]);
+     IO.println (info.instantiateValueUnivParams [Level.zero, Level.zero]);
+     pure ()
+   | none      => IO.println ("Array.foldl not found");
+   pure ()
+
+#eval tst