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

[Richard Eisenberg]

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 <anka.213 at gmail.com> 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.