More examples:

example : False := by
  have : Or.inl trivial = Or.inr trivial := rfl
  injection this

example : False := by
  have : HEq (Or.inl trivial) (Or.inr trivial) := HEq.rfl
  contradiction

It looks like reduceCtorEq is affected too, but I haven't been able to configure simp to not use a builtin rule to simplify this to True on its own.

The cases tactic is not affected because it first does an isDefEq check for the LHS and RHS of an equality before doing any further reasoning.

(@leodemoura Lean.Meta.Grind.injection? and Lean.Meta.Grind.propagateCtor are potentially affected by this. There's no problem if the grind framework simplifies away any equalities of the form h1 = h2 where h1 and h2 are proofs.)

@kmill I was able to replicate the issue with simp (see below), but only in the absence of eq_self as a simp lemma—simp appears to try rewriting with eq_self before applying reduceCtorEq, which I think effectively serves as a definitional-equality check. Given that removing this simp lemma seems unlikely, might it not be worth the overhead of adding a check for no-confusion principles in reduceCtorEq? Also, simp reports an error about the nonexistent constant at the tactic site, rather than silently producing an incorrect proof term like injection and contradiction.

As for grind, it looks like propagateCtor already has a check to make sure a no-confusion principle exists; I think injection? shouldn't be affected because it only tries to construct a noConfusion term when there's an equality of matching constructors after the simp in introNext, which for propositional types (and PUnit) shouldn't happen because the simp will reduce away such an equality to True.

Here's the simp example (you can do it with Or too, but that requires eliminating even more simp lemmas):

inductive Or' (a b : Prop) : Prop
  | inl : a → Or' a b
  | inr : b → Or' a b

set_option trace.Meta.Tactic.simp true

attribute [-simp] eq_self  -- Commenting this line toggles the error below
example : False := by
  have h : Or'.inl trivial = Or'.inr trivial := rfl
  simp at h  -- error: unknown constant 'Or'.noConfusion'