Как доказать, что параметры типа семейства инъективных типов эквивалентны?

Question

Если у меня есть семейство инъективных типов и доказательство эквивалентности типов, как я могу получить доказательство эквивалентности параметров?

Лучшее, что я смог придумать, использует , и это кажется мне оправданным, поскольку TypeFamily является инъективным, но... сама функция не проверяет , является ли TypeFamily инъективным, поэтому это может быть источником для ошибки. Я также могу ошибаться в том, что даже это не безопасное использование unsafeCoerce.

      type family MyTF a = b | b -> a
...

coerceTypeFamily :: (MyTF a :~: MyTF b) -> (a :~: b)
coerceTypeFamily Refl = unsafeCoerce Refl