It's hard to write something that's generic over a uniqueness type and a normal type, which is indeed a bit of a pain. It's not completely impossible: we have a kind 'Type*' which covers both unique and normal types, which can be used to make some polymorphic functions which preserve uniqueness, but that's all at the minute.

On the other hand, I see them as something you use when you want more precise control over memory management, control of in-place update and so on.

As ever, there's a trade off between efficiency and abstraction, which is where the partial evaluator comes in. This is still experimental and we're working on it, but I'm wondering if we can use partial evaluation to turn nicely abstract high level code into something efficient based on uniqueness types at run time.

Thank you for both your answers.

I guess my main worry with this scheme would be fragmentation, having 3rd party libraries not bothering using Type* where it makes sense and making it very difficult to write code using uniqueness types. I guess I'll have to learn me some Idris and see for myself, the language looks very interesting.

That's correct. You can however have a function take a Type\star, meaning it accepts both Types and UniqueTypes. If such a function is passed a Type, that Type can only be used in the ways that UniqueTypes can be used ("any value of type Type* must also satisfy the requirement that it appears at most once on the right hand side"). The linked page provides an example of function composition defined using Type*:

(.) : {a, b, c : Type\star} -> (b -> c) -> (a -> b) -> a -> c

(.) f g x = f (g x)

Not being able to use UniqueTypes in place of regular Types could indeed cause some inconvenience, however I think to some degree it's unavoidable. Rust for instance doesn't let you pass a reference-counted or garbage-collected pointer to a function expecting a unique/borrowed pointer.

Note that \star should be an asterix character, but I'm not sure how to escape it properly here.