What is Idris's “Borrowed”?

Question

In idris, there is a universe called UniqueTypetype values ​​that 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 is a way to borrow a value instead of using it:

data Borrowed : UniqueType -> BorrowedType where ...

The data type is Borroweddefined as indicated above in Idris. Why doesn't it just return Type, but introduce another type universe ( BorrowedType)?

Answer 1

As explained in the documentation , there are restrictions on the BorrowedType-typed values Borrowed:

, . . , , , , , , !

, Borrowed Read, , ( ).

( lend ) typechecker. - , BorrowedType , Type ( lend/Read).