[clean-list] uniqueness attributes of data constructors

[Wolfgang Jeltsch]

Hello,

in the following mail I use the notation ^*, ^x and ^u/^v for uniqueness 
attributes "unique", "non-unique" and "variable".

I declare a type T via this declaration:

	:: T a = C (T a -> a)

The type of C is (T^u a^v -> a^v) -> T^u a^v.  This can be specialized to the 
following types:

	1. (T^* a^v -> a^v) -> T^* a^v

	2. (T^x a^v -> a^v) -> T^x a^v

Further, I have a function f with type T^* a^v -> a^v.

Now, I apply C to f which results in a value of type T^* a^v according to the 
first of the above specializations.  I duplicate the reference to the funtion 
application C f which results in the function application having type
T^x a^v.  Now, I use pattern matching to extract f.  The extracted function 
has type T^x a^v -> a^v according to the second of the above specializations. 

But T^* a^v -> a^v is not a subtype of T^x a^v -> a^v.  In fact, it's the 
other way round.  I could apply the extracted function f to a value of 
non-unique type which shouldn't be possible according to f's original type.

Since I cannot imagine that there is a notable flaw in the uniqueness type 
system, I wonder where my mistake is.  Can somebody explain this to me?

Best regards,
Wolfgang