From f59c2f0ef59fdc1833b6ead6adca721123bd7932 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 20 Apr 2018 15:57:50 +0200
Subject: [PATCH] fix(*): revert broken `typed_expr` refactorings

The refactoring will instead be part of Lean 4
---
 library/init/core.lean                       |  3 -
 src/frontends/lean/CMakeLists.txt            |  2 +-
 src/frontends/lean/builtin_cmds.cpp          |  2 +-
 src/frontends/lean/builtin_exprs.cpp         |  2 +-
 src/frontends/lean/calc.cpp                  |  2 +-
 src/frontends/lean/decl_attributes.cpp       |  2 +-
 src/frontends/lean/definition_cmds.cpp       |  2 +-
 src/frontends/lean/elaborator.cpp            |  6 +-
 src/frontends/lean/notation_cmd.cpp          |  2 +-
 src/frontends/lean/parser.cpp                |  2 +-
 src/frontends/lean/pp.cpp                    |  2 +-
 src/frontends/lean/tactic_notation.cpp       |  2 +-
 src/frontends/lean/typed_expr.cpp            | 22 -----
 src/frontends/lean/util.cpp                  |  2 +-
 src/library/CMakeLists.txt                   |  2 +-
 src/library/constants.cpp                    |  4 -
 src/library/constants.h                      |  1 -
 src/library/constants.txt                    |  1 -
 src/library/init_module.cpp                  |  3 +
 src/library/typed_expr.cpp                   | 93 ++++++++++++++++++++
 src/{frontends/lean => library}/typed_expr.h |  6 +-
 tests/lean/run/1954.lean                     |  2 -
 tests/lean/run/check_constants.lean          |  1 -
 tests/lean/run/type_annot_app.lean           | 12 +++
 24 files changed, 128 insertions(+), 50 deletions(-)
 delete mode 100644 src/frontends/lean/typed_expr.cpp
 create mode 100644 src/library/typed_expr.cpp
 rename src/{frontends/lean => library}/typed_expr.h (85%)
 delete mode 100644 tests/lean/run/1954.lean
 create mode 100644 tests/lean/run/type_annot_app.lean

diff --git a/library/init/core.lean b/library/init/core.lean
index c3a8f98dcb..486a11c4fc 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -104,9 +104,6 @@ a
 /-- Gadget for marking output parameters in type classes. -/
 @[reducible] def out_param (α : Sort u) : Sort u := α
 
-/-- Auxiliary declaration used to implement the notation (a : α) -/
-@[reducible] def typed_expr (α : Sort u) (a : α) : α := a
-
 /-
   id_rhs is an auxiliary declaration used in the equation compiler to address performance
   issues when proving equational lemmas. The equation compiler uses it as a marker.
diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt
index cf42fa967d..55e3194c94 100644
--- a/src/frontends/lean/CMakeLists.txt
+++ b/src/frontends/lean/CMakeLists.txt
@@ -9,4 +9,4 @@ prenum.cpp print_cmd.cpp elaborator.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp module_parser.cpp
 interactive.cpp completion.cpp
-user_notation.cpp user_command.cpp typed_expr.cpp)
+user_notation.cpp user_command.cpp)
diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 1c2313c575..7b5194d16e 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "library/private.h"
 #include "library/type_context.h"
 #include "library/reducible.h"
+#include "library/typed_expr.h"
 #include "library/documentation.h"
 #include "library/placeholder.h"
 #include "library/vm/vm.h"
