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

No. Injective type families are solely a type-inference mechanism. There are no proofs or other evidence. Figuring out how to get this right would be a significant research project, I'm afraid. Richard

On Apr 3, 2021, at 2:59 AM, Andreas Källberg wrote:

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)?_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.