[darcs-devel] (un)safety of unsafeCompare

[Ben Franksen]

Hi Ganesh

I think I begin to understand why we see this differently.

My point of view is that an instance of class Eq2 /defines/ what
semantic equality means for that patch type. As long as the equality
thus defined is an equivalence relation, coercing the witnesses as done
by the default method implementations for =\/= and =/\= is correct by
definition. Indeed, if I write

  unsafeCompare _ _ = True

then I am stating that all patches are considered equal. Coercing
opposing witnesses is therefore completely justified and does not in any
way compromise the witness system!

Of course, if I make such a definition I'd better make sure that all the
other operations are consistent with that definition. That is, when I
apply such a patch I should get the same result for all patches etc. But
this is not different to defining instances of the good old Eq for
unwitnessed types: if == should mean semantic equality then you better
make sure that any function f respects equality in the sense that x == y
==> f x == f y.

In contrast, calling unsafeCoerce really is /undefined/ in the same
sense that calling 'apply (unsafeCoerceP x)' is undefined, in general,
unless you can prove that your contexts are actually equivalent. I could
think of patch types that contain a runtime representation of the start
and end states and IMO it would be fully justified to call error

Cheers
Ben

Am 05.07.19 um 17:58 schrieb Ganesh Sittampalam:
> On 30/06/2019 01:07, Ben Franksen wrote:
>> The haddocks for class Eq2 say the following about unsafeCompare:
>>
>>> It is unsafe to define a class instance via this method, because if
>>> it returns True then the default implementations of '=\/=' and '=/\='
>>> will coerce the equality of two witnesses.
> 
> I think here that "unsafe" means "you have a proof obligation". For
> example if I wrote
> 
>   unsafeCompare _ _ = True
> 
> then a caller could use =\/= to equate two unequal contexts.
> 
> Conversely defining the class with =\/= and not using unsafeCoerce in
> the implementation, can't introduce any extra unsafety. Clearly such an
> implementation would ultimately need to delegate to something that is
> "unsafe" (in the above sense).
> 
>>> Calling this method is safe, although '=\/=' or '=/\=' would be
>>> better choices as it is not usually meaningul to compare two patches
>>> that don't share either a starting or an ending context
>> I think this statement gets it wrong. In fact the opposite is true.
>>
>> It is unsafe to /use/ unsafeCompare because this may mean that we
>> identify two patches that may only accidentally have the same structure,
>> but are otherwise completely unrelated. Here is a simple example:
>>
>>   A=hunk f [x] [y]; B=move f g; C=add f; D=hunk f [x] [y]
>>
>> For these patches,
>>
>>   unsafeCompare A D = True
>>
>> even though A and D are decidedly /not/ the same patch!
> 
> That's true, but we also don't get any equality coercion we can then misuse.
> 
> So I think the existing comment is correct in the narrow sense that
> defining unsafeCompare imposes a proof obligation that the patches
> genuinely are equal. That means that when called with equal starting
> contexts, it's safe to coerce the ending contexts. Complying with that
> (informal) proof obligation in turn means that the safety of the witness
> system is preserved.
> 
> Calling unsafeCompare is probably never/almost never actually the right
> thing to do, but it doesn't in itself compromise the witness system.
> 
> I guess this particular comment could be improved to give more details
> of that. In general the meaning of "unsafe" in the codebase is probably
> not clearly nailed down and some general documentation of that might be
> helpful.
> Cheers,
> 
> Ganesh
>