The limit of linear grades #274
Description
I'm curious where exactly QTT becomes insufficient
The most familiar example is
withArray : Int -> a -> (Array a [1] -> Ur b) [1] -> b
This sort of thing creates too tight a bottle neck that kills all grades
But since ownership can't avoid existentially quantifies identifiers to track provenance, maybe that suffices here?
The other concern is some withImmutable function that can take an immutable array, freeze it and duplicate it temporarily, then resume mutations when all reads are done.
Why exactly is the ownership/uniqueness stuff necessary?