Add subtyping between arrows of related modes (oxcaml#20)

lpw25 · web-flow · commit de3bec9aead8 · 2022-05-03T17:55:17.000+01:00
diff --git a/testsuite/tests/typing-local/local.ml b/testsuite/tests/typing-local/local.ml
@@ -1864,3 +1864,56 @@ Error: This expression has type (local_ int list -> unit) -> int -> unit
        Type local_ int list -> unit is not compatible with type
          int list -> unit
 |}]
+
+(* Subtyping *)
+
+let foo f = (f : local_ string -> float :> string -> float)
+[%%expect{|
+val foo : (local_ string -> float) -> string -> float = <fun>
+|}]
+
+let foo f = (f : string -> float :> string -> local_ float)
+[%%expect{|
+val foo : (string -> float) -> string -> local_ float = <fun>
+|}]
+
+let foo f = (f : string -> local_ float :> string -> float)
+[%%expect{|
+Line 1, characters 12-59:
+1 | let foo f = (f : string -> local_ float :> string -> float)
+                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Type string -> local_ float is not a subtype of string -> float
+|}]
+
+let foo f = (f : string -> float :> local_ string -> local_ float)
+[%%expect{|
+Line 1, characters 12-66:
+1 | let foo f = (f : string -> float :> local_ string -> local_ float)
+                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error: Type string -> float is not a subtype of local_ string -> local_ float
+|}]
+
+let foo f = ignore (f :> string -> float); ()
+[%%expect{|
+val foo : (string -> float) -> unit = <fun>
+|}]
+
+let use_local_to_global (f : local_ string -> float) = ()
+
+let foo f = ignore (f :> string -> float); use_local_to_global f
+[%%expect{|
+val use_local_to_global : (local_ string -> float) -> unit = <fun>
+val foo : (local_ string -> float) -> unit = <fun>
+|}]
+
+let use_global_to_local (f : string -> local_ float) = ()
+
+let foo f = ignore (f :> string -> float); use_global_to_local f
+[%%expect{|
+val use_global_to_local : (string -> local_ float) -> unit = <fun>
+Line 3, characters 63-64:
+3 | let foo f = ignore (f :> string -> float); use_global_to_local f
+                                                                   ^
+Error: This expression has type string -> float
+       but an expression was expected of type string -> local_ float
+|}]
diff --git a/testsuite/tests/typing-objects/Tests.ml b/testsuite/tests/typing-objects/Tests.ml
@@ -715,7 +715,7 @@ Error: Multiple definition of the type name t.
 
 fun x -> (x :> < m : 'a -> 'a > as 'a);;
 [%%expect{|
-- : < m : (< m : 'a > as 'b) -> 'b as 'a; .. > -> 'b = <fun>
+- : < m : (< m : 'a -> 'a > as 'a) -> 'a; .. > -> 'a = <fun>
 |}];;
 
 fun x -> (x : int -> bool :> 'a -> 'a);;
diff --git a/typing/btype.ml b/typing/btype.ml
@@ -1075,11 +1075,18 @@ module Alloc_mode = struct
   let newvar () = Amodevar (fresh ())
 
   let newvar_below = function
-    | Amode Global -> Amode Global
+    | Amode Global -> Amode Global, false
     | m ->
        let v = newvar () in
        submode_exn v m;
-       v
+       v, true
+
+  let newvar_above = function
+    | Amode Local -> Amode Local, false
+    | m ->
+       let v = newvar () in
+       submode_exn m v;
+       v, true
 
   let check_const = function
     | Amode m -> Some m
diff --git a/typing/btype.mli b/typing/btype.mli
@@ -290,7 +290,9 @@ module Alloc_mode : sig
 
   val newvar : unit -> t
 
-  val newvar_below : t -> t
+  val newvar_below : t -> t * bool
+
+  val newvar_above : t -> t * bool
 
   val check_const : t -> const option
 
diff --git a/typing/ctype.ml b/typing/ctype.ml
@@ -4147,6 +4147,17 @@ let find_cltype_for_path env p =
 let has_constr_row' env t =
   has_constr_row (expand_abbrev env t)
 
+let build_submode posi m =
+  if posi then begin
+    let m', changed = Btype.Alloc_mode.newvar_below m in
+    let c = if changed then Changed else Unchanged in
+    m', c
+  end else begin
+    let m', changed = Btype.Alloc_mode.newvar_above m in
+    let c = if changed then Changed else Unchanged in
+    m', c
+  end
+
 let rec build_subtype env visited loops posi level t =
   let t = repr t in
   match t.desc with
@@ -4160,14 +4171,19 @@ let rec build_subtype env visited loops posi level t =
           (t, Unchanged)
       else
         (t, Unchanged)
-  | Tarrow(l, t1, t2, _) ->
+  | Tarrow((l,a,r) , t1, t2, _) ->
       if memq_warn t visited then (t, Unchanged) else
       let visited = t :: visited in
       let (t1', c1) = build_subtype env visited loops (not posi) level t1 in
       let (t2', c2) = build_subtype env visited loops posi level t2 in
-      let c = max c1 c2 in
-      (* FIXME update arrow modes *)
-      if c > Unchanged then (newty (Tarrow(l, t1', t2', Cok)), c)
+      let (a', c3) =
+        if level > 2 then build_submode (not posi) a else a, Unchanged
+      in
+      let (r', c4) =
+        if level > 2 then build_submode posi r else r, Unchanged
+      in
+      let c = max c1 (max c2 (max c3 c4)) in
+      if c > Unchanged then (newty (Tarrow((l,a',r'), t1', t2', Cok)), c)
       else (t, Unchanged)
   | Ttuple tlist ->
       if memq_warn t visited then (t, Unchanged) else
@@ -4336,6 +4352,11 @@ let subtypes = TypePairs.create 17
 let subtype_error env trace =
   raise (Subtype (expand_trace env (List.rev trace), []))
 
+let subtype_alloc_mode env trace a1 a2 =
+  match Btype.Alloc_mode.submode a1 a2 with
+  | Ok () -> ()
+  | Error () -> subtype_error env trace
+
 let rec subtype_rec env trace t1 t2 cstrs =
   let t1 = repr t1 in
   let t2 = repr t2 in
@@ -4353,8 +4374,8 @@ let rec subtype_rec env trace t1 t2 cstrs =
          (l1 = l2
           || !Clflags.classic && not (is_optional l1 || is_optional l2)) ->
         let cstrs = subtype_rec env (Trace.diff t2 t1::trace) t2 t1 cstrs in
-        unify_alloc_mode a1 a2; (* FIXME *)
-        unify_alloc_mode r1 r2;
+        subtype_alloc_mode env trace a2 a1;
+        subtype_alloc_mode env trace r1 r2;
         subtype_rec env (Trace.diff u1 u2::trace) u1 u2 cstrs;
     | (Ttuple tl1, Ttuple tl2) ->
         subtype_list env trace tl1 tl2 cstrs
diff --git a/typing/typecore.ml b/typing/typecore.ml
@@ -5287,15 +5287,15 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg
 and type_apply_arg env ~funct ~index ~position ~partial_app (lbl, arg) =
   match arg with
   | Arg (Unknown_arg { sarg; ty_arg; mode_arg }) ->
-      let mode = Alloc_mode.newvar_below mode_arg in
+      let mode, _ = Alloc_mode.newvar_below mode_arg in
       let expected_mode =
         mode_argument ~funct ~index ~position ~partial_app mode in
       let arg = type_expect env expected_mode sarg (mk_expected ty_arg) in
       if is_optional lbl then
         unify_exp env arg (type_option(newvar()));
       (lbl, Arg arg)
   | Arg (Known_arg { sarg; ty_arg; ty_arg0; mode_arg; wrapped_in_some }) ->
-      let mode = Alloc_mode.newvar_below mode_arg in
+      let mode, _ = Alloc_mode.newvar_below mode_arg in
       let expected_mode =
         mode_argument ~funct ~index ~position ~partial_app mode in
       let arg =
