The paper you cite seems like a best solution, well the only one I’ve seen, though I wonder if one could not be sufficient to introduce a pseudo-variance, which only testify to the fact that the type parameter does not occur in a mutable position in the type.
Update: Forgot about the talk about typed effects mentioned in About Multicore, which could also resolve the value restriction.