[darcs-users] darcs patch: partial type witnesses in Unrevert (and 44 more)

[David Roundy]

On Wed, Aug 27, 2008 at 01:14:56PM -0700, Jason Dagit wrote:
> On Wed, Aug 27, 2008 at 12:06 PM, David Roundy <droundy at darcs.net> wrote:
> > On Wed, Aug 27, 2008 at 09:56:32AM -0700, Jason Dagit wrote:
> >> [updates to Repository.Internal to fix conflicts and support type witness refactor in commands
> >> Jason Dagit <dagit at codersbase.com>**20080827165327] hunk ./src/Darcs/Repository/Internal.lhs 336
> >>  get_unrecorded :: RepoPatch p => Repository p C(r u t) -> IO (FL Prim C(r u))
> >>  get_unrecorded = get_unrecorded_private id
> >>
> >> +-- | The /unrecorded/ includes the pending and the working directory changes.
> >>  get_unrecorded_private :: RepoPatch p => ([DarcsFlag]->[DarcsFlag]) -> Repository p C(r u t) -> IO (FL Prim C(r y))
> >>  get_unrecorded_private _ (Repo _ opts _ _)
> >>      | NoUpdateWorking `elem` opts = return $ unsafeCoerceP NilFL
> >> hunk ./src/Darcs/Repository/Internal.lhs 573
> >>         decideHashedOrNormal rf $ HvsO {hashed = HashedRepo.apply_to_tentative_pristine c opts p,
> >>                                         old = DarcsRepo.add_to_tentative_pristine p}
> >
> > It looks pretty clear to me that tentativelyAddToPending is still used
> > in a buggy manner.  It's only used three times, but two of those make
> > differents assumptions (the third is in Get, where we know there are
> > initially no local changes), so fixing a bug in Unrevert will be
> > guaranteed to create a bug in Unrecord (but in the command
> > obliterate).
> 
> Well, the way I started thinking about tentativelyAddToPending is that
> the pending has context C(r w), where w is the working copy context
> (and thus the unrecorded changes are (pend +>+ working) :: C(r u).  We
> don't track the working copy context.  That's why I changed it to x in
> the type sig of tentatvelyAddToPending.  Even if we add tr and tu to
> the repository state below we're not tracking the working copy
> context.  Furthermore, as I understand it, even if we do track the
> working copy context we'd still have the burden of proving that
> sometimes w = r in some of the commands.

In none of the cases where tentatvelyAddToPending is used, does the
'w' context you mention show up in the arguments to
tentatvelyAddToPending, so this issue is a red herring.  We don't need
to track this state, because it is never used outside
Darcs.Repository.Internal (and friends).

> >> -tentativelyAddToPending :: forall p C(r u t y). RepoPatch p
> >> -                        => Repository p C(r u t) -> [DarcsFlag] -> FL Prim C(u y) -> IO ()
> >> +-- | This fuction is unsafe because it accepts a patch that works on the tentative
> >> +-- pending and we don't currently track the state of the tentative pending.
> >> +tentativelyAddToPending :: forall p C(r u t x y). RepoPatch p
> >> +                        => Repository p C(r u t) -> [DarcsFlag] -> FL Prim C(x y) -> IO ()
> >>  tentativelyAddToPending (Repo _ opts _ _) _ _
> >>      | NoUpdateWorking `elem` opts = return ()
> >>      | DryRun `elem` opts = bug "tentativelyAddToPending called when --dry-run is specified"
> >> hunk ./src/Darcs/Repository/Internal.lhs 585
> >>        let pn = pendingName rt
> >>            tpn = pn ++ ".tentative"
> >>        Sealed pend <- readPrims `liftM` (gzReadFilePS tpn `catchall` (return nilPS))
> >> -      FlippedSeal newpend_ <- return $ newpend (unsafeCoerceP pend :: FL Prim C(r t)) patch
> >> +      FlippedSeal newpend_ <- return $ newpend (unsafeCoerceP pend :: FL Prim C(a x)) patch
> >>        writePatch tpn $ fromPrims_ newpend_
> >>        where newpend :: FL Prim C(a b) -> FL Prim C(b c) -> FlippedSeal (FL Prim) C(c)
> >>              newpend NilFL patch_ = flipSeal patch_
> >
> > ..
> >
> >>  tentativelyRemovePatches :: RepoPatch p => Repository p C(r u t) -> [DarcsFlag]
> >> -                         -> FL (Named p) C(x t) -> IO ()
> >> +                         -> FL (Named p) C(x r) -> IO ()
> >>  tentativelyRemovePatches = tentativelyRemovePatches_ UpdatePristine
> >
> > The former definition is correct.  A quick look at
> > tentativelyRemovePatches_ shows that it is in fact the tentative
> > inventory that is being modified, which requires that the patches be
> > in the context of the tentative state.
> >
> > But it's a bit vague since with our current type witnesses 't' is
> > always guaranteed to be the same as 'r', and there is no correct
> > answer.  Certainly with the type you've given this function, if it's
> > called twice it will corrupt the repository.  (It isn't called twice,
> > but the type system can't check this, and there are reasonable reasons
> > to call it twice, or to use some other repository-modifying command
> > afterwards.)
> 
> As you said in a different email, we don't have a way to track state
> mutation with the type witnesses.  As you said here, we don't separate
> tentative recorded (tr) from tentative unrecorded (tu).  Which, as I
> tried to point out in a different email (off list) which you said you
> didn't read in detail, would be required to solve this ambiguity.  As
> such, I've pretty much stopped using the 't' type and I was tempted to
> just remove it for now but have trouble justifying that work when I
> could probably replace it with tr and tu for a similar amount of
> effort.  Then once I'm done adding tr and tu I'd run head first into
> the problem of tracking the mutations of state.

The "tentative" state is always the tentative recorded state.  There
is not yet such a thing as a "tentative unrecorded" state.  We just
directly modify the unrecorded state after finalizing the tentative
changes.  We could add such a concept, but it isn't in the code
currently.  I do believe that three states is the correct number.  The
key is that repository correctness isn't affected by the unrecorded
state, so we don't need to (and cannot, if we wanted to) modify it
atomically.

> We've rolled around ideas about tracking those mutations, but it seems
> that doing it in a safe way requires formalizing something like Monad
> but with either incompatible kinds or types (I forget which was the
> bigger problem).  Either way, it seems as though this would require a
> new type or class similar to Monad (let's call it Monadish for this
> discussion).  Once we have that defined I imagine us lifting IO into
> that new monadish.  Now the inelegance of this solution rears it's
> ugly head.  We make very heavy use of the do-notation and we'd have to
> revert all our monad code to use the monad primitives.

Yes, we should do this.  We use hardly any do notation in actual
repository-modifying code, so it shouldn't be hard.

> We *might* be able to make heavy use of GHC specific hacks to take
> over the do-notation but I'm not sure.  And as I understand it you
> can't use both means of do-notation in the same module.  This has the
> implication that we'd need to make new Monadish instances for the
> places that we use do-notation currently, such as Maybe and Either.
>
> >> hunk ./src/Darcs/Repository/Internal.lhs 632
> >>        remove_from_unrevert_context repository ps
> >>        debugMessage "Removing changes from tentative inventory..."
> >>        if format_has HashedInventory rf
> >> -        then do HashedRepo.remove_from_tentative_inventory repository opts ps
> >> +        -- I believe this call to HashedRepo.remove_from_tentative_inventory is safe
> >> +        -- Because the above call to remove_from_unrevert_context ensures that
> >> +        -- none of the patches in pending depend on ps.
> >> +        then do HashedRepo.remove_from_tentative_inventory repository opts (unsafeCoerceP ps :: FL (Named p) C(x t))
> >>                  when (up == UpdatePristine) $
> >>                       HashedRepo.apply_to_tentative_pristine c opts $
> >>                       progressFL "Applying inverse to pristine" $ invert ps
> >
> > The comment here is completely wrong.  The call to
> > remove_from_unrevert_context has no effect on pending, and no effect
> > on the repository itself.  Fortunately, fixing the bug in the type of
> > this function removes the need for the unsafeCoerceP.
> 
> Ah right, I forgot to revise that comment after realizing that Pending
> != Tentative.
> 
> Changing the type to t would still be the wrong thing though.  As t is
> not a well-defined context.  The reason I made it r is because we
> don't have tr.  Also, tr would be equal to r until we do our first
> tentative operation, which is probably quite problematic to explain to
> the type checker also.

t is what tr is, so this isn't so bad.

> >> hunk ./src/Darcs/Repository/Internal.lhs 642
> >> -tentativelyReplacePatches :: forall p C(r u t). RepoPatch p => Repository p C(r u t) -> [DarcsFlag]
> >> -                          -> FL (Named p) C(r t) -> IO ()
> >> -tentativelyReplacePatches repository opts ps =
> >> +tentativelyReplacePatches :: forall p C(r u t x). RepoPatch p => Repository p C(r u t) -> [DarcsFlag]
> >> +                          -> FL (Named p) C(x r) -> IO ()
> >> +tentativelyReplacePatches repository@(Repo x y z w) opts ps =
> >> +    -- tentativelyRemovePatches_ leaves the repository in state C(x u t)
> >>      do tentativelyRemovePatches_ DontUpdatePristine repository opts ps
> >
> > Again, this is vague, given that t and r are identical, but the
> > correct answer is clearly t (because this calls
> > tentativelyRemovePatches_).
> 
> If we were tracking tr an tu, the first step would result:
> C(r u tr tu) -> C(r u x tu)
> 
> So, I disagree.  Again, I took the liberty of ignoring t and using r
> (for the reasons above).

Sorry.  Whether we track it or not, 't' is a real and distinct state
that exists in the repository and in the code, and it's wrong to call
it anything else.

...

> > I'm pushing a change fixing these type witnesses... I guess it's
> > basically just a revert of most of this patch, but it involved a
> > careful review.
> 
> Okay, but I wish you hadn't :(  If we're going to stop ignoring t and
> really fix it we need to add tr and tu.  Of course, that change
> doesn't solve the problem that you want to solve.  Adding those types
> without the mutation tracking means the burden of proof is still on
> the programmer.
> 
> I hope you can appreciate that from my point of view your reverts are
> equally wrong to my changes.  But, at least with my changes I was able
> to add documentation at the call sites which tried to explain or give
> a proof as to why the type witnesses didn't match the usage.  In my
> opinion, without the state tracking, the context of Repository is just
> machine checkable documentation.  meaning, it's not a proof, but a
> guide and way to understand the code.

Sorry that I didn't notice the comments in the middle before writing
my last email.  I see now that you did define tr and tu.

David