Allow to name new abstract types in constructor type annotations (oca…

…ml#12507)

Changes

@@ -121,6 +121,10 @@ OCaml 5.2.0
   is given. This allows to work around problems with GADTs in as-patterns.
   (Jacques Garrigue, report by Leo White, review by Gabriel Scherer)
 
+- #11891, #12507: Allow to name new locally abstract types in constructor type
+  annotations.
+  (Jacques Garrigue, report and review by Gabriel Scherer and Florian Angeletti)
+
 ### Runtime system:
 
 - #12193: Re-introduce GC compaction for shared pools

manual/src/tutorials/gadtexamples.etex

@@ -249,7 +249,7 @@ variable "'a" during typing:
 type ('arg,'result,'aux) fn =
   | Fun: ('a ->'b) -> ('a,'b,unit) fn
   | Mem1: ('a ->'b) * 'a * 'b -> ('a, 'b, 'a * 'b) fn
- let apply: ('arg,'result, _ ) fn -> 'arg -> 'result = fun f x ->
+let apply: ('arg,'result, _ ) fn -> 'arg -> 'result = fun f x ->
   match f with
   | Fun f -> f x
   | Mem1 (f,y,fy) -> if x = y then fy else f x
@@ -272,10 +272,23 @@ explicitly. For instance, the following code names the type of the argument of
 type _ closure = Closure : ('a -> 'b) * 'a -> 'b closure
 let eval = fun (Closure (type a) (f, x : (a -> _) * _)) -> f (x : a)
 \end{caml_example*}
-All existential type variables of the constructor must by introduced by
+All existential type variables of the constructor must be introduced by
 the ("type" ...) construct and bound by a type annotation on the
 outside of the constructor argument.
 
+One can additionally bind existentials that were freshly introduced
+by the refinement of another existential type, if they appear in the
+type of the arguments.
+\begin{caml_example*}{verbatim}
+type _ ty =
+  | Int : int ty
+  | Pair : 'b ty * 'c ty -> ('b * 'c) ty
+let rec default : type a. a ty -> a = function
+  | Int -> 0
+  | Pair (type b c) (b, c : b ty * c ty) ->
+      (default b : b), (default c : c)
+\end{caml_example*}
+
 \section{s:gadt-equation-nonlocal-abstract}{Equations on non-local abstract types}
 
 GADT pattern-matching may also add type equations to non-local

testsuite/tests/typing-gadts/name_existentials.ml

@@ -37,9 +37,10 @@ let ko2 = function Dyn (type a b) (a, x : a ty * b) -> ignore (x : b)
 Line 1, characters 42-50:
 1 | let ko2 = function Dyn (type a b) (a, x : a ty * b) -> ignore (x : b)
                                               ^^^^^^^^
-Error: This pattern matches values of type "a ty * b"
-       but a pattern was expected which matches values of type "a ty * a"
-       Type "b" is not compatible with type "a"
+Error: The local name "b" can only be given to an existential variable
+       introduced by this GADT constructor.
+       The type annotation tries to bind it to the name "a"
+       that is already bound.
 |}]
 
 type u = C : 'a * ('a -> 'b list) -> u
@@ -84,7 +85,10 @@ let rec test : type a. a expr -> a = function
 Line 2, characters 22-23:
 2 |   | Int (type b) (n : a) -> n
                           ^
-Error: This type does not bind all existentials in the constructor: "type b. a"
+Error: The local name "b" can only be given to an existential variable
+       introduced by this GADT constructor.
+       The type annotation tries to bind it to the type "'a"
+       that is not a locally abstract type.
 |}]
 
 (* Strange wildcard *)
@@ -117,3 +121,125 @@ let f = function Pair (x, y : int * _) -> x + y
 type ('a, 'b) pair = Pair of 'a * 'b
 val f : (int, int) pair -> int = <fun>
 |}]
