address more comments

ocaml/testsuite/tests/typing-modes/val_modalities_floor.ml

@@ -1,4 +1,4 @@
-(* We test that cmi generaeted without mli has the modalities pushed to the
+(* We test that cmi generated without mli has the modalities pushed to the
 strongest instead of legacy *)
 
 (* TEST

ocaml/typing/env.ml

@@ -1319,9 +1319,9 @@ let find_cltype path env =
 let find_value path env =
   find_value_full path env |> vda_description
 
-let find_value_without_locks id env =
+let find_value_no_locks_exn id env =
   match IdTbl.find_same_and_locks id env.values with
-  | Val_bound _, _ :: _ -> assert false
+  | Val_bound _, _ :: _ -> Misc.fatal_error "locks encountered"
   | Val_bound data, [] -> normalize_vda_mode data
   | Val_unbound _, _ -> raise Not_found
 
@@ -3434,12 +3434,18 @@ let lookup_value ~errors ~use ~loc lid env =
   let path, locks, vda =
     lookup_value_lazy ~errors ~use ~loc lid env
   in
-  (* First, we apply the modalities to acquire the mode of the value at the
-     definition site. Then, we walk the locks. That means the surrounding
-     closure would be closing over the value instead of the module.
-
-     This is better ergonomics, but dangers as it doesn't reflect the real
-     runtime behaviour. With the current set-up, it is sound. *)
+  (* There can be locks between the definition and a use of a value. For
+  example, if a function closes over a value, there will be Closure_lock between
+  the value's definition and the value's use in the function. Walking the locks
+  will constrain the function and the value's modes accrodingly.
+
+  Here, we apply the modalities to acquire the mode of the value at the
+  definition site, using which we walk the locks. That means the surrounding
+  closure would be closing over the value instead of the module. The latter can
+  be achieved by walking the locks before apply modalities.
+
+  Our route provides better ergonomics, but is dangerous as it doesn't reflect
+  the real runtime behaviour. With the current set-up, it is sound. *)
   let vd, mode = normalize_vda_mode vda in
   let vd = Subst.Lazy.force_value_description vd in
   let vmode =

ocaml/typing/env.mli

@@ -84,7 +84,7 @@ val without_cmis: ('a -> 'b) -> 'a -> 'b
 
 (* Lookup by paths *)
 
-val find_value_without_locks: Ident.t -> t ->
+val find_value_no_locks_exn: Ident.t -> t ->
   Subst.Lazy.value_description * Mode.Value.l
 (** Find a value by an [Ident.t]. Raises if encounters any locks. *)
 

ocaml/typing/typemod.ml

@@ -2883,8 +2883,16 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr =
               in
               let (first_loc, _, _) = List.hd id_info in
               Signature_names.check_value names first_loc id;
-              let vd, mode =  Env.find_value_without_locks id newenv in
+              let vd, mode =  Env.find_value_no_locks_exn id newenv in
               let vd = Subst.Lazy.force_value_description vd in
+              (* Upon construction, for comonadic (prescriptive) axes, module
+              must be weaker than the values therein, for otherwise operations
+              would be allowed to performed on the module (and extended to the
+              values) that's disallowed for the values.
+
+              For monadic (descriptive) axes, the restriction is not on the
+              construction but on the projection, which is modelled by the
+              [Diff] modality in [mode.ml]. *)
               begin match Mode.Value.Comonadic.submode
                 mode.Mode.comonadic
                 md_mode.Mode.comonadic with