Inverse injective type families

Question

Lets say I have an injective type family T

type family T a = b | b -> a

My first question is there an way to write:

type family T' = the inverse of T

Without having to repeat all the instances of T but in reverse.

Such that: T (X1 a (T' a)) = a

It seems like this should work, as both T and T' are injective, given one side it is mechanical to work out the other.

Anyway to write T'?

Answer 1

With suitable extensions, one can write:

type T' b = forall a. T a ~ b => a

For example, here's an example showing that you get at least basic type compatibility with this type synonym:

type family T a = b | b -> a
type instance T Int = Bool

f :: T' Bool -> Int
f x = x