+
+
+(* #11891: allow naming more types *)
+(* We stillonly allow to name freshly introduced existentials *)
+
+type _ ty =
+  | Int : int ty
+  | Pair : 'b ty * 'c ty -> ('b * 'c) ty
+let rec example : type a . a ty -> a = function
+| Int -> 0
+| Pair (x, y) -> (example x, example y)
+let rec example : type a . a ty -> a = function
+| Int -> 0
+| Pair (type b c) (x, y : b ty * c ty) -> (example x, example y)
+[%%expect{|
+type _ ty = Int : int ty | Pair : 'b ty * 'c ty -> ('b * 'c) ty
+val example : 'a ty -> 'a = <fun>
+val example : 'a ty -> 'a = <fun>
+|}]
+
+let rec example : type a . a ty -> a = function
+| Int -> 0
+| Pair (type b c) (x, y : b ty * c ty) -> (example x, example (*error*)x)
+[%%expect{|
+Line 3, characters 54-72:
+3 | | Pair (type b c) (x, y : b ty * c ty) -> (example x, example (*error*)x)
+                                                          ^^^^^^^^^^^^^^^^^^
+Error: This expression has type "b" = "$0" but an expression was expected of type
+         "$1"
+|}]
+
+type _ th =
+  | Thunk : 'a * ('a -> 'b) -> 'b th
+let f1 (type a) : a th -> a = function
+  | Thunk (type b) (x, f : b * (b -> _)) -> f x
+let f2 (type a) : a th -> a = function
+  | Thunk (type b c) (x, f : b * (b -> c)) -> f x
+[%%expect{|
+type _ th = Thunk : 'a * ('a -> 'b) -> 'b th
+val f1 : 'a th -> 'a = <fun>
+Line 6, characters 29-41:
+6 |   | Thunk (type b c) (x, f : b * (b -> c)) -> f x
+                                 ^^^^^^^^^^^^
+Error: The local name "c" can only be given to an existential variable
+       introduced by this GADT constructor.
+       The type annotation tries to bind it to the name "a"
+       that was defined before.
+|}]
+(* Do not allow to deduce extra assumptions *)
+let ko1 (type a) : a th -> a = function
+  | Thunk (type b c) (x, f : b * (b -> c option)) -> f x
+[%%expect{|
+Line 2, characters 29-48:
+2 |   | Thunk (type b c) (x, f : b * (b -> c option)) -> f x
+                                 ^^^^^^^^^^^^^^^^^^^
+Error: This pattern matches values of type "b * (b -> c option)"
+       but a pattern was expected which matches values of type "b * (b -> a)"
+       Type "c option" is not compatible with type "a"
+|}]
+(* Can only name fresh existentials *)
+let ko2 = function
+  | Thunk (type b c) (x, f : b * (b -> c)) -> f x
+[%%expect{|
+Line 2, characters 29-41:
+2 |   | Thunk (type b c) (x, f : b * (b -> c)) -> f x
+                                 ^^^^^^^^^^^^
+Error: The local name "c" can only be given to an existential variable
+       introduced by this GADT constructor.
+       The type annotation tries to bind it to the type "'a"
+       that is not a locally abstract type.
+|}]
+let ko3 () =
+  match [] with
+  | [Thunk (type b c) (x, f : b * (b -> c))] -> f x
+  | _ -> assert false
+[%%expect{|
+Line 3, characters 30-42:
+3 |   | [Thunk (type b c) (x, f : b * (b -> c))] -> f x
+                                  ^^^^^^^^^^^^
+Error: The local name "c" can only be given to an existential variable
+       introduced by this GADT constructor.
+       The type annotation tries to bind it to the type "'a"
+       that is not a locally abstract type.
+|}]
+
+type _ tho =
+  | Thunk_opt : 'b * ('b -> 'c option) -> 'c option tho
+let f3 (type a) : a tho -> a = function
+  | Thunk_opt (type b c) (x, f : b * (b -> c option)) -> f x
+[%%expect{|
+type _ tho = Thunk_opt : 'b * ('b -> 'c option) -> 'c option tho
+val f3 : 'a tho -> 'a = <fun>
+|}]
+
+
+(* check locality *)
+type 'a wrap = Wrap of 'a
+type _ ty = Int : int ty | Pair : ('b ty * 'c ty) wrap -> ('b * 'c) ty
+(* ok *)
+let rec default : type a. a ty -> a = function
+  | Int -> 0
+  | Pair (type b c) (Wrap (b, c) : (b ty * c ty) wrap) ->
+      (default b : b), (default c : c)
+[%%expect{|
+type 'a wrap = Wrap of 'a
+type _ ty = Int : int ty | Pair : ('b ty * 'c ty) wrap -> ('b * 'c) ty
+val default : 'a ty -> 'a = <fun>
+|}]
+(* ko *)
+let rec default : type a. a ty -> a = function
+  | Int -> 0
+  | Pair (Wrap (type b c) (b, c : b ty * c ty)) ->
+      (default b : b), (default c : c)
+[%%expect{|
+Line 3, characters 34-45:
+3 |   | Pair (Wrap (type b c) (b, c : b ty * c ty)) ->
+                                      ^^^^^^^^^^^
+Error: The local name "b" can only be given to an existential variable
+       introduced by this GADT constructor.
+       The type annotation tries to bind it to the name "$0"
+       that was defined before.
+|}]

typing/ident.ml

@@ -111,6 +111,9 @@ let stamp = function
   | Scoped { stamp; _ } -> stamp
   | _ -> 0
 
+let compare_stamp id1 id2 =
+  compare (stamp id1) (stamp id2)
+
 let scope = function
   | Scoped { scope; _ } -> scope
   | Local _ -> highest_scope

typing/ident.mli

@@ -50,7 +50,11 @@ val same: t -> t -> bool
             [create_*], or if they are both persistent and have the same
             name. *)
 
