An expression with this type has no aliases. In other words, no other expression, evaluated at the same program point, would evaluate to the exact same object value.

A constructor's return type should be annotated with @Unique if the constructor does not leak references to the constructed object. For example, the String() constructor return type is annotated as @Unique.