fix(kernel/type_checker): add missing test, and kernel_exception has_no_type_exception

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/kernel_exception.cpp

@@ -20,6 +20,10 @@ format already_declared_exception::pp(formatter const &, options const &) const
     return format{format("invalid object declaration, environment already has an object named '"), format(get_name()), format("'")};
 }
 
+format has_no_type_exception::pp(formatter const &, options const &) const {
+    return format{format("object '"), format(const_name(m_const)), format("' has no type associated with it")};
+}
+
 format app_type_mismatch_exception::pp(formatter const & fmt, options const & opts) const {
     unsigned indent     = get_pp_indent(opts);
     context const & ctx = get_context();

src/kernel/kernel_exception.h

@@ -85,6 +85,17 @@ public:
     type_checker_exception(environment const & env):kernel_exception(env) {}
 };
 
+/** \brief Exception for objects that do not have types associated with them */
+class has_no_type_exception : public type_checker_exception {
+    expr m_const;
+public:
+    has_no_type_exception(environment const & env, expr const & c):type_checker_exception(env), m_const(c) {}
+    virtual ~has_no_type_exception() {}
+    virtual expr const & get_main_expr() const { return m_const; }
+    virtual char const * what() const noexcept { return "object does not have a type associated with it"; }
+    virtual format pp(formatter const & fmt, options const & opts) const;
+};
+
 /**
     \brief Exception used to report an application argument type
     mismatch.

src/kernel/type_checker.cpp

@@ -106,9 +106,14 @@ class type_checker::imp {
                 throw unexpected_metavar_occurrence(env(), e);
             }
             break;
-        case expr_kind::Constant:
-            r = env().get_object(const_name(e)).get_type();
+        case expr_kind::Constant: {
+            object const & obj = env().get_object(const_name(e));
+            if (obj.has_type())
+                r = obj.get_type();
+            else
+                throw has_no_type_exception(env(), e);
             break;
+        }
         case expr_kind::Var:
             r = lookup(ctx, var_idx(e));
             break;

src/library/type_inferer.cpp

@@ -114,7 +114,7 @@ class type_inferer::imp {
             if (obj.has_type())
                 return obj.get_type();
             else
-                throw exception("type incorrect expression");
+                throw has_no_type_exception(m_env, e);
             break;
         }
         case expr_kind::Var: {

tests/lua/env1.lua

@@ -6,4 +6,5 @@ e:add_var("N", Type())
 N, M = Consts("N M")
 e:add_var("a", N)
 x, a = Consts("x, a")
-print(e:check_type(fun(x, M, a)))
+check_error(function() e:check_type(fun(x, M, a)) end)
+print(e:check_type(fun(x, N, a)))