+val compare_stamp: t -> t -> int
+        (** Compare only the internal stamps, 0 if absent *)
+
 val compare: t -> t -> int
+        (** Compare identifiers structurally, including the name *)
 
 val global: t -> bool
 val is_predef: t -> bool

typing/typecore.ml

@@ -96,6 +96,11 @@ type existential_restriction =
   | In_class_def  (** or in [class c = let ... in ...] *)
   | In_self_pattern (** or in self pattern *)
 
+type existential_binding =
+  | Bind_already_bound
+  | Bind_not_in_scope
+  | Bind_non_locally_abstract
+
 type error =
   | Constructor_arity_mismatch of Longident.t * int * int
   | Label_mismatch of Longident.t * Errortrace.unification_error
@@ -189,6 +194,7 @@ type error =
   | Andop_type_clash of string * Errortrace.unification_error
   | Bindings_type_clash of Errortrace.unification_error
   | Unbound_existential of Ident.t list * type_expr
+  | Bind_existential of existential_binding * Ident.t * type_expr
   | Missing_type_constraint
   | Wrong_expected_kind of wrong_kind_sort * wrong_kind_context * type_expr
   | Expr_not_a_record_type of type_expr
@@ -747,23 +753,31 @@ let solve_Ppat_tuple (type a) ~refine loc env (args : a list) expected_ty =
   vars
 
 let solve_constructor_annotation
-    tps (penv : Pattern_env.t) name_list sty ty_args ty_ex =
+    tps (penv : Pattern_env.t) name_list sty ty_args ty_ex unify_res =
   let expansion_scope = penv.equations_scope in
-  let ids =
+  (* Introduce fresh type names that expand to type variables.
+     They should eventually be bound to ground types. *)
+  let ids_decls =
     List.map
       (fun name ->
-        let decl = new_local_type ~loc:name.loc Definition in
+        let tv = newvar () in
+        let decl =
+          new_local_type ~loc:name.loc Definition
+            ~manifest_and_scope:(tv, Ident.lowest_scope) in
         let (id, new_env) =
           Env.enter_type ~scope:expansion_scope name.txt decl !!penv in
         Pattern_env.set_env penv new_env;
-        {name with txt = id})
+        ({name with txt = id}, (decl, tv)))
       name_list
   in
+  (* Translate the type annotation using these type names. *)
   let cty, ty, force =
     with_local_level ~post:(fun (_,ty,_) -> generalize_structure ty)
       (fun () -> Typetexp.transl_simple_type_delayed !!penv sty)
   in
   tps.tps_pattern_force <- force :: tps.tps_pattern_force;
+  (* Only unify the return type after generating the ids *)
+  unify_res ();
   let ty_args =
     let ty1 = instance ty and ty2 = instance ty in
     match ty_args with
@@ -777,24 +791,62 @@ let solve_constructor_annotation
           Ttuple tyl -> tyl
         | _ -> assert false
   in
-  if ids <> [] then ignore begin
-    let ids = List.map (fun x -> x.txt) ids in
+  if ids_decls <> [] then begin
+    let ids_decls = List.map (fun (x,dm) -> (x.txt,dm)) ids_decls in
+    let ids = List.map fst ids_decls in
     let rem =
