Type family injectivity annotation is rejected with type variable rhs, even on non-endomorphism

In Injective Type Families for Haskell, the following explanation is given for rejecting bare type variables on RHS:

type family W1 a = r | r -> a
type instance W1 [a] = a

To a mathematician this function certainly looks injective. But, surprisingly, it does not satisfy Definition 1! Here is a counterexample. Clearly we do have a proof of (W1 [W1 Int ] ∼ W1 Int), simply by instantiating the type instance with [a |-> W1 Int]. But if W1 was injective in the sense of Definition 1, we could derive a proof of [W1 Int ] ∼ Int, and that is plainly false!

Similarly:

type family W2 a = r | r -> a
type instance W2 [a] = W2 a

Again W2 looks injective. But we can prove W2 [Int] ∼ W2 Int, simply by instantiating the type instance; then by Definition 1, we could then conclude [Int] ∼ Int, which is plainly false. So neither W1 nor W2 are injective, according to our definition. Note that the partiality of W1 and W2 is critical for the failure case to occur.

In addition to exploiting partiality, the first example also requires W1 to be an endomorphism, and the second one depends on [] being an endomorphism.

So why is the following example still rejected, where the type family is not an endomorphism and not recursive; in fact, even total?

newtype Wrapper = Wrap Type

type family Unwrap (x :: Wrapper) = (r :: Type) | r -> x where
  Unwrap (Wrap a) = a