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
RWShared
constraint, this should just beReadable