[clean-list] instantiation of attributed type variables

[Sjaak Smetsers]

Hello Wolfgang,

Indeed, the same type variables have the same attributes, not only in type
declarations but also in function types. In this way typing is preserved
under substitution. If we would allow a unique variable to be coerced to a
non-unique one the substitution of a unique function type for such a
variable would no longer be valid.

A substitution of a type for variable in only allowed if these types have
the same top attribute. This requirement is also present in the type system
of "Uniqueness Typing for Functional Programming with Graph Rewriting
Semantics", e.g. in the second rule of def 8.3, page 603.

Now back to your original question, which starts with the declaration

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

First of all, this type does not lead to any propagation inequalities, since
the variable a is not on a propagating position. In fact, variables only
occurring 'below' an arrow type are not propagating.

The application you described and Arjen tried in Clean seems to hit on a bug
in the uniqueness typing system. What I expected, is the following:

The type constructor T appears on a negative position (i.e. the first
argument of an arrow type) inside its own definition. This means that the
coercion behavior of a T-type is contra-variant:  u:(T ..) <= v:(T ..) if v
<= u. But when you try it in Clean the results are different, even worse, I
think they are wrong. I've briefly looked at the implementation of the
uniqueness type checker, but was not yet able to see what's going on.
As soon as I've some more time I'll try to fix the problem.

Regards,

Sjaak Smetsers