ReadResult should be less constrained
The current type is:
:: ReadResult p r w = E.sds: ReadResult !r !(sds p r w) & RWShared sds & TC r & TC w | E.sds: AsyncRead !(sds p r w) & RWShared sds & TC r & TC w
Why is the share present in
ReadResult, the reading is done anyway.
Why is there a
RWSharedconstraint, this should just be