Small improvements

Author: goldfirere

jane/doc/extensions/kinds/index.md

@@ -50,7 +50,7 @@ Basic kinds have the form:
 
 For example, the type `(int -> int) option` has the kind `value mod contended
 immutable non_float`. Here, the layout `value` indicates that members of this
-type have the shape of normal OCaml data (and can be garbage collected), and the
+type have the shape of normal OCaml data, and the
 bounds `contended immutable` indicates that they can safely ignore the
 *contention* (any value of this type can be treated as if it were created in the
 current thread) and *visibility* axes (no part of this type is mutable, and so
@@ -127,8 +127,7 @@ stateless <= value mod observing`, and bounding by the maximum mode has no
 effect. However, along the past modal axes, a _higher_ mode leads to a lower
 kind. So `value mod contended <= value mod sharing` and bounding by the minimum
 mode has no effect. We can think of the past axes as flipped, when used in a
-kind. This is because `value mod contended` is more restrictive (describes fewer
-types) than `value mod sharing`, and so we must flip these past axes (somewhat
+kind. This is because `value mod contended` is more restrictive than `value mod sharing` (the former contains types that do not care at all about the value of the contention axis, while the latter contains types that still care about the distinction between `contended` and `sharing`/`uncontended`), and so we must flip these past axes (somewhat
 unfortunately).
 
 If you want to get nerdy about it, each individual piece of a kind (the layout

jane/doc/extensions/kinds/syntax.md

@@ -344,8 +344,9 @@ end
 ```
 
 The kind chosen for `'a t` in the signature is `value` (as described below), and
-thus inferring `'a : any` in the signature would not be safe: it would allow us
-to smuggle, say, a `float64` type where only `value`s are expected.
+thus inferring `'a : any` in the signature (and then accepting the module
+inclusion) would not be safe: it would allow us to smuggle, say, a `float64`
+type where only `value`s are expected.
 
 Accordingly, all type parameters are assumed to have a layout other than `any`
 and also bounded by `non_null` -- unless you write a kind annotation saying
@@ -356,8 +357,8 @@ annotation is not ignored, but instead causes the initial assumed kind of `'a`
 to be `any`, allowing that kind to be lowered by usages of `'a`.
 
 If type inference ends and we still do not know what layout should be used for
-the parameter (this can happen only without an annotation), we default the
-layout to `value_non_null`.
+the parameter (this can happen only without an annotation), we infer the
+kind `value`.
 
 Abstract types are treated identically to concrete ones; it's just that abstract
 types have no right-hand side to use to perform inference, and so an unnanotated