To clarify what I'm aiming for with this patch, my view is that there
are three levels of coercions available inside the darcs source code, apart
from the repository coercions under discussion in this patch:
1. coerce : in line with normal Haskell, always safe to use
2. unsafeCoerceP, unsafeCoercePStart etc : no risk to memory safety,
but risk of patch/repo corruption (of course there are other kinds of
corruption you can still get even if you don't use these).
3. unsafeCoerce : risk to memory safety
The premise of my patch is twofold:
a. The exported repository coercion operations should be in category 2, i.e.
should be named unsafeCoerceXXX rather than coerceXXX, to make it clear they
do come with some proof obligation.
b. coerce shouldn't be available at all to clients of the Repository type,
as it gives the wrong impression of safety.
The downside which you point out is that it requires unsafeCoerce in the
actual implementation, as we have to turn off the ability to use coerce
everywhere (there was some discussion about tying it to the visibility
of the constructors here, but it didn't seem feasible:
https://mail.haskell.org/pipermail/glasgow-haskell-users/2013-
October/024360.html).
|