I don’t know what @hgarrood meant when he said that Purescript’s type constructors are injective.
I mean, sure, injectivity means for any x and y: (f x = f y) → (x = y). Eg. This would mean that (Maybe x = Maybe y) → (x = y).
He told that type families invalidate this reasoning, why do they do so?
Why do you want type constructors to be injective?