[dwohnitmok]

I thought I'd read over `Data.Linear.Array` before, but maybe not? My intuition for linear types would be that for any function that uses the array you basically almost always want to return a pair of the value and new linear version of the array (i.e. `Res a (const (arr t))`). The only exceptions are a set of "terminal" operations that convert it to a non-linear type (in this case probably the things that end up returning an `IArray`).

So I'm a bit confused why e.g. `read` is `(1 _ : arr t) -> Int -> Maybe t` and not `(1 _ : arr t) -> Int -> Res (Maybe t) (const (arr t))`.

But also isn't the `newArray` fixed by just rewrapping the output?

  data Unrestricted : Type -> Type where
    MkUnrestricted : a -> Unrestricted a

  newArray : (size : Int) -> (1 _ : (1 _ : arr t) -> Unrestricted a) -> Unrestricted a

  -- You'll need this if you actually make use of the outer linear multiplicity
  -- in the function argument to newArray
  -- which is also why newArray returns Unrestricted
  useUnrestricted : (1 _ : Unrestricted a) -> (a -> b) -> b
  useUnrestricted (MkUnrestricted x) f = f x

This is e.g. how Linear Haskell does it. The unrestricted multiplicity of the argument to `MkUnrestricted` prevents the bug here by only allowing you to output non-linear things (so it rejects wrapping the linear input in `MkUnrestricted`; you have to first convert it via a terminal operation into something else).

The entire `Data.Linear.Array` seems to be in need of a once-over unless I'm misunderstanding something.

EDIT: Never mind, reading too quickly, I see the mread now that has the signature I'd imagine it should.