Is anything generative?

In the paper "Higher-order Type-level Programming in Haskell", an f :: Type -> Type is defined to be "generative" in the following way:

Definition (Generativity). f is generative ⇔ f a ~ g b ⇒ f ~ g

I'm going to explicitly write out the intended quantification as I understand it:

type IsGenerative :: (Type -> Type) -> Constraint
class (forall g a b. f a ~ g b => f ~ g) => IsGenerative f

Conversely, in words:

F :: Type -> Type is generative if there is no G :: Type -> Type besides F such that there exist A, B :: Type for which F A ~ G B

The paper goes on to make a statement about the generativity of unsaturated type-families (they're not generative). To my understanding, in order to be able to form the proposition of whether or not unsaturated type-families are generative, the variables f, g :: Type -> Type should range over type-families as well as type constructors. Note that this means the ~ in f ~ g must represent some more abstract sense of definitional equality than GHC's (~) :: (Type -> Type) -> (Type -> Type) -> Constraint, which cannot be applied to unsaturated type families.

Now here's the problem: it doesn't seem like anything is generative. You'd expect that a datatype constructor like Maybe :: Type -> Type would be generative, but I can easily construct a distinct type family G :: Type -> Type and A, B :: Type for which F A ~ G B (despite F /~ G).

type G :: Type -> Type
type family G a
  where
  G _ = Maybe Int

data Dict c
  where
  Dict :: c => Dict c

lhs :: Dict (Maybe Int ~ G String)
lhs = Dict

As I said before, we can't actually form the proposition Maybe ~ G within GHC (because G is not saturated), but if F ~ G is taken to mean "F is definitionally equal to G", it's pretty obvious that Maybe /~ G. So it seems like Maybe is not actually generative in the sense defined in the paper. And it seems to me that any data/newtype is susceptible to a similar sequence of reasoning.

So where am I going wrong?

Is my assumption that F, G are allowed to range over type-families as well as type constructors justified? If not, generativity seems like a rather trivial property: "we cannot form the proposition of whether type families are generative, so type families are not generative".

Am I misunderstanding how the variables are quantified in the statement of generativity?

Are there actually any type-level expressions f :: Type -> Type that satisfy the formal property of being generative?