new floating and dependent types

[np]

This is a potential issue regarding the theory.

Typically the channel allocations/restriction, aka new in Ling, is allowed to commute upward (of course renaming channels to avoid conflicts).

Consider the following program:

recv c (i : Int)
new (v : ? Vec A i, v')
( .... | .... )

Here the new cannot float upward because of the type dependency.

At least this might force the types to be kept around in the compiler phases involving these floating rules.