fix(frontends/lean/elaborator): do not expose type information produced when synthesizing class instances

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

src/frontends/lean/elaborator.cpp

@@ -318,12 +318,17 @@ class elaborator {
     /** \brief Auxiliary object for creating backtracking points, and replacing the local scopes. */
     struct new_scope {
         elaborator &           m_main;
+        bool                   m_old_noinfo;
         context::scope_replace m_context_scope;
         context::scope_replace m_full_context_scope;
-        new_scope(elaborator & e, list<expr> const & ctx, list<expr> const & full_ctx):
+        new_scope(elaborator & e, list<expr> const & ctx, list<expr> const & full_ctx, bool noinfo = false):
             m_main(e), m_context_scope(e.m_context, ctx), m_full_context_scope(e.m_full_context, full_ctx) {
+            m_old_noinfo    = m_main.m_noinfo;
+            m_main.m_noinfo = noinfo;
+        }
+        ~new_scope() {
+            m_main.m_noinfo = m_old_noinfo;
         }
-        ~new_scope() {}
     };
 
     struct choice_elaborator {
@@ -424,7 +429,8 @@ class elaborator {
                 pre  = copy_tag(m_meta, ::lean::mk_app(pre, copy_tag(m_meta, mk_strict_expr_placeholder())));
             }
             try {
-                new_scope s(m_elab, m_ctx, m_full_ctx);
+                bool noinfo = true;
+                new_scope s(m_elab, m_ctx, m_full_ctx, noinfo);
                 pair<expr, constraint_seq> rcs = m_elab.visit(pre); // use elaborator to create metavariables, levels, etc.
                 expr r = rcs.first;
                 buffer<constraint> cs;

tests/lean/interactive/class_bug.lean

@@ -0,0 +1,6 @@
+import logic.axioms.hilbert data.nat.basic
+using nonempty inhabited nat
+
+theorem int_inhabited [instance] : inhabited nat := inhabited_mk zero
+
+check epsilon (λ x : nat, true)

tests/lean/interactive/t4.input

@@ -0,0 +1,3 @@
+VISIT class_bug.lean
+WAIT
+INFO 6

tests/lean/interactive/t4.input.expected.out

@@ -0,0 +1,27 @@
+epsilon (λ (x : nat), true) : nat
+-- BEGININFO
+-- TYPE|6|6
+(nat → Prop) → nat
+-- ACK
+-- IDENTIFIER|6|6
+epsilon
+-- ACK
+-- SYMBOL|6|14
+(
+-- ACK
+-- SYMBOL|6|15
+λ
+-- ACK
+-- TYPE|6|21
+Type
+-- ACK
+-- IDENTIFIER|6|21
+nat.nat
+-- ACK
+-- TYPE|6|26
+Prop
+-- ACK
+-- IDENTIFIER|6|26
+true
+-- ACK
+-- ENDINFO