Generate inverse for injective type families?
Talking to @kosmikus about injective type families, he pointed out that in principle GHC could explicitly generate the inverse type family. That is, given these definitions:
type family F a = r | r -> a
type instance F Int = Char
GHC could generate these behind the scenes:
type family FInv r = a | a -> r
type instance FInv Char = Int
Now we can use the existing type family consistency checking to ensure that the inverse is well-defined, and lint that we have FInv (F T) ~ T
for each type instance F T
.
Is there a reason that the original implementation didn't take this approach? Are there some programs accepted by it that wouldn't be accepted under this design? It isn't immediately obvious to me whether we would want to expose the type family to the user, or merely define it internally.
By itself this doesn't get us much further. But if we were to add a coercion axiom that proves forall a . FInv (F a) ~ a
, then it would suffice for issues like #10833, and from a given F a ~ Char
it would become possible to conclude a ~ FInv (F a) ~ FInv Char ~ Int
.
The soundness of this axiom is not immediately obvious, much like the soundness of forall a b . F a ~ F b => a ~ b
is not obvious. On the other hand the fact that we have an explicit witness to the inverse and can verify the axiom holds for each concrete instance makes it seem relatively plausible.