Canonical way to support a temporily duplicatable Mutable vector

[Mansindam]

Here is the use-case:

1. linearly mutate a vector
2. freeze it so some functions can duplicate it and read it
3. when that terminates unfreeze it and continue linear operations

Is there a natural way of doing this? In particular it seems difficult to ensure functions using the duplicated frozen vector terminate before proceeding

[Mansindam]

This seems safe:

withVector :: (V.Vector a -> r) -> LV.Vector a %1 -> (r , LV.Vector a)
withVector f = Unsafe.Linear.toLinear \v -> (,v) $! f (L.unur (LV.freeze v))

I also suggest renaming Vector to Stack, it's a less overloaded and unambiguous

[Mansindam]

Shouldn't size ideally be 0-multiplicity on the vector?
Is that unsupported by ghc atm?

Edit: Probably nonsense, but typing Get at 0-multiplicity could be convenient, although unsafe if laziness allows keeping stale references around

[Mansindam]

Is it just not possible to use let to bind linear names? mklinearthing & \linear -> _ seems to be the only syntax that works

[Mansindam]

Some more experiments

In order to get a State containing linear vectors going It seems mandatory (?) to define lens with a passthrough

v          = LLens.lens \(IEnv p t i l f c) -> (p , \(r,x) -> (r , IEnv x t i l f c))
v'         = LLens.lens \(IEnv p t i l f c) -> (p , \x -> IEnv x t i l f c)

-- Now normal stateful lenses can be defined and can call Linear.Vector.size
l %%= f = state (LLens.over l f)
eg = (v %%= LV.size) >>= \(L.Ur sz) -> .. 

Am I missing anything?
If not, the L.Ur quickly becomes irritating; is there any (even theoretical) solution for managing product types at different linearities?
It seems crude to aggressively distribute the linearity eg. (a,b) %1 => both a and b must be %1