[Haskell-cafe] Get proof of injectivity for an injective type family

[Andreas Källberg]

Is there any way to get hold of a proof of injectivity for an injective type family?
In other words, given this type family

    type family F a = b | b -> a

can I get the term

    fInj :: F a ~ F b => (a ~ b => r) -> r

in any way (without using unsafeCoerce)?
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 1394 bytes
Desc: not available
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210403/1e5af971/attachment.bin>