3

If I have an injective type family, and a proof of type equivalence, how can I get a proof of equivalence of the parameters?

The best I've been able to come up with uses unsafeCoerce, and it seems justified to me since the TypeFamily is injective, but... the function itself doesn't check if the TypeFamily is injective, so, this could be a source for bugs. I could also be wrong, in that, not even this is a safe use of unsafeCoerce.

type family MyTF a = b | b -> a
...

coerceTypeFamily :: (MyTF a :~: MyTF b) -> (a :~: b)
coerceTypeFamily Refl = unsafeCoerce Refl
Josh.F
  • 3,666
  • 2
  • 27
  • 37
  • 2
    Odd. My gut reaction is that `coerceTypeFamily Refl = Refl` should Just Work. The [original paper](http://ics.p.lodz.pl/~stolarek/_media/pl:research:stolarek_peyton-jones_eisenberg_injectivity_extended.pdf) superficially appears to agree: "Given the wanted constraint F σ ∼ F τ , add the derived wanted constraint σn ∼ τn for each n-injective argument of F.". It also includes the example `fid :: F a ~ F b => a -> b; fid x = x` (their `F` is your `MyTF`) and says, "Should that type-check? Absolutely.". Yet it does not type-check in GHC. Perhaps this is a bug...? – Daniel Wagner Oct 26 '21 at 06:00
  • 1
    IIRC, this was discussed in the past, and the result was that this should work, but does not in current GHC. GHC devs won't turn this on until someone proves that doing so keeps the system type safe. Or at least this was what I read on some forum or SO (again, IIRC). I now found the issue: https://gitlab.haskell.org/ghc/ghc/-/issues/10833 – chi Oct 26 '21 at 12:55
  • Since I found a very close duplicate, I closed this question. If you feel that your question is more nuanced, feel free to argue your case and I'll vote to reopen. :-) – chi Oct 26 '21 at 13:07
  • Thanks for the link, The GHC issue seems to coroborate that `unsafeCoerce Refl` is the solution for now. – Josh.F Oct 26 '21 at 14:51

0 Answers0