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

In addition to the smaller fixes, there were two major changes:

1. `Errortrace` has its type completely refactored, removing `desc`
   and exposing both `'variant trace` and `'variant error`.  The
   former is for traces that are being built up, and contains
   `type_expr`s; the lattern is for complete traces, and contains
   `expanded_type`s (a record containing two `type_expr`s).  This
   dramatically affected a number of call sites, but is much cleaner.

2. We now detect weakly polymorphic types much better during
   printing.  This involved fixing a bug in moregeneral, which was not
   restoring enough information in the error case; it also involved
   exposing the flag that differentiated between printing a type (no
   weakly polymorphic type detection) and a scheme (yes weakly
   polymorphic type detection) in more places, and giving it its own
   custom variant type, `Printtyp.type_or_scheme`.

Among the minor changes, the updates to `Includecore` to more
carefully detect privacy violation errors and differentiate between
the various kinds thereof (recorded in the `privacy_mismatch` type) is
the most visible in the code.

1 files changed, 163 insertions, 139 deletions

diff --git a/typing/printtyp.ml b/typing/printtyp.ml
index 5850e1ee56..c486f5c18a 100644
--- a/typing/printtyp.ml
+++ b/typing/printtyp.ml
@@ -1031,11 +1031,15 @@ let reset_and_mark_loops_list tyl =
 (* Disabled in classic mode when printing an unification error *)
 let print_labels = ref true
 
-let rec tree_of_typexp sch ty =
+(* 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
   if Names.has_name px && not (List.memq px !delayed) then
-   let mark = is_non_gen sch ty in
+   let mark = is_non_gen mode ty in
    let name = Names.name_of_type
                 (if mark then Names.new_weak_name ty else Names.new_name)
                 px
@@ -1046,8 +1050,8 @@ let rec tree_of_typexp sch ty =
     match ty.desc with
     | Tvar _ ->
         (*let lev =
-          if is_non_gen sch ty then "/" ^ Int.to_string ty.level else "" in*)
-        let non_gen = is_non_gen sch ty in
+          if is_non_gen mode ty then "/" ^ Int.to_string ty.level else "" in*)
+        let non_gen = is_non_gen mode ty in
         let name_gen =
           if non_gen then Names.new_weak_name ty else Names.new_name
         in
@@ -1061,17 +1065,18 @@ let rec tree_of_typexp sch ty =
             match (repr ty1).desc with
             | Tconstr(path, [ty], _)
               when Path.same path Predef.path_option ->
-                tree_of_typexp sch ty
+                tree_of_typexp mode ty
             | _ -> Otyp_stuff "<hidden>"
-          else tree_of_typexp sch ty1 in
-        Otyp_arrow (lab, t1, tree_of_typexp sch ty2)
+          else tree_of_typexp mode ty1 in
+        Otyp_arrow (lab, t1, tree_of_typexp mode ty2)
     | Ttuple tyl ->
-        Otyp_tuple (tree_of_typlist sch tyl)
+        Otyp_tuple (tree_of_typlist mode tyl)
     | Tconstr(p, tyl, _abbrev) ->
         let p', s = best_type_path p in
         let tyl' = apply_subst s tyl in
