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

[Apologies for the duplicate!] On 06/04/2021 03:30, Richard Eisenberg wrote:

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.

This is quite true, but...

...

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)?

...while injective type families don't themselves carry evidence, it is sometimes helpful to encode it by writing the inverse family explicitly and adding constraints that require it to be an inverse: type family FInv b = a | a -> b type Good a = FInv (F a) ~ a fInj :: (F a ~ F b, Good a, Good b) => (a ~ b => r) -> r fInj x = x Of course this may not be enough, because the extra constraints may get in the way. Hope this helps, Adam -- Adam Gundry, Haskell Consultant Well-Typed LLP, https://www.well-typed.com/ Registered in England & Wales, OC335890 118 Wymering Mansions, Wymering Road, London W9 2NF, England