What's the intention behind Idris' `BorrowedType`?

Question

In idris, there's a universe called UniqueType the values of the types in which can only be used once. As far as I know, it can be used to write high-performance code. But the fact that a value can only be used once is usually too limited, so there's a way to borrow a value instead of consuming it:

data Borrowed : UniqueType -> BorrowedType where ...

The Borrowed data type is defined as above in Idris. Why doesn't it simply return Type but introduce another universe of types (BorrowedType)?

Answer 1

As the documentation explains, there are restriction on BorrowedType-typed Borrowed values:

Unlike a unique value, a borrowed value may be referred to as many times as desired. However, there is a restriction on how a borrowed value can be used. After all, much like a library book or your neighbour’s lawnmower, if a function borrows a value it is expected to return it in exactly the condition in which it was received!

The restriction is that when a Borrowed type is matched, any pattern variables under the Read which have a unique type may not be referred to at all on the right hand side (unless they are themselves lent to another function).

This restriction (and lend's leniency) is implemented by special typing rules in the typechecker. Those rules need something to apply to, which is why BorrowedType has to be a separate kind than regular Type (for which there aren't special lend/Read typing rules).