diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp
index f6014e421c..59832d0d16 100644
--- a/src/library/derive_attribute.cpp
+++ b/src/library/derive_attribute.cpp
@@ -89,7 +89,7 @@ static environment derive(environment env, options const & opts, name const & n,
         for (unsigned i = 0; i < tgt_num_args - expected_tgt_num_args && is_binding(tgt_ty); i++) {
             auto param = ctx.push_local_from_binding(tgt_ty);
             tgt = mk_app(tgt, param);
-            real_tgt = mk_app(real_tgt, param);
+            real_tgt = beta_reduce(mk_app(real_tgt, param));
             params.push_back(param);
             tgt_ty = instantiate(binding_body(tgt_ty), param);
         }
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 2cef0e927e..5ab8542320 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -3445,6 +3445,24 @@ struct instance_synthesizer {
                 r    = mk_app(r, new_arg);
                 type = instantiate(binding_body(type), new_arg);
             }
+
+            /* simple pre-filter: Discard applications of the same class where the last argument's heads are different
+             * and both nonreducible.
+             * Furthermore, we don't even list these "trivially non-applicable instances" in the class_instances trace,
+             * which can drastically reduce the noise in it. */
+            if (is_app(mvar_type) && const_name(get_app_fn(mvar_type)) == const_name(get_app_fn(type))) {
+                auto const & m_head = beta_reduce(get_app_fn(m_ctx.instantiate_mvars(app_arg(mvar_type))));
+                auto const & t_head = get_app_fn(app_arg(type));
+                if (is_const(m_head) && is_const(t_head) && const_name(m_head) != const_name(t_head) &&
+                        !m_ctx.is_delta(m_head) && !m_ctx.is_projection(m_head) &&
+                        !m_ctx.is_delta(t_head) && !m_ctx.is_projection(t_head)) {
+                    // lean_trace_plain("class_instances",
+                    //                  scope_trace_env scope(m_ctx.env(), m_ctx);
+                    //                  tout() << "PRE-FILTER: " << const_name(m_head) << " " << const_name(t_head) << "\n";);
+                    return false;
+                }
+            }
+
             lean_trace_plain("class_instances",
                              scope_trace_env scope(m_ctx.env(), m_ctx);
                              trace(e.m_depth, mk_app(mvar, locals.as_buffer()), mvar_type, r););