Without either GADTs or type families, two types `Foo` and `Bar` with mappings `fw :: Foo -&gt; Bar` and `bw :: Bar -&gt; Foo` that compose in both directions to the identity, are “effectively indistinguishable” from one another in a precise sense. If you have a definition `qux :: T Foo`, for any type function `T` not containing abstract type constructors, you can construct `justAsQuxxy :: T Bar` by applying `fw` and `bw` in the right places.<p>With either GADTs or type families, this nice property is lost.