Linear Types in Silver

[remexre]

Random dump after 2 drinks, so don't spend too much time thinking about this, I just don't wanna lose it:

• It'd be nice to have linear types to prevent IO token screwups
• It'd be nice to have linear types in collection attributes, to have vector-valued attributes
  • This'd involve a change such that linear_collection attribute foo with mutableVectorAppend, withMutableVector; would be allowed, where:
    • MutableVector : Type -> Type
    • Vector : Type -> Type
    • withMutableVector : (MutableVector a -o MutableVector a) -> Vector a
    • mutableVectorAppend : (MutableVector a, Vector a) -o MutableVector a (uncurried b/c too lazy to figure out which arrow(s) need to be -os)
• It'd be easier to do linear-types-for-silvir (where violations are UB but not necessarily detected at compile-time) for the latter usecase
• the former case could maybe work if we put linearity in the flowtypes? we'd want mandatory flowtypechecking (flow-typechecking? flowtype checking? flow(typechecking)?) then?