diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 624758d670..fe62da1f36 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -3,7 +3,7 @@ for_each_fn.cpp replace_fn.cpp free_vars.cpp abstract.cpp
 instantiate.cpp context.cpp formatter.cpp max_sharing.cpp
 definition.cpp replace_visitor.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp
-constraint.cpp type_checker.cpp error_msgs.cpp
+constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
 )
 
 target_link_libraries(kernel ${LEAN_LIBS})
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index e99a65b673..a1691cb1d9 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -16,8 +16,8 @@ namespace lean {
 */
 class noop_normalizer_extension : public normalizer_extension {
 public:
-    virtual optional<std::pair<expr, constraints>> operator()(expr const &, environment const &, type_checker &) const {
-        return optional<std::pair<expr, constraints>>();
+    virtual optional<expr> operator()(expr const &, extension_context const &) const {
+        return none_expr();
     }
 };
 
@@ -54,6 +54,8 @@ environment::environment(unsigned trust_lvl, bool proof_irrel, bool eta, std::un
     m_extensions(std::make_shared<environment_extensions const>())
 {}
 
+environment::~environment() {}
+
 optional<definition> environment::find(name const & n) const {
     definition const * r = m_definitions.find(n);
     return r ? some_definition(*r) : none_definition();
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 94ce04f0b9..fcc7a102e2 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -30,7 +30,8 @@ class certified_definition;
 */
 class normalizer_extension {
 public:
-    virtual optional<expr> operator()(expr const & e, extension_context const & ctx) const;
+    virtual ~normalizer_extension() {}
+    virtual optional<expr> operator()(expr const & e, extension_context const & ctx) const = 0;
 };
 
 /**