@@ -52,7 +53,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/decl_attributes.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 environment section_cmd(parser & p) {
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index b79f98c104..63b318517b 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/aliases.h"
 #include "library/scoped_ext.h"
+#include "library/typed_expr.h"
 #include "library/choice.h"
 #include "library/constants.h"
 #include "library/quote.h"
@@ -35,7 +36,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/brackets.h"
 #include "frontends/lean/tactic_notation.h"
 #include "frontends/lean/elaborator.h"
-#include "frontends/lean/typed_expr.h"
 
 #ifndef LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE
 #define LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE true
diff --git a/src/frontends/lean/calc.cpp b/src/frontends/lean/calc.cpp
index 1a179f4762..0b5e9af49a 100644
--- a/src/frontends/lean/calc.cpp
+++ b/src/frontends/lean/calc.cpp
@@ -22,11 +22,11 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/scoped_ext.h"
 #include "library/annotation.h"
+#include "library/typed_expr.h"
 #include "library/sorry.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 static name * g_calc_name  = nullptr;
diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index cdf483ef8d..efeaf738d7 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -9,12 +9,12 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/class.h"
 #include "library/num.h"
+#include "library/typed_expr.h"
 #include "library/vm/vm_nat.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 // ==========================================
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index a9cd82ed51..aa1abb7be9 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/constants.h"
 #include "library/explicit.h"
+#include "library/typed_expr.h"
 #include "library/private.h"
 #include "library/protected.h"
 #include "library/scoped_ext.h"
@@ -41,7 +42,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/definition_cmds.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 environment ensure_decl_namespaces(environment const & env, name const & full_n) {
diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index a2c502ad34..ec58b5711f 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/sorry.h"
 #include "library/quote.h"
 #include "library/util.h"
+#include "library/typed_expr.h"
 #include "library/annotation.h"
 #include "library/pp_options.h"
 #include "library/replace_visitor.h"
@@ -62,7 +63,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/structure_instance.h"
 #include "frontends/lean/elaborator.h"
-#include "frontends/lean/typed_expr.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_COERCIONS
 #define LEAN_DEFAULT_ELABORATOR_COERCIONS true
@@ -3306,6 +3306,8 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
         return visit_anonymous_constructor(e, expected_type);
     } else if (is_prenum(e)) {
         return visit_prenum(e, expected_type);
+    } else if (is_typed_expr(e)) {
+        return visit_typed_expr(e);
     } else if (is_choice(e) || is_explicit(e) || is_partial_explicit(e)) {
         return visit_app_core(e, buffer<expr>(), expected_type, e);
     } else if (is_by(e)) {
@@ -3565,8 +3567,6 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
     return recover_expr_from_exception(expected_type, e, [&] () -> expr {
         if (is_placeholder(e)) {
             return visit_placeholder(e, expected_type);
-        } else if (is_typed_expr(e)) {
-            return visit_typed_expr(e);
         } else if (is_have_expr(e)) {
             return copy_tag(e, visit_have_expr(e, expected_type));
         } else if (is_suffices_annotation(e)) {
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 117f353436..5a6e0810f6 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -16,12 +16,12 @@ Author: Leonardo de Moura
 #include "library/num.h"
 #include "library/aliases.h"
 #include "library/constants.h"
+#include "library/typed_expr.h"
 #include "library/vm/vm_nat.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/decl_attributes.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 static std::string parse_symbol(parser & p, char const * msg) {
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 26abc71aa6..b81639978c 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -41,6 +41,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/scoped_ext.h"
 #include "library/explicit.h"
+#include "library/typed_expr.h"
 #include "library/num.h"
 #include "library/string.h"
 #include "library/sorry.h"
@@ -63,7 +64,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/local_context_adapter.h"
 #include "frontends/lean/structure_instance.h"
-#include "frontends/lean/typed_expr.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index c3014b5fb2..ead88c0524 100755
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "library/protected.h"
 #include "library/quote.h"
 #include "library/explicit.h"
+#include "library/typed_expr.h"
 #include "library/num.h"
 #include "library/util.h"
 #include "library/print.h"
@@ -51,7 +52,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/tokens.h"
-#include "frontends/lean/typed_expr.h"
 
 #include "library/trace.h"
 
diff --git a/src/frontends/lean/tactic_notation.cpp b/src/frontends/lean/tactic_notation.cpp
index b3a74fd5d8..a0d31288ed 100644
--- a/src/frontends/lean/tactic_notation.cpp
+++ b/src/frontends/lean/tactic_notation.cpp
@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/quote.h"
 #include "library/io_state_stream.h"
 #include "library/trace.h"
+#include "library/typed_expr.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
 #include "kernel/scope_pos_info_provider.h"
@@ -28,7 +29,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/builtin_exprs.h"
-#include "frontends/lean/typed_expr.h"
 
 /* The auto quotation currently supports two classes of tactics: tactic and smt_tactic.
    To add a new class Tac, we have to
diff --git a/src/frontends/lean/typed_expr.cpp b/src/frontends/lean/typed_expr.cpp
deleted file mode 100644
index bda53961d6..0000000000
--- a/src/frontends/lean/typed_expr.cpp
+++ /dev/null
@@ -1,22 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "library/util.h"
-#include "library/constants.h"
-
-namespace lean {
-bool is_typed_expr(expr const & e) {
-    return is_app_of(e, get_typed_expr_name(), 2);
-}
-
-expr mk_typed_expr(expr const & t, expr const & v) {
-    return mk_app(mk_constant(get_typed_expr_name()), t, v);
-}
-
-expr get_typed_expr_type(expr const & e) { lean_assert(is_typed_expr(e)); return app_arg(app_fn(e)); }
-expr get_typed_expr_expr(expr const & e) { lean_assert(is_typed_expr(e)); return app_arg(e); }
-}
diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp
index 2f3132de6e..c3a15dc5f9 100644
--- a/src/frontends/lean/util.cpp
+++ b/src/frontends/lean/util.cpp
@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/aliases.h"
 #include "library/constants.h"
+#include "library/typed_expr.h"
 #include "library/placeholder.h"
 #include "library/unfold_macros.h"
 #include "library/choice.h"
@@ -35,7 +36,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/decl_util.h" // TODO(Leo): remove
 #include "frontends/lean/prenum.h"
-#include "frontends/lean/typed_expr.h"
 
 #ifndef LEAN_DEFAULT_AUTO_PARAM_CHECK_EXISTS
 #define LEAN_DEFAULT_AUTO_PARAM_CHECK_EXISTS true
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index f519d2db5a..25f676babc 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -5,7 +5,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   update_declaration.cpp scoped_ext.cpp sorry.cpp replace_visitor.cpp
   explicit.cpp num.cpp string.cpp head_map.cpp
   class.cpp util.cpp print.cpp annotation.cpp quote.cpp
-  protected.cpp reducible.cpp init_module.cpp
+  typed_expr.cpp protected.cpp reducible.cpp init_module.cpp
   exception.cpp fingerprint.cpp pp_options.cpp
   unfold_macros.cpp app_builder.cpp projection.cpp relation_manager.cpp
   export.cpp user_recursors.cpp idx_metavar.cpp noncomputable.cpp
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 8c038e2c27..6033ef7420 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -341,7 +341,6 @@ name const * g_trans_rel_left = nullptr;
 name const * g_trans_rel_right = nullptr;
 name const * g_true = nullptr;
 name const * g_true_intro = nullptr;
-name const * g_typed_expr = nullptr;
 name const * g_unification_hint = nullptr;
 name const * g_unification_hint_mk = nullptr;
 name const * g_unit = nullptr;
@@ -699,7 +698,6 @@ void initialize_constants() {
     g_trans_rel_right = new name{"trans_rel_right"};
     g_true = new name{"true"};
     g_true_intro = new name{"true", "intro"};
-    g_typed_expr = new name{"typed_expr"};
     g_unification_hint = new name{"unification_hint"};
     g_unification_hint_mk = new name{"unification_hint", "mk"};
     g_unit = new name{"unit"};
@@ -1058,7 +1056,6 @@ void finalize_constants() {
     delete g_trans_rel_right;
     delete g_true;
     delete g_true_intro;
-    delete g_typed_expr;
     delete g_unification_hint;
     delete g_unification_hint_mk;
     delete g_unit;
@@ -1416,7 +1413,6 @@ name const & get_trans_rel_left_name() { return *g_trans_rel_left; }
 name const & get_trans_rel_right_name() { return *g_trans_rel_right; }
 name const & get_true_name() { return *g_true; }
 name const & get_true_intro_name() { return *g_true_intro; }
-name const & get_typed_expr_name() { return *g_typed_expr; }
 name const & get_unification_hint_name() { return *g_unification_hint; }
 name const & get_unification_hint_mk_name() { return *g_unification_hint_mk; }
 name const & get_unit_name() { return *g_unit; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 93dd41a09e..62f36ae1ee 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -343,7 +343,6 @@ name const & get_trans_rel_left_name();
 name const & get_trans_rel_right_name();
 name const & get_true_name();
 name const & get_true_intro_name();
-name const & get_typed_expr_name();
 name const & get_unification_hint_name();
 name const & get_unification_hint_mk_name();
 name const & get_unit_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index ef8a368f86..2d981cb3dc 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -336,7 +336,6 @@ trans_rel_left
 trans_rel_right
 true
 true.intro
-typed_expr
 unification_hint
 unification_hint.mk
 unit
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 4b28e16f9b..1fcab9d39e 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/constants.h"
 #include "library/kernel_serializer.h"
+#include "library/typed_expr.h"
 #include "library/choice.h"
 #include "library/class.h"
 #include "library/num.h"
@@ -84,6 +85,7 @@ void initialize_library_module() {
     initialize_idx_metavar();
     initialize_io_state();
     initialize_kernel_serializer();
+    initialize_typed_expr();
     initialize_choice();
     initialize_string();
     initialize_num();
@@ -157,6 +159,7 @@ void finalize_library_module() {
     finalize_num();
     finalize_string();
     finalize_choice();
+    finalize_typed_expr();
     finalize_kernel_serializer();
     finalize_io_state();
     finalize_idx_metavar();
diff --git a/src/library/typed_expr.cpp b/src/library/typed_expr.cpp
new file mode 100644
index 0000000000..fe3fdf2201
--- /dev/null
+++ b/src/library/typed_expr.cpp
@@ -0,0 +1,93 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "kernel/error_msgs.h"
+#include "kernel/kernel_exception.h"
+#include "kernel/abstract_type_context.h"
+#include "library/util.h"
+#include "library/kernel_serializer.h"
+
+namespace lean {
+static name * g_typed_expr_name = nullptr;
+static std::string * g_typed_expr_opcode = nullptr;
+static macro_definition * g_typed_expr = nullptr;
+
+name const & get_typed_expr_name() { return *g_typed_expr_name; }
+std::string const & get_typed_expr_opcode() { return *g_typed_expr_opcode; }
+
+/** \brief This macro is used to "enforce" a given type to an expression.
+    It is equivalent to
+
+        definition typed_expr (A : Type) (a : A) := a
+
+    We use a macro instead of the definition because we want to be able
+    to use in any environment, even one that does not contain the
+    definition such as typed_expr.
+
+    The macro is also slightly for efficient because we don't need a
+    universe parameter.
+*/
+class typed_expr_macro_definition_cell : public macro_definition_cell {
+    void check_macro(expr const & m) const {
+        if (!is_macro(m) || macro_num_args(m) != 2)
+            throw exception("invalid typed-expr, incorrect number of arguments");
+    }
+public:
+    virtual name get_name() const { return get_typed_expr_name(); }
+    virtual expr check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
+        check_macro(m);
+        expr given_type = macro_arg(m, 0);
+        if (!infer_only) {
+            ctx.check(given_type, infer_only);
+            expr inferred_type = ctx.check(macro_arg(m, 1), infer_only);
+            if (!ctx.is_def_eq(inferred_type, given_type)) {
+                throw_kernel_exception(ctx.env(), m, [=](formatter const & fmt) {
+                    return format("type mismatch at term") + pp_type_mismatch(fmt, macro_arg(m, 1), inferred_type, given_type);
+                });
+            }
+        }
+        return given_type;
+    }
+    virtual optional<expr> expand(expr const & m, abstract_type_context &) const {
+        check_macro(m);
+        return some_expr(macro_arg(m, 1));
+    }
+    virtual void write(serializer & s) const {
+        s.write_string(get_typed_expr_opcode());
+    }
+};
+
+bool is_typed_expr(expr const & e) {
+    return is_macro(e) && macro_def(e) == *g_typed_expr;
+}
+
+expr mk_typed_expr(expr const & t, expr const & v) {
+    expr args[2] = {t, v};
+    return mk_macro(*g_typed_expr, 2, args);
+}
+
+expr get_typed_expr_type(expr const & e) { lean_assert(is_typed_expr(e)); return macro_arg(e, 0); }
+expr get_typed_expr_expr(expr const & e) { lean_assert(is_typed_expr(e)); return macro_arg(e, 1); }
+
+void initialize_typed_expr() {
+    g_typed_expr_name = new name("typed_expr");
+    g_typed_expr_opcode = new std::string("TyE");
+    g_typed_expr = new macro_definition(new typed_expr_macro_definition_cell());
+    register_macro_deserializer(*g_typed_expr_opcode,
+                                [](deserializer &, unsigned num, expr const * args) {
+                                    if (num != 2)
+                                        throw corrupted_stream_exception();
+                                    return mk_typed_expr(args[0], args[1]);
+                                });
+}
+
+void finalize_typed_expr() {
+    delete g_typed_expr;
+    delete g_typed_expr_opcode;
+    delete g_typed_expr_name;
+}
+}
diff --git a/src/frontends/lean/typed_expr.h b/src/library/typed_expr.h
similarity index 85%
rename from src/frontends/lean/typed_expr.h
rename to src/library/typed_expr.h
index 4492796a6c..78ef36d6df 100644
--- a/src/frontends/lean/typed_expr.h
+++ b/src/library/typed_expr.h
@@ -19,6 +19,10 @@ bool is_typed_expr(expr const & e);
 expr get_typed_expr_type(expr const & e);
 /** \brief Return the expression/denotation of a typed expression
 
-    \remark get_typed_expr_type(mk_typed_expr(t, e)) == e */
+    \remark get_typed_expr_type(mk_typed_expr(t, e)) == e
+*/
 expr get_typed_expr_expr(expr const & e);
+
+void initialize_typed_expr();
+void finalize_typed_expr();
 }
diff --git a/tests/lean/run/1954.lean b/tests/lean/run/1954.lean
deleted file mode 100644
index e9e000a563..0000000000
--- a/tests/lean/run/1954.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-def all (p : ℕ → Prop) : Prop := ∀x, p x
-example {p : ℕ → Prop} (h : all p) : p 0 := ‹all p› 0
diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean
index 9d29b68f79..10eec90e04 100644
--- a/tests/lean/run/check_constants.lean
+++ b/tests/lean/run/check_constants.lean
@@ -341,7 +341,6 @@ run_cmd script_check_id `trans_rel_left
 run_cmd script_check_id `trans_rel_right
 run_cmd script_check_id `true
 run_cmd script_check_id `true.intro
-run_cmd script_check_id `typed_expr
 run_cmd script_check_id `unification_hint
 run_cmd script_check_id `unification_hint.mk
 run_cmd script_check_id `unit
diff --git a/tests/lean/run/type_annot_app.lean b/tests/lean/run/type_annot_app.lean
new file mode 100644
index 0000000000..d11a674a84
--- /dev/null
+++ b/tests/lean/run/type_annot_app.lean
@@ -0,0 +1,12 @@
+def f : ℕ → ℕ := λ _, 0
+
+theorem A (x : ℕ) : f x = 0 := rfl
+theorem B (x : ℕ) : (f : _) x = 0 := rfl
+theorem C (x : ℕ) : (f : ℕ → ℕ) x = 0 := rfl
+
+example (x) : f x = 0 := by simp [A] --ok
+example (x) : f x = 0 := by have := A x; rw this --ok
+example (x) : f x = 0 := by simp [B] --fails
+example (x) : f x = 0 := by have := B x; rw this --fails
+example (x) : f x = 0 := by simp [C] --fails
+example (x) : f x = 0 := by have := C x; rw this --fails