stefan-hoeck / idris2-array Goto Github PK

When I use my array, I have a loop get -> IO -> set (with some Either thrown in for good measure, though I don't think it's important here). I then extract one of the values in my MArray n a as the value of interest. Given the loop has to return MArray n a linearly, but in IO, I've used L1 IO, which I can reduce to IO. Thus, my function looks like

f : MArray n a -@ IO (!* a)

Now I can't for the life of me work out how to get this to work with

alloc : (n : Nat) -> a -> (1 fun : MArray n a -@ Ur b) -> Ur b

Is it even possible?