-        if is_nth s && not (tyl'=[]) then tree_of_typexp sch (List.hd tyl') else
-        Otyp_constr (tree_of_path Type p', tree_of_typlist sch tyl')
+        if is_nth s && not (tyl'=[])
+        then tree_of_typexp mode (List.hd tyl')
+        else Otyp_constr (tree_of_path Type p', tree_of_typlist mode tyl')
     | Tvariant row ->
         let row = row_repr row in
         let fields =
@@ -1091,47 +1096,47 @@ let rec tree_of_typexp sch ty =
         | Some(p, tyl) when namable_row row ->
             let (p', s) = best_type_path p in
             let id = tree_of_path Type p' in
-            let args = tree_of_typlist sch (apply_subst s tyl) in
+            let args = tree_of_typlist mode (apply_subst s tyl) in
             let out_variant =
               if is_nth s then List.hd args else Otyp_constr (id, args) in
             if row.row_closed && all_present then
               out_variant
             else
-              let non_gen = is_non_gen sch px in
+              let non_gen = is_non_gen mode px in
               let tags =
                 if all_present then None else Some (List.map fst present) in
               Otyp_variant (non_gen, Ovar_typ out_variant, row.row_closed, tags)
         | _ ->
             let non_gen =
-              not (row.row_closed && all_present) && is_non_gen sch px in
-            let fields = List.map (tree_of_row_field sch) fields in
+              not (row.row_closed && all_present) && is_non_gen mode px in
+            let fields = List.map (tree_of_row_field mode) fields in
             let tags =
               if all_present then None else Some (List.map fst present) in
             Otyp_variant (non_gen, Ovar_fields fields, row.row_closed, tags)
         end
     | Tobject (fi, nm) ->
-        tree_of_typobject sch fi !nm
+        tree_of_typobject mode fi !nm
     | Tnil | Tfield _ ->
-        tree_of_typobject sch ty None
+        tree_of_typobject mode ty None
     | Tsubst _ ->
         (* This case should only happen when debugging the compiler *)
         Otyp_stuff "<Tsubst>"
     | Tlink _ ->
         fatal_error "Printtyp.tree_of_typexp"
     | Tpoly (ty, []) ->
-        tree_of_typexp sch ty
+        tree_of_typexp mode ty
     | Tpoly (ty, tyl) ->
         (*let print_names () =
           List.iter (fun (_, name) -> prerr_string (name ^ " ")) !names;
           prerr_string "; " in *)
         let tyl = List.map repr tyl in
-        if tyl = [] then tree_of_typexp sch ty else begin
+        if tyl = [] then tree_of_typexp mode ty else begin
           let old_delayed = !delayed in
           (* Make the names delayed, so that the real type is
              printed once when used as proxy *)
           List.iter add_delayed tyl;
           let tl = List.map (Names.name_of_type Names.new_name) tyl in
-          let tr = Otyp_poly (tl, tree_of_typexp sch ty) in
+          let tr = Otyp_poly (tl, tree_of_typexp mode ty) in
           (* Forget names when we leave scope *)
           Names.remove_names tyl;
           delayed := old_delayed; tr
@@ -1143,7 +1148,7 @@ let rec tree_of_typexp sch ty =
           List.map
             (fun (li, ty) -> (
               String.concat "." (Longident.flatten li),
-              tree_of_typexp sch ty
+              tree_of_typexp mode ty
             )) fl in
         Otyp_module (tree_of_path Module_type p, fl)
   in
@@ -1153,20 +1158,20 @@ let rec tree_of_typexp sch ty =
     Otyp_alias (pr_typ (), Names.name_of_type Names.new_name px) end
   else pr_typ ()
 
-and tree_of_row_field sch (l, f) =
+and tree_of_row_field mode (l, f) =
   match row_field_repr f with
   | Rpresent None | Reither(true, [], _, _) -> (l, false, [])
-  | Rpresent(Some ty) -> (l, false, [tree_of_typexp sch ty])
+  | Rpresent(Some ty) -> (l, false, [tree_of_typexp mode ty])
   | Reither(c, tyl, _, _) ->
       if c (* contradiction: constant constructor with an argument *)
-      then (l, true, tree_of_typlist sch tyl)
-      else (l, false, tree_of_typlist sch tyl)
+      then (l, true, tree_of_typlist mode tyl)
+      else (l, false, tree_of_typlist mode tyl)
   | Rabsent -> (l, false, [] (* actually, an error *))
 
-and tree_of_typlist sch tyl =
-  List.map (tree_of_typexp sch) tyl
+and tree_of_typlist mode tyl =
+  List.map (tree_of_typexp mode) tyl
 
-and tree_of_typobject sch fi nm =
+and tree_of_typobject mode fi nm =
   begin match nm with
   | None ->
       let pr_fields fi =
@@ -1181,12 +1186,12 @@ and tree_of_typobject sch fi nm =
         let sorted_fields =
           List.sort
             (fun (n, _) (n', _) -> String.compare n n') present_fields in
-        tree_of_typfields sch rest sorted_fields in
+        tree_of_typfields mode rest sorted_fields in
       let (fields, rest) = pr_fields fi in
       Otyp_object (fields, rest)
   | Some (p, ty :: tyl) ->
-      let non_gen = is_non_gen sch (repr ty) in
-      let args = tree_of_typlist sch tyl in
+      let non_gen = is_non_gen mode (repr ty) in
+      let args = tree_of_typlist mode tyl in
       let (p', s) = best_type_path p in
       assert (s = Id);
       Otyp_class (non_gen, tree_of_path Type p', args)
@@ -1194,28 +1199,30 @@ and tree_of_typobject sch fi nm =
       fatal_error "Printtyp.tree_of_typobject"
   end
 
-and is_non_gen sch ty =
-    sch && is_Tvar ty && ty.level <> generic_level
+and is_non_gen mode ty =
+  match mode with
+  | Scheme -> is_Tvar ty && ty.level <> generic_level
+  | Type   -> false
 
-and tree_of_typfields sch rest = function
+and tree_of_typfields mode rest = function
   | [] ->
       let rest =
         match rest.desc with
-        | Tvar _ | Tunivar _ -> Some (is_non_gen sch rest)
+        | Tvar _ | Tunivar _ -> Some (is_non_gen mode rest)
         | Tconstr _ -> Some false
         | Tnil -> None
         | _ -> fatal_error "typfields (1)"
       in
       ([], rest)
   | (s, t) :: l ->
-      let field = (s, tree_of_typexp sch t) in
-      let (fields, rest) = tree_of_typfields sch rest l in
+      let field = (s, tree_of_typexp mode t) in
+      let (fields, rest) = tree_of_typfields mode rest l in
       (field :: fields, rest)
 
-let typexp sch ppf ty =
-  !Oprint.out_type ppf (tree_of_typexp sch ty)
+let typexp mode ppf ty =
+  !Oprint.out_type ppf (tree_of_typexp mode ty)
 
-let marked_type_expr ppf ty = typexp false ppf ty
+let marked_type_expr ppf ty = typexp Type ppf ty
 
 let type_expr ppf ty =
   (* [type_expr] is used directly by error message printers,
@@ -1223,9 +1230,9 @@ let type_expr ppf ty =
   reset_and_mark_loops ty;
   marked_type_expr ppf ty
 
-and type_sch ppf ty = typexp true ppf ty
+and type_sch ppf ty = typexp Scheme ppf ty
 
-and type_scheme ppf ty = reset_and_mark_loops ty; typexp true ppf ty
+and type_scheme ppf ty = reset_and_mark_loops ty; typexp Scheme ppf ty
 
 let type_path ppf p =
   let (p', s) = best_type_path p in
@@ -1236,10 +1243,10 @@ 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 true ppf ty
+  typexp Scheme ppf ty
 (* End Maxence *)
 
-let tree_of_type_scheme ty = reset_and_mark_loops ty; tree_of_typexp true ty
+let tree_of_type_scheme ty = reset_and_mark_loops ty; tree_of_typexp Scheme ty
 
 (* Print one type declaration *)
 
@@ -1248,8 +1255,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 true ty in
-         (tr, tree_of_typexp true ty') :: list
+         let tr = tree_of_typexp Scheme ty in
+         (tr, tree_of_typexp Scheme ty') :: list
        else list)
     params []
 
@@ -1360,13 +1367,13 @@ let rec tree_of_type_decl id decl =
         decl.type_params decl.type_variance
     in
     (Ident.name id,
-     List.map2 (fun ty cocn -> type_param (tree_of_typexp false ty), cocn)
+     List.map2 (fun ty cocn -> type_param (tree_of_typexp Type ty), cocn)
        params vari)
   in
   let tree_of_manifest ty1 =
     match ty_manifest with
     | None -> ty1
-    | Some ty -> Otyp_manifest (tree_of_typexp false ty, ty1)
+    | Some ty -> Otyp_manifest (tree_of_typexp Type ty, ty1)
   in
   let (name, args) = type_defined decl in
   let constraints = tree_of_constraints params in
@@ -1376,7 +1383,7 @@ let rec tree_of_type_decl id decl =
         begin match ty_manifest with
         | None -> (Otyp_abstract, Public, false)
         | Some ty ->
-            tree_of_typexp false ty, decl.type_private, false
+            tree_of_typexp Type ty, decl.type_private, false
         end
     | Type_variant (cstrs, rep) ->
         tree_of_manifest (Otyp_sum (List.map tree_of_constructor cstrs)),
@@ -1400,7 +1407,7 @@ let rec tree_of_type_decl id decl =
       otype_cstrs = constraints }
 
 and tree_of_constructor_arguments = function
-  | Cstr_tuple l -> tree_of_typlist false l
+  | Cstr_tuple l -> tree_of_typlist Type l
   | Cstr_record l -> [ Otyp_record (List.map tree_of_label l) ]
 
 and tree_of_constructor cd =
@@ -1410,12 +1417,12 @@ and tree_of_constructor cd =
   | None -> (name, arg (), None)
   | Some res ->
       Names.with_local_names (fun () ->
-        let ret = tree_of_typexp false res in
+        let ret = tree_of_typexp Type res in
         let args = arg () in
         (name, args, Some ret))
 
 and tree_of_label l =
-  (Ident.name l.ld_id, l.ld_mutable = Mutable, tree_of_typexp false l.ld_type)
+  (Ident.name l.ld_id, l.ld_mutable = Mutable, tree_of_typexp Type l.ld_type)
 
 let constructor ppf c =
   reset_except_context ();
@@ -1442,7 +1449,7 @@ let extension_constructor_args_and_ret_type_subtree ext_args ext_ret_type =
   | None -> (tree_of_constructor_arguments ext_args, None)
   | Some res ->
       Names.with_local_names (fun () ->
-        let ret = tree_of_typexp false res in
+        let ret = tree_of_typexp Type res in
         let args = tree_of_constructor_arguments ext_args in
         (args, Some ret))
 
@@ -1461,7 +1468,7 @@ let tree_of_extension_constructor id ext es =
     | _ -> "?"
   in
   let ty_params =
-    List.map (fun ty -> type_param (tree_of_typexp false ty)) ty_params
+    List.map (fun ty -> type_param (tree_of_typexp Type ty)) ty_params
   in
   let name = Ident.name id in
   let args, ret =
@@ -1528,13 +1535,13 @@ let method_type (_, kind, ty) =
     Fpresent, {desc=Tpoly(ty, tyl)} -> (ty, tyl)
   | _       , ty                    -> (ty, [])
 
-let tree_of_metho sch concrete csil (lab, kind, ty) =
+let tree_of_metho mode concrete csil (lab, kind, ty) =
   if lab <> dummy_method then begin
     let kind = field_kind_repr kind in
     let priv = kind <> Fpresent in
     let virt = not (Concr.mem lab concrete) in
     let (ty, tyl) = method_type (lab, kind, ty) in
-    let tty = tree_of_typexp sch ty in
+    let tty = tree_of_typexp mode ty in
     Names.remove_names tyl;
     Ocsg_method (lab, priv, virt, tty) :: csil
   end
@@ -1563,17 +1570,17 @@ let rec prepare_class_type params = function
       mark_loops ty;
       prepare_class_type params cty
 
-let rec tree_of_class_type sch params =
+let rec tree_of_class_type mode params =
   function
   | Cty_constr (p', tyl, cty) ->
       let sty = Ctype.self_type cty in
       if List.memq (proxy sty) !visited_objects
       || not (List.for_all is_Tvar params)
       then
-        tree_of_class_type sch params cty
+        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 true tyl)
+        Octy_constr (tree_of_path namespace p', tree_of_typlist Scheme tyl)
   | Cty_signature sign ->
       let sty = repr sign.csig_self in
       let self_ty =
@@ -1598,12 +1605,12 @@ let rec tree_of_class_type sch params =
       let csil =
         List.fold_left
           (fun csil (l, m, v, t) ->
-            Ocsg_value (l, m = Mutable, v = Virtual, tree_of_typexp sch t)
+            Ocsg_value (l, m = Mutable, v = Virtual, tree_of_typexp mode t)
             :: csil)
           csil all_vars
       in
       let csil =
-        List.fold_left (tree_of_metho sch sign.csig_concr) csil fields
+        List.fold_left (tree_of_metho mode sign.csig_concr) csil fields
       in
       Octy_signature (self_ty, List.rev csil)
   | Cty_arrow (l, ty, cty) ->
@@ -1614,18 +1621,18 @@ let rec tree_of_class_type sch params =
        if is_optional l then
          match (repr ty).desc with
          | Tconstr(path, [ty], _) when Path.same path Predef.path_option ->
-             tree_of_typexp sch ty
+             tree_of_typexp mode ty
          | _ -> Otyp_stuff "<hidden>"
-       else tree_of_typexp sch ty in
-      Octy_arrow (lab, tr, tree_of_class_type sch params cty)
+       else tree_of_typexp mode ty in
+      Octy_arrow (lab, tr, tree_of_class_type mode params cty)
 
 let class_type ppf cty =
   reset ();
   prepare_class_type [] cty;
-  !Oprint.out_class_type ppf (tree_of_class_type false [] cty)
+  !Oprint.out_class_type ppf (tree_of_class_type Type [] cty)
 
 let tree_of_class_param param variance =
-  (match tree_of_typexp true param with
+  (match tree_of_typexp Scheme param with
     Otyp_var (_, s) -> s
   | _ -> "?"),
   if is_Tvar (repr param) then Asttypes.(NoVariance, NoInjectivity)
@@ -1654,7 +1661,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 true params cl.cty_type,
+     tree_of_class_type Scheme params cl.cty_type,
      tree_of_rec rs)
 
 let class_declaration id ppf cl =
@@ -1687,7 +1694,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 true params cl.clty_type,
+     tree_of_class_type Scheme params cl.clty_type,
      tree_of_rec rs)
 
 let cltype_declaration id ppf cl =
@@ -1893,7 +1900,7 @@ let modtype_declaration id ppf decl =
 (* Refresh weak variable map in the toplevel *)
 let refresh_weak () =
   Names.refresh_weak (fun t name (m,s) ->
-    if is_non_gen true (repr t) then
+    if is_non_gen Scheme (repr t) then
       begin
         TypeMap.add t name m,
         String.Set.add name s
@@ -1932,7 +1939,25 @@ let printed_signature sourcefile ppf sg =
   end;
   fprintf ppf "%a" print_signature t
 
-(* Print an unification error *)
+(* Trace-specific printing *)
+
+(* A configuration type that controls which trace we print.  This could be
+   exposed, but we instead expose three separate
+   [report_{unification,equality,moregen}_error] functions.  This also lets us
+   give the unification case an extra optional argument without adding it to the
+   equality and moregen cases. *)
+type 'variety trace_format =
+  | Unification : Errortrace.unification trace_format
+  | Equality    : Errortrace.comparison  trace_format
+  | Moregen     : Errortrace.comparison  trace_format
+
+let incompatibility_phrase (type variety) : variety trace_format -> string =
+  function
+  | Unification -> "is not compatible with type"
+  | Equality    -> "is not equal to type"
+  | Moregen     -> "is not compatible with type"
+
+(* Print a unification error *)
 
 let same_path t t' =
   let t = repr t and t' = repr t' in
@@ -1953,15 +1978,15 @@ let same_path t t' =
 
 type 'a diff = Same of 'a | Diff of 'a * 'a
 
-let trees_of_type_expansion (t,t') =
+let trees_of_type_expansion mode Errortrace.{ty = t; expanded = t'} =
   if same_path t t'
-  then begin add_delayed (proxy t); Same (tree_of_typexp false t) end
+  then begin add_delayed (proxy t); Same (tree_of_typexp mode t) end
   else
     let t' = if proxy t == proxy t' then unalias t' else t' in
     (* beware order matter due to side effect,
        e.g. when printing object types *)
-    let first = tree_of_typexp false t in
-    let second = tree_of_typexp false t' in
+    let first = tree_of_typexp mode t in
+    let second = tree_of_typexp mode t' in
     if first = second then Same first
     else Diff(first,second)
 
@@ -1970,7 +1995,8 @@ let type_expansion ppf = function
   | Diff(t,t') ->
       fprintf ppf "@[<2>%a@ =@ %a@]"  !Oprint.out_type t  !Oprint.out_type t'
 
-let trees_of_trace = List.map (Errortrace.map_diff trees_of_type_expansion)
+let trees_of_trace mode =
+  List.map (Errortrace.map_diff (trees_of_type_expansion mode))
 
 let trees_of_type_path_expansion (tp,tp') =
   if Path.same tp tp' then Same(tree_of_path Type tp) else
@@ -2003,29 +2029,14 @@ type printing_status =
       type error.
   *)
 
-let diff_printing_status { Errortrace.got=t1, t1'; expected=t2, t2'} =
+let diff_printing_status Errortrace.{ got      = {ty = t1; expanded = t1'};
+                                      expected = {ty = t2; expanded = t2'} } =
   if  is_constr_row ~allow_ident:true t1'
    || is_constr_row ~allow_ident:true t2'
   then Discard
   else if same_path t1 t1' && same_path t2 t2' then Optional_refinement
   else Keep
 
-(* A configuration type that controls which trace we print.  This could be
-   exposed, but we instead expose three separate
-   [report_{unification,equality,moregen}_error] functions.  This also lets us
-   give the unification case an extra optional argument without adding it to the
-   equality and moregen cases. *)
-type 'variety trace_format =
-  | Unification : Errortrace.unification trace_format
-  | Equality    : Errortrace.comparison  trace_format
-  | Moregen     : Errortrace.comparison  trace_format
-
-let incompatibility_phrase (type variety) : variety trace_format -> string =
-  function
-  | Unification -> "is not compatible with type"
-  | Equality    -> "is not equal to type"
-  | Moregen     -> "is not compatible with type"
-
 let printing_status = function
   | Errortrace.Diff d -> diff_printing_status d
   | Errortrace.Escape {kind = Constraint} -> Keep
@@ -2046,11 +2057,14 @@ let prepare_any_trace printing_status tr =
   | elt :: rem -> elt :: List.fold_right clean_trace rem []
 
 let prepare_trace f tr =
-  prepare_any_trace printing_status (Errortrace.flatten f tr)
+  prepare_any_trace printing_status (Errortrace.map f tr)
 
 (** Keep elements that are not [Diff _ ] and take the decision
     for the last element, require a prepared trace *)
-let rec filter_trace trace_format keep_last = function
+let rec filter_trace
+          (trace_format : 'variety trace_format)
+          keep_last
+  : ('a, 'variety) Errortrace.t -> _ = function
   | [] -> []
   | [Errortrace.Diff d as elt]
     when printing_status elt = Optional_refinement ->
@@ -2071,17 +2085,17 @@ let hide_variant_name t =
                    row_more = newvar2 (row_more row).level})
   | _ -> t
 
-let prepare_expansion (t, t') =
-  let t' = hide_variant_name t' in
-  mark_loops t;
-  if not (same_path t t') then mark_loops t';
-  (t, t')
+let prepare_expansion Errortrace.{ty; expanded} =
+  let expanded = hide_variant_name expanded in
+  mark_loops ty;
+  if not (same_path ty expanded) then mark_loops expanded;
+  Errortrace.{ty; expanded}
 
-let may_prepare_expansion compact (t, t') =
-  match (repr t').desc with
+let may_prepare_expansion compact (Errortrace.{ty; expanded} as ty_exp) =
+  match (repr expanded).desc with
     Tvariant _ | Tobject _ when compact ->
-      mark_loops t; (t, t)
-  | _ -> prepare_expansion (t, t')
+      mark_loops ty; Errortrace.{ty; expanded = ty}
+  | _ -> prepare_expansion ty_exp
 
 let print_path p = Format.dprintf "%a" !Oprint.out_ident (tree_of_path Type p)
 
@@ -2189,7 +2203,7 @@ let explain_escape pre = function
         "%t@,@[The module type@;<1 2>%a@ would escape its scope@]"
         pre path p
     )
-  | Errortrace.Equation (_,t) -> Some(
+  | Errortrace.Equation Errortrace.{ty = _; expanded = t} -> Some(
       dprintf "%t @,@[<hov>This instance of %a is ambiguous:@ %s@]"
         pre type_expr t
         "it would escape the scope of its equation"
@@ -2213,10 +2227,10 @@ let explain_object (type variety) : variety Errortrace.obj -> _ = function
       Some (dprintf "@,Self type cannot be unified with a closed object type")
 
 let explanation (type variety) intro prev env
-  : ('a, variety) Errortrace.elt -> _ = function
-  | Errortrace.Diff { Errortrace.got = _,s; expected = _,t } ->
-    explanation_diff env s t
-  | Errortrace.Escape {kind;context} ->
+  : (Errortrace.expanded_type, variety) Errortrace.elt -> _ = function
+  | Errortrace.Diff {got; expected} ->
+    explanation_diff env got.expanded expected.expanded
+  | Errortrace.Escape {kind; context} ->
     let pre =
       match context, kind, prev with
       | Some ctx, _, _ ->
@@ -2276,26 +2290,32 @@ let prepare_expansion_head empty_tr = function
       Some (Errortrace.map_diff (may_prepare_expansion empty_tr) d)
   | _ -> None
 
-let head_error_printer txt_got txt_but = function
+let head_error_printer mode txt_got txt_but = function
   | None -> ignore
   | Some d ->
-      let d = Errortrace.map_diff trees_of_type_expansion d in
+      let d = Errortrace.map_diff (trees_of_type_expansion mode) d in
       dprintf "%t@;<1 2>%a@ %t@;<1 2>%a"
         txt_got type_expansion d.Errortrace.got
         txt_but type_expansion d.Errortrace.expected
 
 let warn_on_missing_defs env ppf = function
   | None -> ()
-  | Some {Errortrace.got=te1,_; expected=te2,_ } ->
+  | Some Errortrace.{got      = {ty=te1; expanded=_};
+                     expected = {ty=te2; expanded=_} } ->
       warn_on_missing_def env ppf te1;
       warn_on_missing_def env ppf te2
 
 (* [subst] comes out of equality, and is [[]] otherwise *)
-let error trace_format subst env tr txt1 ppf txt2 ty_expect_explanation =
+let error trace_format mode subst env tr txt1 ppf txt2 ty_expect_explanation =
   reset ();
   (* We want to substitute in the opposite order from [Eqtype] *)
   Names.add_subst (List.map (fun (ty1,ty2) -> ty2,ty1) subst);
-  let tr = prepare_trace (fun t t' -> t, hide_variant_name t') tr in
+  let tr =
+    prepare_trace
+      (fun ty_exp ->
+         Errortrace.{ty_exp with expanded = hide_variant_name ty_exp.expanded})
+      tr
+  in
   let mis = mismatch txt1 env tr in
   match tr with
   | [] -> assert false
@@ -2305,8 +2325,8 @@ let error trace_format subst env tr txt1 ppf txt2 ty_expect_explanation =
       let tr = filter_trace trace_format (mis = None) tr in
       let head = prepare_expansion_head (tr=[]) elt in
       let tr = List.map (Errortrace.map_diff prepare_expansion) tr in
-      let head_error = head_error_printer txt1 txt2 head in
-      let tr = trees_of_trace tr in
+      let head_error = head_error_printer mode txt1 txt2 head in
+      let tr = trees_of_trace mode tr in
       fprintf ppf
         "@[<v>\
           @[%t%t@]%a%t\
@@ -2323,24 +2343,32 @@ let error trace_format subst env tr txt1 ppf txt2 ty_expect_explanation =
       print_labels := true;
       raise exn
 
-let report_error trace_format ppf env tr
+let report_error trace_format ppf mode env tr
       ?(subst = [])
       ?(type_expected_explanation = fun _ -> ())
       txt1 txt2 =
-  wrap_printing_env env (fun () -> error trace_format subst env tr txt1 ppf txt2
-                                     type_expected_explanation)
-    ~error:true
+  wrap_printing_env ~error:true env (fun () ->
+    error trace_format mode subst env tr txt1 ppf txt2
+      type_expected_explanation)
+
+let report_unification_error
+      ppf env ({trace} : Errortrace.unification_error) =
+  report_error Unification ppf Type env
+    ?subst:None trace
+
+let report_equality_error
+      ppf mode env ({subst; trace} : Errortrace.equality_error) =
+  report_error Equality ppf mode env
+    ~subst ?type_expected_explanation:None trace
 
-let report_unification_error ppf env ({trace} : Errortrace.unification_error) =
-  report_error Unification ppf env ?subst:None trace
-let report_equality_error ppf env ({subst; trace} : Errortrace.equality_error) =
-  report_error Equality ppf env ~subst ?type_expected_explanation:None trace
-let report_moregen_error ppf env ({trace} : Errortrace.moregen_error) =
-  report_error Moregen ppf env ?subst:None ?type_expected_explanation:None trace
+let report_moregen_error
+      ppf mode env ({trace} : Errortrace.moregen_error) =
+  report_error Moregen ppf mode env
+    ?subst:None ?type_expected_explanation:None trace
 
-let report_comparison_error ppf env = function
-  | Errortrace.Equality_error error -> report_equality_error ppf env error
-  | Errortrace.Moregen_error  error -> report_moregen_error  ppf env error
+let report_comparison_error ppf mode env = function
+  | Errortrace.Equality_error error -> report_equality_error ppf mode env error
+  | Errortrace.Moregen_error  error -> report_moregen_error  ppf mode env error
 
 module Subtype = struct
   (* There's a frustrating amount of code duplication between this module and
@@ -2355,7 +2383,7 @@ module Subtype = struct
   let prepare_unification_trace = prepare_trace
 
   let prepare_trace f tr =
-    prepare_any_trace printing_status (Errortrace.Subtype.flatten f tr)
+    prepare_any_trace printing_status (Errortrace.Subtype.map f tr)
 
   let trace filter_trace get_diff fst keep_last txt ppf tr =
     print_labels := not !Clflags.classic;
@@ -2363,7 +2391,7 @@ module Subtype = struct
       | elt :: tr' ->
         let diffed_elt = get_diff elt in
         let tr =
-          trees_of_trace
+          trees_of_trace Type
           @@ List.map (Errortrace.map_diff prepare_expansion)
           @@ filter_trace keep_last tr' in
         let tr =
@@ -2390,23 +2418,19 @@ module Subtype = struct
 
   let unification_get_diff = function
     | Errortrace.Diff diff ->
-        Some (Errortrace.map_diff trees_of_type_expansion diff)
+        Some (Errortrace.map_diff (trees_of_type_expansion Type) diff)
     | _ -> None
 
   let subtype_get_diff = function
     | Errortrace.Subtype.Diff diff ->
-        Some (Errortrace.map_diff trees_of_type_expansion diff)
+        Some (Errortrace.map_diff (trees_of_type_expansion Type) diff)
 
   let report_error
         ppf env tr1 txt1 ({trace=tr2} : Errortrace.unification_error) =
     wrap_printing_env ~error:true env (fun () ->
       reset ();
-      let tr1 =
-        prepare_trace (fun t t' -> prepare_expansion (t, t')) tr1
-      in
-      let tr2 =
-        prepare_unification_trace (fun t t' -> prepare_expansion (t, t')) tr2
-      in
+      let tr1 = prepare_trace prepare_expansion tr1 in
+      let tr2 = prepare_unification_trace prepare_expansion tr2 in
       let keep_first = match tr2 with
         | [Obj _ | Variant _ | Escape _ ] | [] -> true
         | _ -> false in
@@ -2446,8 +2470,8 @@ let report_ambiguous_type_error ppf env tp0 tpl txt1 txt2 txt3 =
 (* Adapt functions to exposed interface *)
 let tree_of_path = tree_of_path Other
 let tree_of_modtype = tree_of_modtype ~ellipsis:false
-let type_expansion ty ppf ty' =
-  type_expansion ppf (trees_of_type_expansion (ty,ty'))
+let type_expansion mode ppf ty_exp =
+  type_expansion ppf (trees_of_type_expansion mode ty_exp)
 let tree_of_type_declaration ident td rs =
   with_hidden_items [{hide=true; ident}]
     (fun () -> tree_of_type_declaration ident td rs)