diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index b7a6aa00a8..2dd47b3b35 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -13,12 +13,14 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 #include "library/util.h"
 #include "library/quote.h"
+#include "library/replace_visitor.h"
 #include "library/vm/vm.h"
 #include "library/vm/optimize.h"
 #include "library/compiler/simp_inductive.h"
 #include "library/compiler/erase_irrelevant.h"
 #include "library/compiler/nat_value.h"
 #include "library/compiler/preprocess.h"
+#include "library/compiler/comp_irrelevant.h"
 
 namespace lean {
 class vm_compiler_fn {
@@ -235,11 +237,21 @@ class vm_compiler_fn {
         }
     }
 
+    class elim_comp_irrelevant_marks_fn : public replace_visitor {
+        virtual expr visit_macro(expr const & e) override {
+            if (is_marked_as_comp_irrelevant(e))
+                return visit(get_annotation_arg(e));
+            else
+                return replace_visitor::visit_macro(e);
+        }
+    };
+
     optional<expr> to_type_info(expr const & t) {
-        if (!is_neutral_expr(t) && closed(t))
-            return some_expr(t);
-        else
+        if (!is_neutral_expr(t) && closed(t) && !has_param_univ(t)) {
+            return some_expr(elim_comp_irrelevant_marks_fn()(t));
+        } else {
             return none_expr();
+        }
     }
 
     void compile_let(expr e, unsigned bpz, name_map<unsigned> const & m) {
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index 31d2c56b27..2b3fe6ce07 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -1758,6 +1758,7 @@ unsigned vm_state::pop_frame() {
 
 void vm_state::invoke_global(vm_decl const & d) {
 #if 0
+    std::cout << d.get_name() << "\n";
     for (auto info : d.get_args_info()) {
         std::cout << info.first << " : ";
         if (info.second)
@@ -1766,6 +1767,7 @@ void vm_state::invoke_global(vm_decl const & d) {
             std::cout << "none";
         std::cout << "\n";
     }
+    std::cout << "----------\n";
 #endif
     push_frame(d.get_arity(), m_pc+1, d.get_idx());
     m_code            = d.get_code();