diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 83e4ad6891..6f4214f4f1 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -456,6 +456,7 @@ static environment eval_cmd(parser & p) {
 
     type_context tc(p.env(), transparency_mode::All);
     auto type = tc.infer(e);
+    bool has_repr_inst = false;
 
     /* Check if resultant type has an instance of has_repr */
     try {
@@ -463,8 +464,9 @@ static environment eval_cmd(parser & p) {
         optional<expr> repr_instance = tc.mk_class_instance(has_repr_type);
         if (repr_instance) {
             /* Modify the 'program' to (repr e) */
-            e         = mk_app(tc, get_repr_name(), type, *repr_instance, e);
-            type      = tc.infer(e);
+            e             = mk_app(tc, get_repr_name(), type, *repr_instance, e);
+            type          = tc.infer(e);
+            has_repr_inst = true;
         }
     } catch (exception &) {}
 
@@ -490,6 +492,9 @@ static environment eval_cmd(parser & p) {
             if (!fn.try_exec()) {
                 auto r = fn.invoke_fn();
                 should_report = true;
+                if (!has_repr_inst) {
+                    (p.mk_message(p.cmd_pos(), WARNING) << "result type does not have an instance of type class 'has_repr', dumping internal representation").report();
+                }
                 if (is_constant(fn.get_type(), get_string_name())) {
                     out << to_string(r);
                 } else {
diff --git a/tests/lean/1861.lean.expected.out b/tests/lean/1861.lean.expected.out
index e32cbfe5d6..e7fb137a01 100644
--- a/tests/lean/1861.lean.expected.out
+++ b/tests/lean/1861.lean.expected.out
@@ -1,4 +1,6 @@
+1861.lean:3:0: warning: result type does not have an instance of type class 'has_repr', dumping internal representation
 #2147483647
 -1
 -1
+1861.lean:22:0: warning: result type does not have an instance of type class 'has_repr', dumping internal representation
 (#0 #1)