Documentation: Disclaimer for soundness of uniqueness (ocaml-flambda#…

…3252)

* Update the disclaimer to describe the problem and how it can be worked-around

* We no longer throw an error if a barrier was required

* Fix typo: aliased to unique

jane/doc/extensions/uniqueness/intro.md

@@ -129,4 +129,44 @@ let okay t =
     store t
 ```
 
+## When can you rely on Uniqueness
+
+There are several cases where a value is unique but it is not permitted
+to perform a destructive update (such as a free) on the value:
+
+ - If a record is unique but contains a field annotated by the aliased
+   modality, you may free the record itself but not the aliased field.
+ - If a value mode-crosses uniqueness, it can be unique even though there might
+   be further references. You can check whether a value mode-crosses uniqueness
+   by attempting to cast it from aliased to unique.
+
+Furthermore, we are currently working around a limitation which makes it unsound
+to use uniqueness with pattern-matching. In particular, if `field` had the
+aliased modality, it is currently not permitted to write:
+
+```ocaml
+let bad t =
+  match t with
+  | Con { field } -> field, free t
+```
+
+Since `field` has the aliased modality, this is permitted in our full design for
+uniqueness. However, the compiler may perform the read of `field` after the
+`free`, causing a segfault. Instead, you should adopt the idiom of
+`Ext.Freeable` where all pattern matches happen within a function that takes a
+local reference to the data:
+
+```ocaml
+let okay t =
+  let field =
+    use t (fun t ->
+      match t with
+      | Con { field } -> field)
+  in
+  field, free t
+```
+
+If the function passed to `use` takes its argument locally, this will create the
+necessary protections in the compiler to make this safe from segfaults.
+
 For more details, read [the reference](./reference.md).