Allow uniqueness annotations for types

Motivation

1. From Linear types in Haskell:

   [...] in our system if one wants to indicate that a returned value is linear, we have to use a double-negation trick. That is, given f : A → (B ⊸ !r) ⊸ r, then B can be used a single time in the (single) continuation, and effectively f “returns” a single B. One can obviously declare a type for linear values Linear a = (a ⊸ !r) ⊸ r and chain Linear-returning functions with appropriate combinators.

   • This suggestion is easily "negated" e.g:

     f :: forall r . A → (B ⊸ !r) ⊸ r
     
     inval :: A
     
     id :: a -> a
     id x = x
     
     f  inval  id :: B

   • In consideration of the efforts made to confine their use in the implementation of lightweight concurrency, why would we then subject Haskell users to the joys of continuations (in all their g(l)ory) just to obtain linear types and values?

2. (Update: syntax has already been revised; see comments) The current syntax for linear functions is at best cumbersome: instead of ⊸, one uses #-> - if your linear functions are going to regularly use GHC's primitive types, this is what you can look forward to seeing:

   ugh :: Int# #-> Double# #-> ...

   ...or was that supposed to be:

   ugh :: Int# -> Double# #-> ...

   Oh what fun...

   But wait! We can just use that Linear type instead:

   ugh :: Linear Int# -> Linear Double# #-> ...

   ...oh, that's right: we now also have to drag in levity polymorphism to get this to work...for now - what's next?

Proposal

Since Haskell 1.3, strictness annotations have been available for use with type declarations:

data Complex a = !a :+ !a

Uniqueness annotations would have a similar appearance, using a small piece of Clean syntax:

newtype UUID = MkUUID *Integer

data Label a = MkLabel *a

Linear functions would then be just a specific use of uniqueness annotations (and a little syntactic sugar), with an implementation expanding the type a ⊸ b to *a -> b.

As for those examples:

1. The Linear type would be a mere type synonym: type Linear a = *a (if it's even needed at all...)

2. Being a simple annotation (rather than an intricate extension) for types, it can be used with all types directly.

Similar to those for strictness, uniqueness annotations would largely be administered by the Haskell implementation:

• The obvious difference being the implementation's reaction to discovering values of annotated types being reused: an obligatory error message.

• Another detail relates to the propagation of the annotation - we would like the following to be rejected:

  \i@(MkUUID _) -> (i, i+1)

  \l@(MkLabel x) -> (l, MkLabel x)

  and if possible:

  \(MkLabel x) -> repeat x

  But this should be accepted:

  \i -> (i+1, MkUUID i) :: Integer -> (Integer, UUID)

  i.e. propagation only occurs where annotated values are being used.