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

Richard Eisenberg rae at richarde.dev
Tue Apr 6 02:30:43 UTC 2021

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.


> 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.

More information about the Haskell-Cafe mailing list