diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp
index 8e35fb43a2..f9f078ca51 100644
--- a/src/library/compiler/extern_attribute.cpp
+++ b/src/library/compiler/extern_attribute.cpp
@@ -13,6 +13,7 @@ Authors: Leonardo de Moura
 #include "library/attribute_manager.h"
 #include "library/compiler/borrowed_annotation.h"
 #include "library/compiler/util.h"
+#include "library/compiler/ir.h"
 #include "library/compiler/extern_attribute.h"
 
 namespace lean {
@@ -317,8 +318,16 @@ optional<expr> get_extern_constant_ll_type(environment const & env, name const &
 void initialize_extern_attribute() {
     g_all = new name("all");
     register_system_attribute(extern_attr("extern", "builtin and foreign functions",
-                                          [](environment const & env, io_state const &, name const &, unsigned, bool persistent) {
+                                          [](environment const & env, io_state const &, name const & n, unsigned, bool persistent) {
                                               if (!persistent) throw exception("invalid [extern] attribute, it must be persistent");
+                                              if (optional<constant_info> cinfo = env.find(n)) {
+                                                  if (cinfo->is_constructor()) {
+                                                      /* Hack: we can mark constructors as `extern`.
+                                                         The compiler is not invoked for constructors. So, we
+                                                         register them in the IR here. */
+                                                      return ir::add_extern(env, n);
+                                                  }
+                                              }
                                               return env;
                                           }));
 }
diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp
index 1d680c956b..10755e2b54 100644
--- a/src/library/compiler/ir.cpp
+++ b/src/library/compiler/ir.cpp
@@ -472,7 +472,6 @@ public:
 
     /* Convert extern constant into a IR.Decl */
     ir::decl operator()(name const & fn) {
-        lean_assert(is_extern_constant(env(), fn));
         buffer<bool> borrow; bool dummy;
         get_extern_borrowed_info(env(), fn, borrow, dummy);
         buffer<ir::param> xs;