Hey, Just to continue the academic nitpicking.. :-)
Linear logic/typing does not quite capture uniqueness types since a term with a unique type can always be copied to become non-unique, but a linear type cannot become unrestricted.
Actually, that isn't quite accurate. In linear logic, a term with a non-linear type can always be regarded as having a linear type, i.e. U -o !U is a theorem (my favourite reading of this theorem is "if you have an unlimited supply of bank notes, then you also have a single one"). The implication in the opposite direction is a falsity (from the fact that we have a single bank note, we cannot decude that we have an unlimited supply). By contrast, in uniqueness typing we certainly don't want to allow treat a term with a non-unique type as having a unique type, but we *may* want to allow to treat a term with a unique type as having a non-unique type (as you mention). However, you have to be very careful when you do that: if you allow to treat functions with a unique type as having a non-unique type, you loose all uniqueness guarantees unless you indicate in the type of the term whether or not the function has any unique elements in its closure. If you don't, you could for example construct a term that duplicates unique elements using dup x = (\f -> (f _|_, f _|_)) (\y -> x) (which would get type "forall a, unique a to pair of unique a's" if you allow to copy unique functions and then apply them). Edsko