[Haskell-cafe] Get proof of injectivity for an injective type family
anka.213 at gmail.com
Sat Apr 3 06:59:15 UTC 2021
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...
Size: 1394 bytes
Desc: not available
More information about the Haskell-Cafe