Respond to more review for the structured error messages (ocaml#10407)

testsuite/tests/typing-short-paths/short-paths.ml

@@ -57,6 +57,10 @@ module N2 = struct type u = v and v = M1.v end;;
 module type PR6566 = sig type t = string end;;
 module PR6566 = struct type t = int end;;
 module PR6566' : PR6566 = PR6566;;
+(* Short-paths is currently a bit overzealous with this error message: we print
+   "The type t is not equal to the type string" instead of "The type int is not
+   equal to the type string".  This is correct, but less clear than it could
+   be. *)
 
 module A = struct module B = struct type t = T end end;;
 module M2 = struct type u = A.B.t type foo = int type v = A.B.t end;;

testsuite/tests/typing-unboxed/test.ml

@@ -445,7 +445,7 @@ Error: Signature mismatch:
          val f : int -> int
        is not included in
          external f : int -> int = "f" "f_nat"
-       The definition is not a primitive
+       The implementation is not a primitive
 |}]
 
 (* Good: not claiming something is a primitive when it is *)

typing/ctype.ml

@@ -57,6 +57,20 @@ open Local_store
 
 (**** Errors ****)
 
+(* There are two classes of errortrace-related exceptions: *traces* and
+   *errors*.  The former, whose names end with [_trace], contain
+   [Errortrace.trace]s, representing traces that are currently being built; they
+   are local to this file.  All the internal functions that implement
+   unification, type equality, and moregen raise trace exceptions.  Once we are
+   done, in the top level functions such as [unify], [equal], and [moregen], we
+   catch the trace exceptions and transform them into the analogous error
+   exception.  This indicates that we are done building the trace, and expect
+   the error to flow out of unification, type equality, or moregen into
+   surrounding code (with some few exceptions when these top-level functions are
+   used as building blocks elsewhere.)  Only the error exceptions are exposed in
+   [ctype.mli]; the trace exceptions are an implementation detail.  Any trace
+   exception that escapes from a function in this file is a bug. *)
+
 exception Unify_trace    of unification trace
 exception Equality_trace of comparison  trace
 exception Moregen_trace  of comparison  trace
@@ -2147,7 +2161,7 @@ let expanded_diff env ~got ~expected =
 (* Diff while transforming a [type_expr] into an [expanded_type] without
    expanding *)
 let unexpanded_diff ~got ~expected =
-  Diff (map_diff unexpanded_type {got; expected})
+  Diff (map_diff trivial_expansion {got; expected})
 
 (**** Unification ****)
 
@@ -3625,12 +3639,14 @@ let moregeneral env inst_nongen pat_sch subj_sch =
        try
          moregen inst_nongen (TypePairs.create 13) env patt subj
        with Moregen_trace trace ->
-         (* In order to properly detect and print weak variables when printing
-            this error, we need to regeneralize the levels of the types after
-            they were instantiated at [generic_level - 1] above.  Because
+         (* Moregen splits the generic level into two finer levels:
+            [generic_level] and [generic_level - 1].  In order to properly
+            detect and print weak variables when printing this error, we need to
+            merge them back together, by regeneralizing the levels of the types
+            after they were instantiated at [generic_level - 1] above.  Because
             [moregen] does some unification that we need to preserve for more
             legible error messages, we have to manually perform the
-            rengeneralization rather than backtracking. *)
+            regeneralization rather than backtracking. *)
          current_level := generic_level - 2;
          generalize subj_inst;
          raise (Moregen {trace = expand_trace env trace}))
@@ -3692,10 +3708,10 @@ let matches ~expand_error_trace env ty ty' =
         backtrack snap;
         let diff =
           if expand_error_trace
-          then expanded_diff env
-          else unexpanded_diff
+          then expanded_diff env ~got:ty ~expected:ty'
+          else unexpanded_diff ~got:ty ~expected:ty'
         in
