Re: My current work on darcs...

On 09/14/2017 10:28 AM, Ben Franksen wrote:
> Like I said last time, whether we operate on the tentative or the "real"
> recorded state should not be visible outside the Repository layer. Thus,
> we should not distinguish between them in the witnesses for the
> Repository type. Instead, we should add a witness for the pending state.
> (The repo type parameter should be kept as long as we mix rebase and
> normal patches.) This gives us
> 
>   Repository rt p wR wP wU
> 
> which should be understood to mean that when we read the complete repo
> we get
> 
>   (recorded :> pending :> working)
>   :: PatchSet rt p Origin wR :> Pending p wR wP :> Working p wP wU

I have been playing on and off with this idea. One problem I encountered
regularly is that when we have a function that returns a patch or a
patch list in such a way that we know that the starting and ending
states do not change, then it should be possible to avoid sealing:

  do_some_internal_commutation :: (FL p) wX wY -> (FL p) wX wY

But that fails to compile for the trivial case:

    do_some_internal_commutation NilFL = NilFL

with an error could not deduce wX ~ wY