Fix tricky typing bug with type substitutions

Changes

@@ -973,6 +973,9 @@ Some of those changes will benefit all OCaml packages.
 - #11879: Bugfix for Ctype.nondep_type
   (Stephen Dolan, review by Gabriel Scherer)
 
+- #11931: Fix tricky typing bug with type substitutions
+  (Stephen Dolan, review by Leo White and Jacques Garrigue)
+
 - #12004: Don't ignore function attributes on lambdas with locally abstract
   types.
   (Chris Casinghino, review by Gabriel Scherer)

testsuite/tests/typing-signatures/regression_tsubst_error.ml

@@ -0,0 +1,12 @@
+(* TEST
+   expect;
+*)
+type t = bool
+module type Subst = sig
+  type t2 := t
+  type _ s = C : 'a -> (t * t2 * 'a) s
+end
+[%%expect{|
+type t = bool
+module type Subst = sig type _ s = C : 'a -> (t * t * 'a) s end
+|}]

typing/ctype.ml

@@ -1521,14 +1521,13 @@ let subst env level priv abbrev oty params args body =
    care about efficiency here.
 *)
 let apply ?(use_current_level = false) env params body args =
+  simple_abbrevs := Mnil;
   let level = if use_current_level then !current_level else generic_level in
   try
     subst env level Public (ref Mnil) None params args body
   with
     Cannot_subst -> raise Cannot_apply
 
-let () = Subst.ctype_apply_env_empty := apply Env.empty
-
                               (****************************)
                               (*  Abbreviation expansion  *)
                               (****************************)

typing/subst.ml

@@ -157,7 +157,68 @@ let norm = function
   | Tunivar None -> tunivar_none
   | d -> d
 
-let ctype_apply_env_empty = ref (fun _ -> assert false)
+let apply_type_function params args body =
+  For_copy.with_scope (fun copy_scope ->
+    List.iter2
+      (fun param arg ->
+        For_copy.redirect_desc copy_scope param (Tsubst (arg, None)))
+      params args;
+    let rec copy ty =
+      assert (get_level ty = generic_level);
+      match get_desc ty with
+      | Tsubst (ty, _) -> ty
+      | Tvariant row ->
+          let t = newgenstub ~scope:(get_scope ty) in
+          For_copy.redirect_desc copy_scope ty (Tsubst (t, None));
+          let more = row_more row in
+          assert (get_level more = generic_level);
+          let mored = get_desc more in
+          (* We must substitute in a subtle way *)
+          (* Tsubst takes a tuple containing the row var and the variant *)
+          let desc' =
+            match mored with
+            | Tsubst (_, Some ty2) ->
+                (* This variant type has been already copied *)
+                (* Change the stub to avoid Tlink in the new type *)
+                For_copy.redirect_desc copy_scope ty (Tsubst (ty2, None));
+                Tlink ty2
+            | _ ->
+                let more' =
+                  match mored with
+                    Tsubst (ty, None) -> ty
+                    (* TODO: is this case possible?
+                       possibly an interaction with (copy more) below? *)
+                  | Tconstr _ | Tnil ->
+                      copy more
+                  | Tvar _ | Tunivar _ ->
+                      newgenty mored
+                  |  _ -> assert false
+                in
+                let row =
+                  match get_desc more' with (* PR#6163 *)
+                    Tconstr (x,_,_) when not (is_fixed row) ->
+                      let Row {fields; more; closed; name} = row_repr row in
+                      create_row ~fields ~more ~closed ~name
+                        ~fixed:(Some (Reified x))
+                  | _ -> row
+                in
+                (* Register new type first for recursion *)
+                For_copy.redirect_desc copy_scope more
+                  (Tsubst(more', Some t));
+                (* Return a new copy *)
+                Tvariant (copy_row copy true row false more')
+          in
+          Transient_expr.set_stub_desc t desc';
+          t
+      | desc ->
+          let t = newgenstub ~scope:(get_scope ty) in
+          For_copy.redirect_desc copy_scope ty (Tsubst (t, None));
+          let desc' = copy_type_desc copy desc in
+          Transient_expr.set_stub_desc t desc';
+          t
+    in
+    copy body)
+
 
 (* Similar to [Ctype.nondep_type_rec]. *)
 let rec typexp copy_scope s ty =
@@ -206,7 +267,7 @@ let rec typexp copy_scope s ty =
          | exception Not_found -> Tconstr(type_path s p, args, ref Mnil)
          | Path _ -> Tconstr(type_path s p, args, ref Mnil)
          | Type_function { params; body } ->
-            Tlink (!ctype_apply_env_empty params body args)
+            Tlink (apply_type_function params args body)
          end
       | Tpackage(p, fl) ->
           Tpackage(modtype_path s p,

typing/subst.mli

@@ -84,11 +84,6 @@ val module_declaration: scoping -> t -> module_declaration -> module_declaration
      apply (compose s1 s2) x = apply s2 (apply s1 x) *)
 val compose: t -> t -> t
 
-(* A forward reference to be filled in ctype.ml. *)
-val ctype_apply_env_empty:
-  (type_expr list -> type_expr -> type_expr list -> type_expr) ref
-
-
 module Lazy : sig
   type module_decl =
     {