-        raise (Matches_failure (env, {trace = [diff ~got:ty ~expected:ty']}))
+        raise (Matches_failure (env, {trace = [diff]}))
       end;
       backtrack snap
   | exception Unify err ->
@@ -4124,12 +4140,14 @@ let match_class_types ?(trace=true) env pat_sch subj_sch =
   begin match res with
   | []   -> ()
   | _::_ ->
-    (* If [res] is nonempty, we've found an error.  In order to properly detect
-       and print weak variables when printing this error, we need to
-       regeneralize the levels of the types after they were instantiated at
-       [generic_level - 1] above.  Because we may do unification that we need to
-       preserve for more legible error messages, we have to manually perform the
-       rengeneralization rather than backtracking. *)
+    (* If [res] is nonempty, we've found an error.  Moregen splits the generic
+       level into two finer levels: [generic_level] and [generic_level - 1].  In
+       order to properly detect and print weak variables when printing this
+       error, we need to merge them back together, by regeneralizing the levels
+       of the types after they were instantiated at [generic_level - 1] above.
+       Because [moregen] does some unification that we need to preserve for more
+       legible error messages, we have to manually perform the regeneralization
+       rather than backtracking. *)
     current_level := generic_level - 2;
     generalize_class_type true subj_inst;
   end;

typing/ctype.mli

@@ -193,18 +193,18 @@ val expand_head_opt: Env.t -> type_expr -> type_expr
 (** The compiler's own version of [expand_head] necessary for type-based
     optimisations. *)
 
-(* Expansion of types for error traces; lives here instead of in [Errortrace]
-   because the expansion machinery lives here. *)
+(** Expansion of types for error traces; lives here instead of in [Errortrace]
+    because the expansion machinery lives here. *)
 
-(* Create an [Errortrace.Diff] by expanding the two types *)
+(** Create an [Errortrace.Diff] by expanding the two types *)
 val expanded_diff :
   Env.t ->
   got:type_expr -> expected:type_expr ->
   (Errortrace.expanded_type, 'variant) Errortrace.elt
 
-(* Create an [Errortrace.Diff] by *duplicating* the two types, so that each
-   one's expansion is identical to itself.  Despite the name, does create
-   [Errortrace.expanded_type]s. *)
+(** Create an [Errortrace.Diff] by *duplicating* the two types, so that each
+    one's expansion is identical to itself.  Despite the name, does create
+    [Errortrace.expanded_type]s. *)
 val unexpanded_diff :
   got:type_expr -> expected:type_expr ->
   (Errortrace.expanded_type, 'variant) Errortrace.elt

typing/errortrace.ml

@@ -30,7 +30,7 @@ let print_pos ppf = function
 
 type expanded_type = { ty: type_expr; expanded: type_expr }
 
-let unexpanded_type ty = { ty; expanded = ty }
+let trivial_expansion ty = { ty; expanded = ty }
 
 type 'a diff = { got: 'a; expected: 'a }
 

typing/errortrace.mli

@@ -24,12 +24,12 @@ val print_pos : Format.formatter -> position -> unit
 
 type expanded_type = { ty: type_expr; expanded: type_expr }
 
-(** [unexpanded_type ty] creates an [expanded_type] whose expansion is also
+(** [trivial_expansion ty] creates an [expanded_type] whose expansion is also
     [ty].  Usually, you want [Ctype.expand_type] instead, since the expansion
     carries useful information; however, in certain circumstances, the error is
     about the expansion of the type, meaning that actually performing the
     expansion produces more confusing or inaccurate output. *)
-val unexpanded_type : type_expr -> expanded_type
+val trivial_expansion : type_expr -> expanded_type
 
 type 'a diff = { got: 'a; expected: 'a }
 

typing/includecore.ml

@@ -218,14 +218,14 @@ let report_value_mismatch first second env ppf err =
   | Primitive_mismatch pm ->
       report_primitive_mismatch first second ppf pm
   | Not_a_primitive ->
-      pr "The definition is not a primitive"
+      pr "The implementation is not a primitive"
   | Type trace ->
-      Printtyp.report_moregen_error ppf Scheme env trace
+      Printtyp.report_moregen_error ppf Type_scheme env trace
         (fun ppf -> Format.fprintf ppf "The type")
         (fun ppf -> Format.fprintf ppf "is not compatible with the type")
 
 let report_type_inequality env ppf err =
-  Printtyp.report_equality_error ppf Scheme env err
+  Printtyp.report_equality_error ppf Type_scheme env err
     (fun ppf -> Format.fprintf ppf "The type")
     (fun ppf -> Format.fprintf ppf "is not equal to the type")
 
@@ -522,17 +522,17 @@ let privacy_mismatch env decl1 decl2 =
       | Type_abstract, Type_abstract
         when Option.is_some decl2.type_manifest -> begin
           match decl1.type_manifest with
-          | Some ty1 -> Some begin
+          | Some ty1 -> begin
             let ty1 = Ctype.expand_head env ty1 in
             match ty1.desc with
             | Tvariant row when Btype.is_constr_row ~allow_ident:true
                                   (Btype.row_more row) ->
-                Private_row_type
+                Some Private_row_type
             | Tobject (fi, _) when Btype.is_constr_row ~allow_ident:true
                                      (snd (Ctype.flatten_fields fi)) ->
-                Private_row_type
+                Some Private_row_type
             | _ ->
-                Private_type_abbreviation
+                Some Private_type_abbreviation
             end
           | None ->
               None

typing/includemod_errorprinter.ml

@@ -653,7 +653,7 @@ let core env id x =
         (Printtyp.tree_of_cltype_declaration id diff.got Trec_first)
         !Oprint.out_sig_item
         (Printtyp.tree_of_cltype_declaration id diff.expected Trec_first)
-        (Includeclass.report_error Scheme) diff.symptom
+        (Includeclass.report_error Type_scheme) diff.symptom
         Printtyp.Conflicts.print_explanations
   | Err.Class_declarations {got;expected;symptom} ->
       let t1 = Printtyp.tree_of_class_declaration id got Trec_first in
@@ -663,7 +663,7 @@ let core env id x =
          %a@;<1 -2>does not match@ %a@]@ %a%t"
         !Oprint.out_sig_item t1
         !Oprint.out_sig_item t2
-        (Includeclass.report_error Scheme) symptom
+        (Includeclass.report_error Type_scheme) symptom
         Printtyp.Conflicts.print_explanations
 
 let missing_field ppf item =

typing/printtyp.ml

@@ -782,6 +782,15 @@ let best_type_path p =
 
 (* Print a type expression *)
 
+(* When printing a type scheme, we print weak names.  When printing a plain
+   type, we do not.  This type controls that behavior *)
+type type_or_scheme = Type | Type_scheme
+
+let is_non_gen mode ty =
+  match mode with
+  | Type_scheme -> is_Tvar ty && ty.level <> generic_level
+  | Type        -> false
+
 module Names : sig
   val reset_names : unit -> unit
 
@@ -800,13 +809,9 @@ module Names : sig
 
   val with_local_names : (unit -> 'a) -> 'a
 
-  (* For [print_items], which is itself for the toplevel *)
-  val refresh_weak :
-    (type_expr ->
-     string ->
-     string TypeMap.t * String.Set.t ->
-     string TypeMap.t * String.Set.t) ->
-    unit
+  (* Refresh the weak variable map in the toplevel; for [print_items], which is
+     itself for the toplevel *)
+  val refresh_weak : unit -> unit
 end = struct
   (* We map from types to names, but not directly; we also store a substitution,
      which maps from types to types.  The lookup process is
@@ -913,9 +918,16 @@ end = struct
         name_subst := old_subst)
       f
 
-  let refresh_weak refresh =
+  let refresh_weak () =
+    let refresh t name (m,s) =
+      if is_non_gen Type_scheme (repr t) then
+        begin
+          TypeMap.add t name m,
+          String.Set.add name s
+        end
+      else m, s in
     let m, s =
-      TypeMap.fold refresh !weak_var_map (TypeMap.empty ,String.Set.empty)  in
+      TypeMap.fold refresh !weak_var_map (TypeMap.empty ,String.Set.empty) in
     named_weak_vars := s;
     weak_var_map := m
 end
@@ -1031,10 +1043,6 @@ let reset_and_mark_loops_list tyl =
 (* Disabled in classic mode when printing an unification error *)
 let print_labels = ref true
 
-(* When printing a type scheme, we print weak names.  When printing a plain
-   type, we do not.  This type controls that behavior *)
-type type_or_scheme = Type | Scheme
-
 let rec tree_of_typexp mode ty =
   let ty = repr ty in
   let px = proxy ty in
@@ -1199,11 +1207,6 @@ and tree_of_typobject mode fi nm =
       fatal_error "Printtyp.tree_of_typobject"
   end
 
-and is_non_gen mode ty =
-  match mode with
-  | Scheme -> is_Tvar ty && ty.level <> generic_level
-  | Type   -> false
-
 and tree_of_typfields mode rest = function
   | [] ->
       let rest =
@@ -1230,9 +1233,9 @@ let type_expr ppf ty =
   reset_and_mark_loops ty;
   marked_type_expr ppf ty
 
-and type_sch ppf ty = typexp Scheme ppf ty
+and type_sch ppf ty = typexp Type_scheme ppf ty
 
-and type_scheme ppf ty = reset_and_mark_loops ty; typexp Scheme ppf ty
+and type_scheme ppf ty = reset_and_mark_loops ty; typexp Type_scheme ppf ty
 
 let type_path ppf p =
   let (p', s) = best_type_path p in
@@ -1243,10 +1246,12 @@ let type_path ppf p =
 (* Maxence *)
 let type_scheme_max ?(b_reset_names=true) ppf ty =
   if b_reset_names then Names.reset_names () ;
-  typexp Scheme ppf ty
+  typexp Type_scheme ppf ty
 (* End Maxence *)
 
-let tree_of_type_scheme ty = reset_and_mark_loops ty; tree_of_typexp Scheme ty
+let tree_of_type_scheme ty =
+  reset_and_mark_loops ty;
+  tree_of_typexp Type_scheme ty
 
 (* Print one type declaration *)
 
@@ -1255,8 +1260,8 @@ let tree_of_constraints params =
     (fun ty list ->
        let ty' = unalias ty in
        if proxy ty != proxy ty' then
-         let tr = tree_of_typexp Scheme ty in
-         (tr, tree_of_typexp Scheme ty') :: list
+         let tr = tree_of_typexp Type_scheme ty in
+         (tr, tree_of_typexp Type_scheme ty') :: list
        else list)
     params []
 
@@ -1580,7 +1585,7 @@ let rec tree_of_class_type mode params =
         tree_of_class_type mode params cty
       else
         let namespace = Namespace.best_class_namespace p' in
-        Octy_constr (tree_of_path namespace p', tree_of_typlist Scheme tyl)
+        Octy_constr (tree_of_path namespace p', tree_of_typlist Type_scheme tyl)
   | Cty_signature sign ->
       let sty = repr sign.csig_self in
       let self_ty =
@@ -1632,7 +1637,7 @@ let class_type ppf cty =
   !Oprint.out_class_type ppf (tree_of_class_type Type [] cty)
 
 let tree_of_class_param param variance =
-  (match tree_of_typexp Scheme param with
+  (match tree_of_typexp Type_scheme param with
     Otyp_var (_, s) -> s
   | _ -> "?"),
   if is_Tvar (repr param) then Asttypes.(NoVariance, NoInjectivity)
@@ -1661,7 +1666,7 @@ let tree_of_class_declaration id cl rs =
   Osig_class
     (vir_flag, Ident.name id,
      List.map2 tree_of_class_param params (class_variance cl.cty_variance),
-     tree_of_class_type Scheme params cl.cty_type,
+     tree_of_class_type Type_scheme params cl.cty_type,
      tree_of_rec rs)
 
 let class_declaration id ppf cl =
@@ -1694,7 +1699,7 @@ let tree_of_cltype_declaration id cl rs =
   Osig_class_type
     (virt, Ident.name id,
      List.map2 tree_of_class_param params (class_variance cl.clty_variance),
-     tree_of_class_type Scheme params cl.clty_type,
+     tree_of_class_type Type_scheme params cl.clty_type,
      tree_of_rec rs)
 
 let cltype_declaration id ppf cl =
@@ -1897,18 +1902,8 @@ let modtype_declaration id ppf decl =
 
 (* For the toplevel: merge with tree_of_signature? *)
 
-(* Refresh weak variable map in the toplevel *)
-let refresh_weak () =
-  Names.refresh_weak (fun t name (m,s) ->
-    if is_non_gen Scheme (repr t) then
-      begin
-        TypeMap.add t name m,
-        String.Set.add name s
-      end
-    else m, s)
-
 let print_items showval env x =
-  refresh_weak();
+  Names.refresh_weak();
   reset_naming_context ();
   Conflicts.reset ();
   let extend_val env (sigitem,outcome) = outcome, showval env sigitem in

typing/printtyp.mli

@@ -160,7 +160,7 @@ val functor_parameters:
   ('b -> Format.formatter -> unit) ->
   (Ident.t option * 'b) list -> Format.formatter -> unit
 
-type type_or_scheme = Type | Scheme
+type type_or_scheme = Type | Type_scheme
 
 val tree_of_signature: Types.signature -> out_sig_item list
 val tree_of_typexp: type_or_scheme -> type_expr -> out_type

typing/typecore.ml

@@ -1306,7 +1306,7 @@ let check_scope_escape loc env level ty =
   with Escape esc ->
     (* We don't expand the type here because if we do, we might expand to the
        type that escaped, leading to confusing error messages. *)
-    let trace = Errortrace.[Escape (map_escape unexpanded_type esc)] in
+    let trace = Errortrace.[Escape (map_escape trivial_expansion esc)] in
     raise (Error(loc, env, Pattern_type_clash({trace}, None)))
 
 type pattern_checking_mode =