CODEWITHSUNDEEP
haskelldependent-typetype-familiesinjective-function
Josh.F
Josh.F

Reputation: 3806

How to prove that the type parameters of an Injective Type Family are Equivalent?

If I have an injective type family, and a proof of type equivalence, how can I get a proof of equivalence of the parameters?

The best I've been able to come up with uses unsafeCoerce, and it seems justified to me since the TypeFamily is injective, but... the function itself doesn't check if the TypeFamily is injective, so, this could be a source for bugs. I could also be wrong, in that, not even this is a safe use of unsafeCoerce.

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

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

Upvotes: 3

Views: 43

Answers (0)

Related Questions