Opening a file in write mode may cause a visible side-effect

[asajeffrey]

Currently, opening a file for writing causes it to be opened immediately, not on commit. This may cause a visible side-effect, e.g. creating or clearing an existing file. Perhaps the semantics should enforce that files are always opened as tmp files, and are copied to their destination when closed? We could save the filename in a ref to be opened on a later commit, but this would mean that Agda handles aren't Haskell handles, which complicates the FFI layer.