Can adding a constraint cause other constraints to go out of scope?

It's not really a bug; it's expected. In the definition of foo, the context has

1. forall x y. (Eq x, Eq y) => Eq (t x y) (i.e. Eq2 t)
2. Eq a
3. SomeClass t
4. forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y) (from the "closure of the superclass relation over" SomeClass t)

We want Eq (t a a). Well, from the context, there are two axioms whose heads match: (1) with x ~ a, y ~ a and (2) with ob ~ Eq, x ~ a, y ~ a. There is doubt; GHC rejects. (Note that since SomeConstraint t ~ ob is only in the hypothesis of (4), it gets completely ignored; choosing instances pays attention only to instance heads.)

The obvious way forward is to remove (4) from the superclasses of SomeClass. How? Split the quantification from the actual instance "head":

class ob (t x y) => SomeClassSuper ob t x y where
instance ob (t x y) => SomeClassSuper ob t x y where
class (forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y) => SomeClass t where
  type SomeConstraint t :: * -> Constraint

This is what your forall ob. _ => forall x y. _ => _ trick basically did, except this doesn't rely on a bug (your syntax is not allowed). Now, (4) becomes forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y. Because this is not actually a constraint of the form Class args..., it doesn't have superclasses, so GHC doesn't search upwards and find the all-powerful forall ob x y. ob (t x y) head that ruins everything. Now the only instance capable of discharging Eq (t a a) is (1), so we use it.

GHC does search the "superclasses" of the new (4) when it absolutely needs to; the User's Guide actually makes this feature out to be an extension to the base rules above, which come from the original paper. That is, forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => ob (t x y) is still available, but it is considered after all the "true" superclasses in the context (since it isn't actually the superclass of anything).

import Data.Kind

ensure :: forall c x. c => ()
ensure = ()

type Eq2 t = (forall x y. (Eq x, Eq y) => Eq (t x y) :: Constraint)

-- fine
foo :: forall t a. (Eq2 t, Eq a) => ()
foo = ensure @(Eq (t a a))

class ob (t x y) => SomeClassSuper ob t x y where
instance ob (t x y) => SomeClassSuper ob t x y where
class (forall ob x y. (SomeConstraint t ~ ob, ob x, ob y) => SomeClassSuper ob t x y) => SomeClass t where
  type SomeConstraint t :: * -> Constraint

-- also fine
bar :: forall t a. (Eq2 t, Eq a, SomeClass t) => ()
bar = ensure @(Eq (t a a))

-- also also fine
qux :: forall t a. (Eq2 t, Eq a, SomeConstraint t a, SomeClass t) => ()
qux = ensure @(SomeConstraint t (t a a))

You might argue that, in accordance with the open world policy, GHC should backtrack in the face of "incoherence" (such as the overlap between (1) and the original (4)), since quantified constraints can manufacture "incoherence" while there is no actual incoherence and we'd like your code to "just work". That's a perfectly valid want, but GHC is currently being conservative and just giving up instead of backtracking for reasons of performance, simplicity, and predictability.

I think you're running up against the "Reject if in doubt" rule for overlapping axioms. When you bring the SomeClass t constraint into scope, you also introduce the new quantified constraint forall ob x y. (ob x, ob y) => ob (t x y). When it comes time to discharge Eq (t a a), GHC doesn't know whether to use the quantified constraint Eq2 t in foo's signature or the quantified constraint in the SomeClass class, as either one would apply. (As always, GHC doesn't consider SomeConstraint t ~ ob in assessing whether the polymorphic instance applies or not.) There's no mechanism to check that the latter can be "specialized" to the former.

If you delete the Eq2 t constraint from foo:

foo :: forall u t a.
  ( SomeClass t
  , Eq a
  ) => ()
foo = ensure @(Eq (a `t` a)) ()

then you'll get an error "Couldn't match type SomeConstraint t with Eq", suggesting that this is exactly how GHC is trying to solve this constraint. (If you remove the SomeConstraint t ~ ob from the class, it'll even typecheck!)

This doesn't solve your problem, but I think it explains what's going on.