I won't screen this immediately. Essentially the problem it's
trying to address is that the Repository type parameters can all
be manipulated with plain "coerce", which is generally seen as safe.

Concrete patch types in theory have the same problem, but in practice
most patch code is polymorphic on the patch type so the witnesses
can't be coerced. I may take a look at doing the same for patches
at some point; it might also be nice to use the new kind system
features in GHC to properly classify the witnesses in general.

I don't feel too strongly about this if there are significant
downsides I've missed.

1 patch for repository darcs-unstable@darcs.net:screened:

patch f0fc5379f75d02cb2ac15e75ce64293bdb0ed153
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Sun Nov 18 22:01:43 GMT 2018
  * make it clear that coercing Repository is "unsafe"
  
  This may be a little pedantic, especially as we don't claim that
  mkRepo is unsafe, but it's consistent with the API for patches.

Attachments

• make-it-clear-that-coercing-repository-is-_unsafe_.dpatch
• patch-preview.txt
• unnamed

Well, the obvious disadvantage is that unsafeCoerce is unsafe while coerce is 
safe.

With every use of unsafeCoerce comes a proof obligation that the types you 
cast between have the same run-time representation, otherwise you risk memory 
corruption. Using coerce you can rely on GHC to check that for you. I feel 
much more comfortable using coerce.

You want to disallow coerce to cast witnesses because it doesn't have 
"unsafe" in its name. Indeed, casting Repository witnesses is not "safe" in 
the sense that it allows to apply patches in the wrong context. However, this 
is unsafety at a whole other level than what can happen if you make a mistake 
using unsafeCoerce. This is why I think it is better to avoid unsafeCoerce 
where possible and instead rely on convention and common sense when it comes 
to casting Repository witnesses i.e. use only the coercion functions exported 
by D.R.InternalTypes, just as we do not use unsafeCoerce when casting 
witnesses for patches but only use the restricted versions exported from 
D.P.Witnesses.Unsafe.

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

I am not convinced the gain (making it impossible to use coerce for
witness casts) is worth the cost. Your patch is okay for demonstrating
the idea, but to do this right means adding role annotations to every
data type that takes witness type parameters. This is a considerable
complication. It also means potential contributors have to learn about
roles.

My suggestion is: go ahead and start to make this change consistently
throughout all of Darcs. When you are done with that and are still
convinced this is the right way to go, I may re-consider.

The role annotations would only be needed on the low-level
representation types (primitive patches and maybe repo patches)
- for anything that wraps them, the right role would be
inferred automatically.

As I mention in my original message, it's less important
in practice for them because most code that works on patches
is polymorphic in the patch type, but agreed it should be
done in theory to be consistent.

The advantage of my patch even in isolation is that it
brings coercions for Repository witnesses in line with
coercions for the witnesses on patches.

After reading up on type roles and letting that sink for a while I 
take back my reservations. This is indeed a standard use case for 
assigning a stricter role than that which is inferred by the compiler, 
i.e. to maintain a data type's invariants.

I've pushed to screened now, thanks.

We already discussed it in detail. One point I like is that we are now 
forced to say which witnesses we coerce (see the change to 
Darcs.Repository.Job) which clarifies the code. Also unsafeCoerceXXX 
stands out more and this increases the motivation to remove as many of 
them as possible.