Linear Mutable Arrays with Linear Values via Ownership

Is your feature request related to a problem? Please describe.

We can't have linear values inside Data.Array.Mutable.Linear because then we can't freeze. Namely,

freeze :: Array (Array Int) %1-> Ur (Vector (Array Int))

would be unsafe because the inner arrays can now be read and duplicated, though they are mutable references which need to be single-threaded.

Describe the solution you'd like

We can get around this with some notion of an ownership witness that allows you to freeze because using the inner values requires the witness. This is incorrect but gets at the rough idea:

data Arr :: Own -> Type -> Type where ...

deepFreeze :: Arr o (Arr o' Int) -> Owned o %1-> Ur (Vector (Arr o' Int), Owned o')

use :: Owned o %1-> (Owned o %1-> Ur b) %1-> Ur b
write :: Arr o a -> Int -> a %1-> Owned o %1 -> (Arr o' a, Owned o')

This ^ will require some careful thought to tease out.