Make unrestricted linear in the (!*) (#3506)

* Make `unrestricted` linear in its argument

Author: joelberkeley

.gitignore

@@ -49,6 +49,8 @@ idris2docs_venv
 .\#*
 # VS Code
 .vscode/*
+# JetBrains IDEs
+.idea/
 
 # macOS
 .DS_Store

CHANGELOG_NEXT.md

@@ -294,6 +294,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 
 * Added `System.Concurrency.getThreadId` for the chez backend.
 
+* `unrestricted`, for unpacking a `!* a`, now uses its argument once
+
 #### Contrib
 
 * `Data.Vect.Views.Extra` was moved from `contrib` to `base`.

libs/linear/Data/Linear/Notation.idr

@@ -21,6 +21,17 @@ public export
 export prefix 5 !*
 ||| Prefix notation for the linear unrestricted modality
 public export
-record (!*) (a : Type) where
-  constructor MkBang
-  unrestricted : a
+data (!*) : Type -> Type where
+  MkBang : a -> !* a
+
+||| Unpack an unrestricted value in a linear context
+public export
+unrestricted : !* a -@ a
+unrestricted (MkBang unr) = unr
+
+||| Unpack an unrestricted value in a linear context
+|||
+||| A postfix alias for function unrestricted.
+public export
+(.unrestricted) : !* a -@ a
+(.unrestricted) = unrestricted