+      (* First process the existentials introduced by this constructor.
+         Just need to make their definitions abstract. *)
       List.fold_left
         (fun rem tv ->
           match get_desc tv with
-            Tconstr(Path.Pident id, [], _) when List.mem id rem ->
-              list_remove id rem
+            Tconstr(Path.Pident id, [], _) when List.mem_assoc id rem ->
+              let decl, tv' = List.assoc id ids_decls in
+              let env =
+                Env.add_type ~check:false id
+                  {decl with type_manifest = None} !!penv
+              in
+              Pattern_env.set_env penv env;
+              (* We have changed the definition, so clean up *)
+              Btype.cleanup_abbrev ();
+              (* Since id is now abstract, this does not create a cycle *)
+              unify_pat_types cty.ctyp_loc env tv tv';
+              List.remove_assoc id rem
           | _ ->
               raise (Error (cty.ctyp_loc, !!penv,
                             Unbound_existential (ids, ty))))
-        ids ty_ex
+        ids_decls ty_ex
     in
-    if rem <> [] then
-      raise (Error (cty.ctyp_loc, !!penv,
-                    Unbound_existential (ids, ty)))
+    (* The other type names should be bound to newly introduced existentials. *)
+    let bound_ids = ref ids in
+    List.iter
+      (fun (id, (decl, tv')) ->
+        let tv' = expand_head !!penv tv' in
+        begin match get_desc tv' with
+        | Tconstr (Path.Pident id', [], _) ->
+              if List.exists (Ident.same id') !bound_ids then
+                raise (Error (cty.ctyp_loc, !!penv,
+                              Bind_existential (Bind_already_bound, id, tv')));
+              (* Both id and id' are Scoped identifiers, so their stamps grow *)
+              if Ident.scope id' <> penv.equations_scope
+              || Ident.compare_stamp id id' > 0 then
+                raise (Error (cty.ctyp_loc, !!penv,
+                              Bind_existential (Bind_not_in_scope, id, tv')));
+              bound_ids := id' :: !bound_ids
+        | _ ->
+            raise (Error (cty.ctyp_loc, !!penv,
+                          Bind_existential
+                            (Bind_non_locally_abstract, id, tv')));
+        end;
+        let env =
+          Env.add_type ~check:false id
+            {decl with type_manifest = Some (correct_levels tv')} !!penv
+        in
+        Pattern_env.set_env penv env)
+      rem;
+    if rem <> [] then Btype.cleanup_abbrev ();
   end;
-  ty_args, Some (ids, cty)
+  ty_args, Some (List.map fst ids_decls, cty)
 
 let solve_Ppat_construct ~refine tps penv loc constr no_existentials
         existential_styp expected_ty =
@@ -832,11 +884,12 @@ let solve_Ppat_construct ~refine tps penv loc constr no_existentials
             let ty_args, ty_res, ty_ex =
               instance_constructor existential_treatment constr
             in
-            let equated_types = unify_res ty_res expected_ty in
+            let equated_types = lazy (unify_res ty_res expected_ty) in
             let ty_args, existential_ctyp =
               solve_constructor_annotation tps penv name_list sty ty_args ty_ex
+                (fun () -> ignore (Lazy.force equated_types))
             in
-            ty_args, ty_res, equated_types, existential_ctyp
+            ty_args, ty_res, Lazy.force equated_types, existential_ctyp
       in
       if constr.cstr_existentials <> [] then
         lower_variables_only !!penv penv.Pattern_env.equations_scope ty_res;
@@ -6864,6 +6917,20 @@ let report_error ~loc env = function
         "@[<2>%s:@ %a@]"
         "This type does not bind all existentials in the constructor"
         (Style.as_inline_code pp_type) (ids, ty)
+  | Bind_existential (reason, id, ty) ->
+      let reason1, reason2 = match reason with
+      | Bind_already_bound -> "the name", "that is already bound"
+      | Bind_not_in_scope -> "the name", "that was defined before"
+      | Bind_non_locally_abstract -> "the type",
+          "that is not a locally abstract type"
+      in
+      Location.errorf ~loc
+        "@[<hov0>The local name@ %a@ %s@ %s.@ %s@ %s@ %a@ %s.@]"
+        (Style.as_inline_code Printtyp.ident) id
+        "can only be given to an existential variable"
+        "introduced by this GADT constructor"
+        "The type annotation tries to bind it to"
+        reason1 (Style.as_inline_code Printtyp.type_expr) ty reason2
   | Missing_type_constraint ->
       Location.errorf ~loc
         "@[%s@ %s@]"