Make Tsubst directly retain two arguments, instead of nesting a Ttuple (

#10174)

.depend

@@ -6284,6 +6284,8 @@ toplevel/trace.cmi : \
     typing/path.cmi \
     parsing/longident.cmi \
     typing/env.cmi
+toplevel/byte/topdirs.cmi : \
+    parsing/longident.cmi
 toplevel/byte/topeval.cmo : \
     utils/warnings.cmi \
     typing/types.cmi \
@@ -6363,11 +6365,20 @@ toplevel/byte/topeval.cmi : \
     typing/path.cmi \
     parsing/parsetree.cmi \
     typing/env.cmi
+toplevel/byte/toploop.cmi : \
+    utils/warnings.cmi \
+    typing/types.cmi \
+    typing/path.cmi \
+    parsing/parsetree.cmi \
+    typing/outcometree.cmi \
+    parsing/longident.cmi \
+    parsing/location.cmi \
+    typing/env.cmi
 toplevel/byte/topmain.cmo : \
     toplevel/byte/trace.cmi \
-    toplevel/toploop.cmi \
+    toplevel/byte/toploop.cmi \
     toplevel/byte/topeval.cmi \
-    toplevel/topdirs.cmi \
+    toplevel/byte/topdirs.cmi \
     toplevel/topcommon.cmi \
     typing/printtyp.cmi \
     typing/path.cmi \
@@ -6382,9 +6393,9 @@ toplevel/byte/topmain.cmo : \
     toplevel/byte/topmain.cmi
 toplevel/byte/topmain.cmx : \
     toplevel/byte/trace.cmx \
-    toplevel/toploop.cmx \
+    toplevel/byte/toploop.cmi \
     toplevel/byte/topeval.cmx \
-    toplevel/topdirs.cmx \
+    toplevel/byte/topdirs.cmi \
     toplevel/topcommon.cmx \
     typing/printtyp.cmx \
     typing/path.cmx \

Changes

@@ -8,6 +8,12 @@ Working version
     'let* x = x in ...' and 'let%ext x = x in ...' respectively.
   (Stephen Dolan, review by Gabriel Scherer)
 
+### Type system:
+
+- #10174: Make Tsubst more robust by avoiding strange workarounds
+  (Takafumi Saikawa and Jacques Garrigue, review by Gabriel Scherer and
+   Florian Angeletti)
+
 ### Runtime system:
 
 - #9284: Add -config option to display the configuration of ocamlrun on stdout,
@@ -69,7 +75,7 @@ Working version
   with respect to closing.
   (Xavier Leroy, report by Jacques-Henri Jourdan, review by Guillaume
    Munch-Maccagnoni, Gabriel Scherer, Jacques-Henri Jourdan)
-  
+
 - #10139: Remove confusing navigation bar from stdlib documentation.
   Removes the 'Up', 'Previous' and 'Next' links from the top of each standard
   library module's documentation.

ocamldoc/odoc_misc.ml

@@ -506,8 +506,8 @@ let remove_option typ =
     | Types.Tnil
     | Types.Tvariant _
     | Types.Tpackage _ -> t
-    | Types.Tlink t2
-    | Types.Tsubst t2 -> iter t2.Types.desc
+    | Types.Tlink t2 -> iter t2.Types.desc
+    | Types.Tsubst _ -> assert false
   in
   Types.Private_type_expr.create (iter typ.Types.desc)
     ~level:typ.Types.level ~scope:typ.Types.scope ~id:typ.Types.id

ocamldoc/odoc_str.ml

@@ -32,23 +32,24 @@ let string_of_variance t (co,cn) =
 let rec is_arrow_type t =
   match t.Types.desc with
     Types.Tarrow _ -> true
-  | Types.Tlink t2 | Types.Tsubst t2 -> is_arrow_type t2
+  | Types.Tlink t2 -> is_arrow_type t2
   | Types.Ttuple _
   | Types.Tconstr _
   | Types.Tvar _ | Types.Tunivar _ | Types.Tobject _ | Types.Tpoly _
   | Types.Tfield _ | Types.Tnil | Types.Tvariant _ | Types.Tpackage _ -> false
+  | Types.Tsubst _ -> assert false
 
 let raw_string_of_type_list sep type_list =
   let buf = Buffer.create 256 in
   let fmt = Format.formatter_of_buffer buf in
   let rec need_parent t =
     match t.Types.desc with
       Types.Tarrow _ | Types.Ttuple _ -> true
-    | Types.Tlink t2 | Types.Tsubst t2 -> need_parent t2
-    | Types.Tconstr _ ->
-        false
+    | Types.Tlink t2 -> need_parent t2
+    | Types.Tconstr _
     | Types.Tvar _ | Types.Tunivar _ | Types.Tobject _ | Types.Tpoly _
     | Types.Tfield _ | Types.Tnil | Types.Tvariant _ | Types.Tpackage _ -> false
+    | Types.Tsubst _ -> assert false
   in
   let print_one_type variance t =
     Printtyp.mark_loops t;

ocamldoc/odoc_value.ml

@@ -76,8 +76,6 @@ let parameter_list_from_arrows typ =
       Types.Tarrow (l, t1, t2, _) ->
         (l, t1) :: (iter t2)
     | Types.Tlink texp
-    | Types.Tsubst texp ->
-        iter texp
     | Types.Tpoly (texp, _) -> iter texp
     | Types.Tvar _
     | Types.Ttuple _
@@ -89,6 +87,8 @@ let parameter_list_from_arrows typ =
     | Types.Tpackage _
     | Types.Tvariant _ ->
         []
+    | Types.Tsubst _ ->
+        assert false
   in
   iter typ
 
@@ -114,10 +114,10 @@ let dummy_parameter_list typ =
             { Odoc_parameter.sn_name = normal_name label ;
               Odoc_parameter.sn_type = t ;
               Odoc_parameter.sn_text = None }
-    | Types.Tlink t2
-    | Types.Tsubst t2 ->
+    | Types.Tlink t2 ->
         (iter (label, t2))
-
+    | Types.Tsubst _ ->
+        assert false
     | _ ->
         Odoc_parameter.Simple_name
           { Odoc_parameter.sn_name = normal_name label ;

testsuite/tests/typing-misc/filter_params.ml

@@ -0,0 +1,8 @@
+(* TEST
+   * expect
+*)
+
+type ('a, 'b) t constraint 'a = 'b
+[%%expect{|
+type ('b, 'a) t constraint 'a = 'b
+|}]

toplevel/genprintval.ml

@@ -473,9 +473,7 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct
                 find row.row_fields
           | Tobject (_, _) ->
               Oval_stuff "<obj>"
-          | Tsubst ty ->
-              tree_of_val (depth - 1) obj ty
-          | Tfield(_, _, _, _) | Tnil | Tlink _ ->
+          | Tsubst _ | Tfield(_, _, _, _) | Tnil | Tlink _ ->
               fatal_error "Printval.outval_of_value"
           | Tpoly (ty, _) ->
               tree_of_val (depth - 1) obj ty

typing/btype.ml

@@ -300,7 +300,7 @@ let rec fold_row f init row =
 let iter_row f row =
   fold_row (fun () v -> f v) () row
 
-let fold_type_expr f init ty =
+let rec fold_type_expr f init ty =
   match ty.desc with
     Tvar _              -> init
   | Tarrow (_, ty1, ty2, _) ->
@@ -320,8 +320,8 @@ let fold_type_expr f init ty =
     let result = f init ty1 in
     f result ty2
   | Tnil                -> init
-  | Tlink ty            -> f init ty
-  | Tsubst ty           -> f init ty
+  | Tlink ty            -> fold_type_expr f init ty
+  | Tsubst _            -> assert false
   | Tunivar _           -> init
   | Tpoly (ty, tyl)     ->
     let result = f init ty in
@@ -487,15 +487,6 @@ let rec copy_kind = function
 let copy_commu c =
   if commu_repr c = Cok then Cok else Clink (ref Cunknown)
 
-(* Since univars may be used as row variables, we need to do some
-   encoding during substitution *)
-let rec norm_univar ty =
-  match ty.desc with
-    Tunivar _ | Tsubst _ -> ty
-  | Tlink ty           -> norm_univar ty
-  | Ttuple (ty :: _)   -> norm_univar ty
-  | _                  -> assert false
-
 let rec copy_type_desc ?(keep_names=false) f = function
     Tvar _ as ty        -> if keep_names then ty else Tvar None
   | Tarrow (p, ty1, ty2, c)-> Tarrow (p, f ty1, f ty2, copy_commu c)
@@ -512,7 +503,7 @@ let rec copy_type_desc ?(keep_names=false) f = function
   | Tsubst _            -> assert false
   | Tunivar _ as ty     -> ty (* always keep the name *)
   | Tpoly (ty, tyl)     ->
-      let tyl = List.map (fun x -> norm_univar (f x)) tyl in
+      let tyl = List.map f tyl in
       Tpoly (f ty, tyl)
   | Tpackage (p, n, l)  -> Tpackage (p, n, List.map f l)
 

typing/ctype.ml

@@ -1134,7 +1134,7 @@ let rec copy ?partial ?keep_names scope ty =
   let copy = copy ?partial ?keep_names scope in
   let ty = repr ty in
   match ty.desc with
-    Tsubst ty -> ty
+    Tsubst (ty, _) -> ty
   | _ ->
     if ty.level <> generic_level && partial = None then ty else
     (* We only forget types that are non generic and do not contain
@@ -1153,7 +1153,7 @@ let rec copy ?partial ?keep_names scope ty =
     For_copy.save_desc scope ty desc;
     let t = newvar() in          (* Stub *)
     set_scope t ty.scope;
-    Private_type_expr.set_desc ty (Tsubst t);
+    Private_type_expr.set_desc ty (Tsubst (t, None));
     Private_type_expr.set_desc t
       begin match desc with
       | Tconstr (p, tl, _) ->
@@ -1182,17 +1182,17 @@ let rec copy ?partial ?keep_names scope ty =
           (* We must substitute in a subtle way *)
           (* Tsubst takes a tuple containing the row var and the variant *)
           begin match more.desc with
-            Tsubst {desc = Ttuple [_;ty2]} ->
+            Tsubst (_, Some ty2) ->
               (* This variant type has been already copied *)
-              Private_type_expr.set_desc ty (Tsubst ty2);
+              Private_type_expr.set_desc ty (Tsubst (ty2, None));
               (* avoid Tlink in the new type *)
               Tlink ty2
           | _ ->
               (* If the row variable is not generic, we must keep it *)
               let keep = more.level <> generic_level && partial = None in
               let more' =
                 match more.desc with
-                  Tsubst ty -> ty
+                  Tsubst (ty, None) -> ty
                   (* TODO: is this case possible?
                      possibly an interaction with (copy more) below? *)
                 | Tconstr _ | Tnil ->
@@ -1235,7 +1235,7 @@ let rec copy ?partial ?keep_names scope ty =
               in
               (* Register new type first for recursion *)
               Private_type_expr.set_desc
-                more (Tsubst(newgenty(Ttuple[more';t])));
+                more (Tsubst (more', Some t));
               (* Return a new copy *)
               Tvariant (copy_row copy true row keep more')
           end
@@ -1449,8 +1449,10 @@ let rec copy_sep cleanup_scope fixed free bound visited ty =
       match ty.desc with
         Tarrow _ | Ttuple _ | Tvariant _ | Tconstr _ | Tobject _ | Tpackage _ ->
           (ty,(t,bound)) :: visited
-      | Tvar _ | Tfield _ | Tnil | Tpoly _ | Tunivar _ | Tlink _ | Tsubst _ ->
+      | Tvar _ | Tfield _ | Tnil | Tpoly _ | Tunivar _ ->
           visited
+      | Tlink _ | Tsubst _ ->
+          assert false
     in
     let copy_rec = copy_sep cleanup_scope fixed free bound visited in
     Private_type_expr.set_desc t
@@ -1477,6 +1479,7 @@ let rec copy_sep cleanup_scope fixed free bound visited ty =
   end
 
 let instance_poly' cleanup_scope ~keep_names fixed univars sch =
+  (* In order to compute univars below, [sch] schould not contain [Tsubst] *)
   let univars = List.map repr univars in
   let copy_var ty =
     match ty.desc with
@@ -1498,14 +1501,15 @@ let instance_poly ?(keep_names=false) fixed univars sch =
 
 let instance_label fixed lbl =
   For_copy.with_scope (fun scope ->
-    let ty_res = copy scope lbl.lbl_res in
     let vars, ty_arg =
       match repr lbl.lbl_arg with
         {desc = Tpoly (ty, tl)} ->
           instance_poly' scope ~keep_names:false fixed tl ty
       | _ ->
           [], copy scope lbl.lbl_arg
     in
+    (* call [copy] after [instance_poly] to avoid introducing [Tsubst] *)
+    let ty_res = copy scope lbl.lbl_res in
     (vars, ty_arg, ty_res)
   )
 
@@ -2058,7 +2062,7 @@ let polyfy env ty vars =
     | Tvar name when ty.level = generic_level ->
         For_copy.save_desc scope ty ty.desc;
         let t = newty (Tunivar name) in
-        Private_type_expr.set_desc ty (Tsubst t);
+        Private_type_expr.set_desc ty (Tsubst (t, None));
         Some t
     | _ -> None
   in

typing/printtyp.ml

@@ -518,7 +518,9 @@ and raw_type_desc ppf = function
         raw_type t1 raw_type t2
   | Tnil -> fprintf ppf "Tnil"
   | Tlink t -> fprintf ppf "@[<1>Tlink@,%a@]" raw_type t
-  | Tsubst t -> fprintf ppf "@[<1>Tsubst@,%a@]" raw_type t
+  | Tsubst (t, None) -> fprintf ppf "@[<1>Tsubst@,(%a,None)@]" raw_type t
+  | Tsubst (t, Some t') ->
+      fprintf ppf "@[<1>Tsubst@,(%a,@ Some%a)@]" raw_type t raw_type t'
   | Tunivar name -> fprintf ppf "Tunivar %a" print_name name
   | Tpoly (t, tl) ->
       fprintf ppf "@[<hov1>Tpoly(@,%a,@,%a)@]"
@@ -915,7 +917,7 @@ let rec mark_loops_rec visited ty =
     | Tfield(_, _, _, ty2) ->
         mark_loops_rec visited ty2
     | Tnil -> ()
-    | Tsubst ty -> mark_loops_rec visited ty
+    | Tsubst _ -> ()  (* we do not print arguments *)
     | Tlink _ -> fatal_error "Printtyp.mark_loops_rec (2)"
     | Tpoly (ty, tyl) ->
         List.iter (fun t -> add_alias t) tyl;
@@ -1022,8 +1024,9 @@ let rec tree_of_typexp sch ty =
         tree_of_typobject sch fi !nm
     | Tnil | Tfield _ ->
         tree_of_typobject sch ty None
-    | Tsubst ty ->
-        tree_of_typexp sch ty
+    | Tsubst _ ->
+        (* This case should only happen when debugging the compiler *)
+        Otyp_stuff "<Tsubst>"
     | Tlink _ ->
         fatal_error "Printtyp.tree_of_typexp"
     | Tpoly (ty, []) ->
@@ -1162,8 +1165,12 @@ let filter_params tyl =
     List.fold_left
       (fun tyl ty ->
         let ty = repr ty in
-        if List.memq ty tyl then Btype.newgenty (Tsubst ty) :: tyl
+        if List.memq ty tyl then Btype.newgenty (Ttuple [ty]) :: tyl
         else ty :: tyl)
+      (* Two parameters might be identical due to a constraint but we need to
+         print them differently in order to make the output syntactically valid.
+         We use [Ttuple [ty]] because it is printed as [ty]. *)
+      (* Replacing fold_left by fold_right does not work! *)
       [] tyl
   in List.rev params
 

typing/subst.ml

@@ -155,12 +155,12 @@ let rec typexp copy_scope s ty =
           else newty2 ty.level desc
         in
         For_copy.save_desc copy_scope ty desc;
-        Private_type_expr.set_desc ty (Tsubst ty');
+        Private_type_expr.set_desc ty (Tsubst (ty', None));
         (* TODO: move this line to btype.ml
            there is a similar problem also in ctype.ml *)
         ty'
       else ty
-  | Tsubst ty ->
+  | Tsubst (ty, _) ->
       ty
   | Tfield (m, k, _t1, _t2) when not s.for_saving && m = dummy_method
       && field_kind_repr k <> Fabsent && (repr ty).level < generic_level ->
@@ -179,8 +179,7 @@ let rec typexp copy_scope s ty =
     (* Make a stub *)
     let ty' = if s.for_saving then newpersty (Tvar None) else newgenvar () in
     Private_type_expr.set_scope ty' ty.scope;
-    (* TODO: figure out why not use set_scope *)
-    Private_type_expr.set_desc ty (Tsubst ty');
+    Private_type_expr.set_desc ty (Tsubst (ty', None));
     Private_type_expr.set_desc ty'
       begin if has_fixed_row then
         match tm.desc with (* PR#7348 *)
@@ -216,9 +215,9 @@ let rec typexp copy_scope s ty =
           (* We must substitute in a subtle way *)
           (* Tsubst takes a tuple containing the row var and the variant *)
           begin match more.desc with
-            Tsubst {desc = Ttuple [_;ty2]} ->
+            Tsubst (_, Some ty2) ->
               (* This variant type has been already copied *)
-              Private_type_expr.set_desc ty (Tsubst ty2);
+              Private_type_expr.set_desc ty (Tsubst (ty2, None));
               (* avoid Tlink in the new type *)
               Tlink ty2
           | _ ->
@@ -228,7 +227,7 @@ let rec typexp copy_scope s ty =
               (* Various cases for the row variable *)
               let more' =
                 match more.desc with
-                  Tsubst ty -> ty
+                  Tsubst (ty, None) -> ty
                 | Tconstr _ | Tnil -> typexp copy_scope s more
                 | Tunivar _ | Tvar _ ->
                     For_copy.save_desc copy_scope more more.desc;
@@ -238,7 +237,7 @@ let rec typexp copy_scope s ty =
               in
               (* Register new type first for recursion *)
               Private_type_expr.set_desc more
-                (Tsubst(newgenty(Ttuple[more';ty'])));
+                (Tsubst (more', Some ty'));
               (* TODO: check if more' can be eliminated *)
               (* Return a new copy *)
               let row =