Restrict subtyping (#1970)

rossberg · web-flow · commit 3f92a7773659 · 2020-09-25T13:19:15.000Z
I realised that we allow quantifier bounds to vary under subtyping, which is undecidable, see Pierce's POPL '92 paper. This change enforces equivalence.
diff --git a/src/mo_types/type.ml b/src/mo_types/type.ml
@@ -680,6 +680,7 @@ let stable t = serializable true t
    TODO: haul string_of_typ before the lub/glb business, if possible *)
 let str = ref (fun _ -> failwith "")
 
+
 (* Equivalence & Subtyping *)
 
 module SS = Set.Make (struct type t = typ * typ let compare = compare end)
@@ -748,7 +749,7 @@ let rec rel_typ rel eq t1 t2 =
     rel_list rel_typ rel eq ts1 ts2
   | Func (s1, c1, tbs1, t11, t12), Func (s2, c2, tbs2, t21, t22) ->
     s1 = s2 && c1 = c2 &&
-    (match rel_binds rel eq tbs1 tbs2 with
+    (match rel_binds eq eq tbs1 tbs2 with
     | Some ts ->
       rel_list rel_typ rel eq (List.map (open_ ts) t21) (List.map (open_ ts) t11) &&
       rel_list rel_typ rel eq (List.map (open_ ts) t12) (List.map (open_ ts) t22)
@@ -818,6 +819,9 @@ and eq t1 t2 : bool =
 and sub t1 t2 : bool =
   rel_typ (ref SS.empty) (ref SS.empty) t1 t2
 
+and eq_binds tbs1 tbs2 =
+  let eq = ref SS.empty in rel_binds eq eq tbs1 tbs2 <> None
+
 and eq_kind' eq k1 k2 : bool =
   match k1, k2 with
   | Def (tbs1, t1), Def (tbs2, t2)
@@ -843,6 +847,7 @@ and eq_con eq c1 c2 =
 
 let eq_kind k1 k2 : bool = eq_kind' (ref SS.empty) k1 k2
 
+
 (* Compatibility *)
 
 let compatible_list p co xs1 xs2 =
@@ -997,8 +1002,7 @@ let rec lub' lubs glbs t1 t2 =
     | Obj (s1, tf1), Obj (s2, tf2) when s1 = s2 ->
       Obj (s1, lub_fields lubs glbs tf1 tf2)
     | Func (s1, c1, bs1, args1, res1), Func (s2, c2, bs2, args2, res2) when
-        s1 = s2 && c1 = c2 && List.(length bs1 = length bs2) &&
-        List.for_all2 (fun b1 b2 -> b1.sort = b2.sort) bs1 bs2 &&
+        s1 = s2 && c1 = c2 && eq_binds bs1 bs2 &&
         List.(length args1 = length args2 && length res1 = length res2) ->
       combine_func_parts s1 c1 bs1 args1 res1 bs2 args2 res2 lubs glbs glb' lub'
     | Async (t11, t12), Async (t21, t22) when eq t11 t21 ->
@@ -1071,8 +1075,7 @@ and glb' lubs glbs t1 t2 =
       | Some fs -> Obj (s1, fs)
       )
     | Func (s1, c1, bs1, args1, res1), Func (s2, c2, bs2, args2, res2) when
-        s1 = s2 && c1 = c2 && List.(length bs1 = length bs2) &&
-        List.for_all2 (fun b1 b2 -> b1.sort = b2.sort) bs1 bs2 &&
+        s1 = s2 && c1 = c2 && eq_binds bs1 bs2 &&
         List.(length args1 = length args2 && length res1 = length res2) ->
       combine_func_parts s1 c1 bs1 args1 res1 bs2 args2 res2 lubs glbs lub' glb'
     | Async (t11, t12), Async (t21, t22) when eq t11 t21 ->
@@ -1129,10 +1132,8 @@ and combine_func_parts s c bs1 args1 res1 bs2 args2 res2 lubs glbs contra co =
   let get_con = function | Con (c, []) -> c | _ -> assert false in
   let cs = map get_con ts1 in
   let cl = map (close cs) in
-  let combine_binds =
-    map2 (fun b1 b2 -> {b1 with bound = contra lubs glbs b1.bound b2.bound}) in
   Func (
-    s, c, combine_binds bs1 bs2,
+    s, c, bs1,
     cl (map2 (contra lubs glbs) (op args1) (op args2)),
     cl (map2 (co lubs glbs) (op res1) (op res2))
   )
diff --git a/test/fail/bounds-mismatch.mo b/test/fail/bounds-mismatch.mo
@@ -0,0 +1,129 @@
+{
+  func f(g : <A>() -> ()) {};
+  f(func<A>() {});  // okay
+};
+
+{
+  func f(g : <A <: Nat>() -> ()) {};
+  f(func<A <: Nat>() {});  // okay
+};
+
+{
+  func f(g : <A>() -> ()) {};
+  f(func() {});  // error
+};
+
+{
+  func f(g : () -> ()) {};
+  f(func<A>() {});  // error
+};
+
+{
+  func f(g : <A>() -> ()) {};
+  f(func<A <: Nat>() {});  // error
+};
+
+{
+  func f(g : <A <: Nat>() -> ()) {};
+  f(func<A>() {});  // error
+};
+
+{
+  func f(g : <A <: Int>() -> ()) {};
+  f(func<A <: Nat>() {});  // error
+};
+
+{
+  func f(g : <A <: Nat>() -> ()) {};
+  f(func<A <: Int>() {});  // error
+};
+
+{
+  let _ = [func<A>() {}, func<A>() {}];  // okay
+};
+
+{
+  let _ = [func<A <: Nat>() {}, func<A <: Nat>() {}];  // okay
+};
+
+{
+  let _ = [func() {}, func<A>() {}];  // warn
+};
+
+{
+  let _ = [func<A>() {}, func<A <: Nat>() {}];  // warn
+};
+
+{
+  let _ = [func<A <: Int>() {}, func<A <: Nat>() {}];  // warn
+};
+
+{
+  // okay
+  let _ = [func(_ : <A <: Nat>() -> ()) {}, func(_ : <A <: Nat>() -> ()) {}];
+};
+
+{
+  // no warning
+  let _ : [None -> ()] = [func(_ : <A <: Nat>() -> ()) {}, func(_ : <A <: Int>() -> ()) {}];
+};
+
+
+{
+type A = <X> X -> X;
+type B = <Y <: Nat> Y -> Y;
+func f(x : A) : B = x;
+};
+
+{
+type A = <X <: Int, Y <: {}> X -> Y;
+type B = <X <: Int, Y <: {x : Nat}> X -> Y;
+func f(x : A) : B = x;
+};
+
+{
+type A = <X <: Nat, Y> X -> Y;
+type B = <Y <: Nat, X <: Y> Y -> X;
+func f(x : A) : B = x;
+};
+
+{
+type A = <X, Y> X -> X;
+type B = <X <: Y, Y> X -> X;
+func f(x : A) : B = x;
+};
+
+{
+type A = <X, Y, Z <: X> X -> X;
+type B = <X, Y <: X, Z <: Y> X -> X;
+func f(x : A) : B = x;
+};
+
+{
+class C() { public let x = 0 };
+type A = <X <: {x : Int}> X -> X;
+type B = <X <: C> X -> X;
+func f(x : A) : B = x;
+};
+
+{
+class C<X <: Int>() {public func f() : X { f() }};
+type A = <X, Y <: {f : () -> X}> X -> X;
+type B = <X <: Nat, Y <: C<X>> X -> X;
+func f(x : A) : B = x;
+};
+
+{
+class C<X <: Int>() {public func f() : X { f() }};
+type A = <X, Y <: {f : () -> Nat}> X -> X;
+type B = <X <: Nat, Y <: C<X>> X -> X;
+func f(x : A) : B = x;
+};
+
+
+{
+  let poly_funcs4 = [
+    func<A <: Int, B <: Nat> (as : [A], b : B) : A = as[0],
+    func<B <: Nat, A <: Int> (bs : [B], a : A) : B = bs[0]
+  ];
+};
diff --git a/test/fail/ok/bounds-mismatch.tc.ok b/test/fail/ok/bounds-mismatch.tc.ok
@@ -0,0 +1,60 @@
+bounds-mismatch.mo:13.5-13.14: type error, expression of type
+  () -> ()
+cannot produce expected type
+  <A>() -> ()
+bounds-mismatch.mo:18.5-18.17: type error, expression of type
+  <A>() -> ()
+cannot produce expected type
+  () -> ()
+bounds-mismatch.mo:23.5-23.24: type error, expression of type
+  <A <: Nat>() -> ()
+cannot produce expected type
+  <A>() -> ()
+bounds-mismatch.mo:28.5-28.17: type error, expression of type
+  <A>() -> ()
+cannot produce expected type
+  <A <: Nat>() -> ()
+bounds-mismatch.mo:33.5-33.24: type error, expression of type
+  <A <: Nat>() -> ()
+cannot produce expected type
+  <A <: Int>() -> ()
+bounds-mismatch.mo:38.5-38.24: type error, expression of type
+  <A <: Int>() -> ()
+cannot produce expected type
+  <A <: Nat>() -> ()
+bounds-mismatch.mo:50.11-50.36: warning, this array has type [Any] because elements have inconsistent types
+bounds-mismatch.mo:54.11-54.46: warning, this array has type [Any] because elements have inconsistent types
+bounds-mismatch.mo:58.11-58.53: warning, this array has type [Any] because elements have inconsistent types
+bounds-mismatch.mo:75.21-75.22: type error, expression of type
+  <X>X -> X
+cannot produce expected type
+  <Y <: Nat>Y -> Y
+bounds-mismatch.mo:81.21-81.22: type error, expression of type
+  <X <: Int, Y <: {}>X -> Y
+cannot produce expected type
+  <X <: Int, Y <: {x : Nat}>X -> Y
+bounds-mismatch.mo:87.21-87.22: type error, expression of type
+  <X <: Nat, Y>X -> Y
+cannot produce expected type
+  <Y <: Nat, X <: Y>Y -> X
+bounds-mismatch.mo:93.21-93.22: type error, expression of type
+  <X, Y>X -> X
+cannot produce expected type
+  <X <: Y, Y>X -> X
+bounds-mismatch.mo:99.21-99.22: type error, expression of type
+  <X, Y, Z <: X>X -> X
+cannot produce expected type
+  <X, Y <: X, Z <: Y>X -> X
+bounds-mismatch.mo:106.21-106.22: type error, expression of type
+  <X <: {x : Int}>X -> X
+cannot produce expected type
+  <X <: C>X -> X
+bounds-mismatch.mo:113.21-113.22: type error, expression of type
+  <X, Y <: {f : () -> X}>X -> X
+cannot produce expected type
+  <X <: Nat, Y <: C/1<X>>X -> X
+bounds-mismatch.mo:120.21-120.22: type error, expression of type
+  <X, Y <: {f : () -> Nat}>X -> X
+cannot produce expected type
+  <X <: Nat, Y <: C/2<X>>X -> X
+bounds-mismatch.mo:125.21-128.4: warning, this array has type [Any] because elements have inconsistent types
diff --git a/test/fail/ok/bounds-mismatch.tc.ret.ok b/test/fail/ok/bounds-mismatch.tc.ret.ok
@@ -0,0 +1 @@
+Return code 1
diff --git a/test/repl/lib/type-lub.mo b/test/repl/lib/type-lub.mo
@@ -25,10 +25,6 @@ let poly_funcs3 = [ func<A, B> (as : [A], b : B) : A = as[0]
                   , func<B, A> (bs : [B], a : A) : B = bs[0]
                   ];
 
-let poly_funcs4 = [ func<A <: Int, B <: Nat> (as : [A], b : B) : A = as[0]
-                  , func<B <: Nat, A <: Int> (bs : [B], a : A) : B = bs[0]
-                  ];
-
 let funcs = [ func (a : [Int]) : Nat = a.size()
             , func (a : [Nat]) : Int = -42
             ];
diff --git a/test/repl/ok/type-lub-repl.stdout.ok b/test/repl/ok/type-lub-repl.stdout.ok
@@ -17,9 +17,6 @@ Motoko compiler (revision XXX)
 > 3 : Int
 > -42 : Int
 > [func, func] : [(<A, B>([A], B) -> A)]
-> [func, func] : [(<A <: Nat, B <: Nat>([A], B) -> A)]
-> 1 : Nat
-> 11 : Nat
 >   [func, func] : [({#bar} -> ())]
 > > >   [[42], [25], [77]] : [[Any]]
 >   [42, 77, [1, 2, 3]] : [Any]
diff --git a/test/repl/type-lub-repl.sh b/test/repl/type-lub-repl.sh
@@ -19,9 +19,6 @@ poly_funcs2;
 poly_funcs2[0]<Int>([1, 2, 3]);
 poly_funcs2[1]<Char>([1, 2, 3]);
 poly_funcs3;
-poly_funcs4;
-poly_funcs4[0]<Nat, Nat>([1, 2, 3], 42);
-poly_funcs4[1]<Nat, Nat>([11, 22, 33], 25);
 
 variant_funcs;
 variant_funcs[0](#bar);
diff --git a/test/run-drun/type-lub.mo b/test/run-drun/type-lub.mo
@@ -27,10 +27,6 @@ actor a {
                       , func<B, A> (bs : [B], a : A) : B = bs[0]
                       ];
 
-    let poly_funcs4 = [ func<A <: Int, B <: Nat> (as : [A], b : B) : A = as[0]
-                      , func<B <: Nat, A <: Int> (bs : [B], a : A) : B = bs[0]
-                      ];
-
     let funcs = [ func (a : [Int]) : Nat = a.size()
                 , func (a : [Nat]) : Int = -42
                 ];
diff --git a/test/run/type-inclusion.mo b/test/run/type-inclusion.mo
@@ -108,52 +108,52 @@ func f(x : A) : B<Nat> = x;
 
 {
 type A = <X> X -> X;
-type B = <Y <: Nat> Y -> Y;
+type B = <Y> Y -> Y;
 func f(x : A) : B = x;
 };
 
 {
 type A = <X <: Int, Y <: {}> X -> Y;
-type B = <X <: Int, Y <: {x : Nat}> X -> Y;
+type B = <X <: Int, Y <: {}> X -> Y;
 func f(x : A) : B = x;
 };
 
 {
 type A = <X <: Nat, Y> X -> Y;
-type B = <Y <: Nat, X <: Y> Y -> X;
+type B = <Y <: Nat, X> Y -> X;
 func f(x : A) : B = x;
 };
 
 {
 type A = <X, Y> X -> X;
-type B = <X <: Y, Y> X -> X;
+type B = <X, Y> X -> X;
 func f(x : A) : B = x;
 };
 
 {
 type A = <X, Y, Z <: X> X -> X;
-type B = <X, Y <: X, Z <: Y> X -> X;
+type B = <X, Y, Z <: X> X -> X;
 func f(x : A) : B = x;
 };
 
 {
 class C() { public let x = 0 };
-type A = <X <: {x : Int}> X -> X;
+type A = <X <: C> X -> X;
 type B = <X <: C> X -> X;
 func f(x : A) : B = x;
 };
 
 {
 class C<X <: Int>() {public func f() : X { f() }};
-type A = <X, Y <: {f : () -> X}> X -> X;
-type B = <X <: Nat, Y <: C<X>> X -> X;
+type A = <X <: Int, Y <: {f : () -> X}> X -> X;
+type B = <X <: Int, Y <: C<X>> X -> X;
 func f(x : A) : B = x;
 };
 
 {
 class C<X <: Int>() {public func f() : X { f() }};
 type A = <X, Y <: {f : () -> Nat}> X -> X;
-type B = <X <: Nat, Y <: C<X>> X -> X;
+type B = <X, Y <: C<Nat>> X -> X;
 func f(x : A) : B = x;
 };
 
