PR#7511: Unboxed type with unboxed argument should not be accepted (#1133)

5 files changed, 144 insertions, 11 deletions

diff --git a/Changes b/Changes
index 798518f2b8..d09f6be61a 100644
--- a/Changes
+++ b/Changes
@@ -882,6 +882,9 @@ Next minor version (4.04.1):
     Bigarray.Genarray.change_layout.
   (Damien Doligez and Xavier Leroy, report by Liang Wang)
 
+- PR#7511, GPR#1133: Unboxed type with unboxed argument should not be accepted
+  (Damien Doligez, review by Jeremy Yallop and Leo White)
+
 - GPR#912: Fix segfault in Unix.create_process on Windows caused by wrong header
   configuration.
   (David Allsopp)
diff --git a/VERSION b/VERSION
index 8ee286ea96..c440566d6f 100644
--- a/VERSION
+++ b/VERSION
@@ -1,4 +1,4 @@
-4.05.0+dev8-2017-03-20
+4.05.0+dev9-2017-06-02
 
 # The version string is the first line of this file.
 # It must be in the format described in stdlib/sys.mli
diff --git a/testsuite/tests/typing-unboxed-types/test.ml b/testsuite/tests/typing-unboxed-types/test.ml
index f187b76d81..8e0b337bc8 100644
--- a/testsuite/tests/typing-unboxed-types/test.ml
+++ b/testsuite/tests/typing-unboxed-types/test.ml
@@ -119,3 +119,38 @@ module T : sig
 end = struct
   type t = A of int [@@ocaml.unboxed]
 end;;
