[clean-list] Serious bug in the type system

[Edsko de Vries]

> There are no arrays with unboxed values in this example. {#Char} is an array
> of unboxed evaluated characters. {Char} is an array of boxed, possibly
> unevaluated characters.

Sorry, yes, I misread.

> An example of a unique array with (only) unboxed values for which typing
> as an observer may be correct is:
> 
> copy2 :: !*{#Int} -> (!*{#Int},!*{#Int})
> copy2 a1
>     #! a2=copy a1
>     = (a2,a1)
> 
> copy :: {#Int} -> *{#Int}
> copy a = {e\\e<-:a}
> 
> The Clean 2.2 compiler allows this because of the bug. After fixing the bug
> it is rejected. This is not necessary, because the result of copy must be a
> newly created array, because no unique array is passed to function copy.

But it's not enough to check if the result is a unique array with
unboxed values, is it? The only reason that copy2 should be allowed is
that the result of 'copy' is a *new* array; but that cannot really be
expressed through uniqueness typing (we need something like Odersky's
observer type system?). There is no way in a uniqueness type system to
make the distinction between the result of 'copy' and the result of 'id'
(unless perhaps you want to use the fact that the domain of copy is
non-unique and the result is unique?).

Edsko