`@[ext]` generates highly general theorem patterns without warning

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Consider:

import Lean

open Lean Meta

class Injects (H : Type u) (X : outParam (Type v)) where
  coe : H → X
  injective : Function.Injective coe

@[ext] theorem Injects.ext {H : Type u} {X : Type v} [Injects H X]
    {a b : H} (h : Injects.coe a = Injects.coe b) : a = b := Injects.injective h


structure Foo where
  x : BitVec 8

#eval Ext.getExtTheorems (mkConst ``Foo)

This returns Injects.ext because it is a theorem that can apply to any type in principle and thus has a * discr tree key. The only way to know is to run the Injects TC query. Arguably this is a potentially dangerous lemma to register.

Expected behavior: ext should warn or refuse to register the theorem

Actual behavior: the theorem is silently accepted

Versions

Lean 4.34.0-nightly-2026-07-22

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the minimal reproduction using @[ext], Ext.getExtTheorems, and the Injects.ext theorem after importing Lean. Trace how the ext attribute registers theorem patterns and how the discrimination-tree key is chosen. Done means the overly general theorem is warned about or refused, with the reproduction covered by a regression test.