+
+(* regression test for PR#7511 (wrong determination of unboxability for GADTs)
+*)
+type 'a s = S : 'a -> 'a s [@@unboxed];;
+type t = T : _ s -> t [@@unboxed];;
+
+(* regression test for GPR#1133 (follow-up to PR#7511) *)
+type 'a s = S : 'a -> 'a option s [@@unboxed];;
+type t = T : _ s -> t [@@unboxed];;
+
+(* Another test for GPR#1133: abstract types *)
+module M : sig
+  type 'a r constraint 'a = unit -> 'b
+  val inj : 'b -> (unit -> 'b) r
+end = struct
+  type 'a r = 'b constraint 'a = unit -> 'b
+  let inj x = x
+end;;
+
+(* reject *)
+type t = T : (unit -> _) M.r -> t [@@unboxed];;
+
+type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed];;
+
+(* reject *)
+type t = T : _ s -> t [@@unboxed];;
+
+(* accept *)
+type 'a t = T : 'a s -> 'a t [@@unboxed];;
+
+
+(* Another corner case from GPR#1133 *)
+type _ s = S : 'a t -> _ s  [@@unboxed]
+ and _ t = T : 'a -> 'a s t
+;;
diff --git a/testsuite/tests/typing-unboxed-types/test.ml.reference b/testsuite/tests/typing-unboxed-types/test.ml.reference
index b555db8d12..10a118d86f 100644
--- a/testsuite/tests/typing-unboxed-types/test.ml.reference
+++ b/testsuite/tests/typing-unboxed-types/test.ml.reference
@@ -144,7 +144,12 @@ Error: Signature mismatch:
 Error: This type cannot be unboxed because
        it might contain both float and non-float values.
        You should annotate it with [@@ocaml.boxed].
-#     type t18 = A : 'a list abs -> t18 [@@unboxed]
+#     Characters 19-69:
+  type t18 = A : _ list abs -> t18 [@@ocaml.unboxed];;
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This type cannot be unboxed because
+       it might contain both float and non-float values.
+       You should annotate it with [@@ocaml.boxed].
 #   *               Characters 176-256:
   ......struct
     type t = A of float [@@ocaml.unboxed]
@@ -159,4 +164,40 @@ Error: Signature mismatch:
        Their internal representations differ:
        the first declaration uses unboxed float representation.
 #     * *           module T : sig type t [@@immediate] end
+#   *   type 'a s = S : 'a -> 'a s [@@unboxed]
+# Characters 0-33:
+  type t = T : _ s -> t [@@unboxed];;
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This type cannot be unboxed because
+       it might contain both float and non-float values.
+       You should annotate it with [@@ocaml.boxed].
+#     type 'a s = S : 'a -> 'a option s [@@unboxed]
+# Characters 0-33:
+  type t = T : _ s -> t [@@unboxed];;
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This type cannot be unboxed because
+       it might contain both float and non-float values.
+       You should annotate it with [@@ocaml.boxed].
+#                 module M :
+  sig type 'a r constraint 'a = unit -> 'b val inj : 'b -> (unit -> 'b) r end
+#     Characters 14-59:
+  type t = T : (unit -> _) M.r -> t [@@unboxed];;
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This type cannot be unboxed because
+       it might contain both float and non-float values.
+       You should annotate it with [@@ocaml.boxed].
+#   type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed]
+#     Characters 14-47:
+  type t = T : _ s -> t [@@unboxed];;
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This type cannot be unboxed because
+       it might contain both float and non-float values.
+       You should annotate it with [@@ocaml.boxed].
+#     type 'a t = T : 'a s -> 'a t [@@unboxed]
+#           Characters 42-81:
+  type _ s = S : 'a t -> _ s  [@@unboxed]
+  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: This type cannot be unboxed because
+       it might contain both float and non-float values.
+       You should annotate it with [@@ocaml.boxed].
 # 
diff --git a/typing/typedecl.ml b/typing/typedecl.ml
index fde3963ced..4872da67d7 100644
--- a/typing/typedecl.ml
+++ b/typing/typedecl.ml
@@ -276,13 +276,63 @@ let make_constructor env type_path type_params sargs sret_type =
       widen z;
       targs, Some tret_type, args, Some ret_type
 
+(* Check that the variable [id] is present in the [univ] list. *)
+let check_type_var loc univ id =
+  let f t = (Btype.repr t).id = id in
+  if not (List.exists f univ) then raise (Error (loc, Wrong_unboxed_type_float))
+
+(* Check that all the variables found in [ty] are in [univ].
+   Because [ty] is the argument to an abstract type, the representation
+   of that abstract type could be any subexpression of [ty], in particular
+   any type variable present in [ty].
+*)
+let rec check_unboxed_abstract_arg loc univ ty =
+  match ty.desc with
+  | Tvar _ -> check_type_var loc univ ty.id
+  | Tarrow (_, t1, t2, _)
+  | Tfield (_, _, t1, t2) ->
+    check_unboxed_abstract_arg loc univ t1;
+    check_unboxed_abstract_arg loc univ t2
+  | Ttuple args
+  | Tconstr (_, args, _)
+  | Tpackage (_, _, args) ->
+    List.iter (check_unboxed_abstract_arg loc univ) args
+  | Tobject (fields, r) ->
+    check_unboxed_abstract_arg loc univ fields;
+    begin match !r with
+    | None -> ()
+    | Some (_, args) -> List.iter (check_unboxed_abstract_arg loc univ) args
+    end
+  | Tnil
+  | Tunivar _ -> ()
+  | Tlink e -> check_unboxed_abstract_arg loc univ e
+  | Tsubst _ -> assert false
+  | Tvariant { row_fields; row_more; row_name } ->
+    List.iter (check_unboxed_abstract_row_field loc univ) row_fields;
+    check_unboxed_abstract_arg loc univ row_more;
+    begin match row_name with
+    | None -> ()
+    | Some (_, args) -> List.iter (check_unboxed_abstract_arg loc univ) args
+    end
+  | Tpoly (t, _) -> check_unboxed_abstract_arg loc univ t
+
+and check_unboxed_abstract_row_field loc univ (_, field) =
+  match field with
+  | Rpresent (Some ty) -> check_unboxed_abstract_arg loc univ ty
+  | Reither (_, args, _, r) ->
+    List.iter (check_unboxed_abstract_arg loc univ) args;
+    begin match !r with
+    | None -> ()
+    | Some f -> check_unboxed_abstract_row_field loc univ ("", f)
+    end
+  | Rabsent
+  | Rpresent None -> ()
+
 (* Check that the argument to a GADT constructor is compatible with unboxing
-   the type, given the existential variables introduced by this constructor. *)
-let rec check_unboxed_gadt_arg loc ex env ty =
+   the type, given the universal parameters of the type. *)
+let rec check_unboxed_gadt_arg loc univ env ty =
   match get_unboxed_type_representation env ty with
-  | Some {desc = Tvar _; id} ->
-    let f t = (Btype.repr t).id = id in
-    if List.exists f ex then raise(Error(loc, Wrong_unboxed_type_float))
+  | Some {desc = Tvar _; id} -> check_type_var loc univ id
   | Some {desc = Tarrow _ | Ttuple _ | Tpackage _ | Tobject _ | Tnil
                  | Tvariant _; _} ->
     ()
@@ -292,10 +342,10 @@ let rec check_unboxed_gadt_arg loc ex env ty =
     let tydecl = Env.find_type p env in
     assert (not tydecl.type_unboxed.unboxed);
     if tydecl.type_kind = Type_abstract then
-      List.iter (check_unboxed_gadt_arg loc ex env) args
+      List.iter (check_unboxed_abstract_arg loc univ) args
   | Some {desc = Tfield _ | Tlink _ | Tsubst _; _} -> assert false
   | Some {desc = Tunivar _; _} -> ()
-  | Some {desc = Tpoly (t2, _); _} -> check_unboxed_gadt_arg loc ex env t2
+  | Some {desc = Tpoly (t2, _); _} -> check_unboxed_gadt_arg loc univ env t2
   | None -> ()
       (* This case is tricky: the argument is another (or the same) type
          in the same recursive definition. In this case we don't have to
@@ -388,10 +438,14 @@ let transl_declaration env sdecl id =
                unboxed (or abstract) type constructor applied to some
                existential type variable. Of course we also have to rule
                out any abstract type constructor applied to anything that
-               might be an existential type variable. *)
+               might be an existential type variable.
+               There is a difficulty with existential variables created
+               out of thin air (rather than bound by the declaration).
+               See PR#7511 and GPR#1133 for details. *)
             match Datarepr.constructor_existentials args ret_type with
             | _, [] -> ()
-            | [argty], ex -> check_unboxed_gadt_arg sdecl.ptype_loc ex env argty
+            | [argty], _ex ->
+                check_unboxed_gadt_arg sdecl.ptype_loc params env argty
             | _ -> assert false
           end;
           let tcstr =