tl;dr (hopefully)

While writing the question below, I think I've come up with a simpler way to ask it.

Assume this senario:

• you've never seen Maybe in Haskell before, so you don't know it's generative,
• you're given two entities of kind Type -> Types,
  • one called Maybe
  • and one called Optional,
• and you are told they are two synonyms to all intent and purposes, but that one of them is generative and the other is not.

How would you tell which one is which?

Is the only way to tell them apart to pass them unsaturated to a function f accepting Type -> Type and see which one compiles? (Or any other trick leveraging the fact that an unsaturated type family can't be passed around.)

E.g. if f @Maybe (resp. f @Optional) compiles and f @Optional (resp. f @Maybe) doesn't then Maybe (resp. Optional) is generative and Optional (Maybe) is not?

If the answer to the above is "No, that's not the only way", then probably I've that's a XY problem, and reading the following might fix it.

Full fledged question

I’m reading Higher-order Type-level Programming in Haskell, and I have some doubts about the definition of generativity. I feel there's a link to this existing question, but I haven't solved my doubts reading that.

At page 3 of the paper, the definitions are:

Definition (injectivity). f is injective ⇔ f a ~ f b ⇒ a ~ b.

Definition (generativity). f and g are generative ⇔ f a ~ g b ⇒ f ~ g.

Definition (matchability). f is matchable ⇔ f is both injective and generative.

While the definition of injectivity (which comes with an implied ∀ a, b, doesn't it?) seems natural to me from calculus, and the definition of matchability seems natural to because it's just the logical conjunction of the other two, what leaves me puzzled is this:

• generativity is in fact defined as a binary property,
• yet, it's used in the definiton of matchability as is if it was unary.

In other words, if according to the definition of genarativity I need to talk about two Type -> Types¹ f and g in order te tell whether they are both generative, how can I say talk about generativity of just f in defining matchability?

Furthermore, that a vs b in the definition of generativity also puzzles me, but even precisely formulating my confusion is made harder by the fact that generativity is given as a property of two Type -> Types.

Anyway, let me try explain, by making two examples.

• Say I want to check whether Maybe and [] are generative (and we know they are, aren't they?). How does the definition help me? If I set f = Maybe and g = [], I know f ~ g doesn't hold to start with, so by implication I know f a ~ g b, which is Maybe a ~ [b] must be false for whichever a and b I choose. So I don't have a single pair of a and b for which the left-to-right implication holds, so I can't really be satisfied with it. I mean, the implicatio holds just because the left-hand side is always false.

• Say I want to check whether Maybe and F, being F a type family mapping any a to Maybea are generative. What does this even mean? I know that Maybe is and F isn't, so how is the definition helping me? Plus, if f = Maybe and g = F, obviusly f a ~ g b, which is Maybe a ~ F b, i.e. Maybe a ~ Maybe b will be false whenever a ~ b is false.

Again, I have a hard time understanding this definition of generativity, even though intuitively I think I would be able to tell, given a list of Type -> Types, which one is generative and which one is not.

¹ I'm using Type -> Type as a word because there's both type constructors and type families.