Lets say I have an injective type family <code>T</code> <pre class="prettyprint"><code>type family T a = b | b -> a </code></pre> My first question is there an way to write: <pre class="prettyprint"><code>type family T' = the inverse of T </code></pre> Without having to repeat all the instances of <code>T</code> but in reverse. Such that: <code>T (X1 a (T' a)) = a</code> It seems like this should work, as both <code>T</code> and <code>T'</code> are injective, given one side it is mechanical to work out the other. Anyway to write <code>T'</code>?

Inverse injective type families

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'?

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