[clean-list] uniqueness correction

[Wolfgang Jeltsch]

Hello,

another question concerning the paper "Uniqueness Typing for Functional 
Languages with Graph Rewriting Semantics".  Again, x (when used as an 
uniqueness attribute) stands for non-unique (\times) and * stands for unique 
(\bullet).

Definition 7.2 on page 16 defines the concept of the smallest non-unique 
supertype.  The paper comments:

    The last clause possibly introduces types like List x(Int *).  Contrasting
    Turner et al. (1995), we allow these types in our system.  This is
    harmless since these 'inconsistent' types have no proper inhabitants (for
    example, there is no Cons yielding type List x(Int *)).

But I would argue that these types get proper inhabitants by contraction as 
defined on page 18.  Consider the type statement

    y : [List x(a *)], z : [List x(a *)] |- (head y, head z) : (a *, a *).

By the contraction rule, it follows that

    x : List *(a *) |- (head x, head x) : (a *, a *)

but this is wrong in my opinion.

Is the paper in error or am I missing something?

Best wishes,
Wolfgang