feat: Infer invariant when bound is isolated (no proper super/subtypes except Top/Bottom) (#5359)

Author: Kamirus

src/mo_frontend/bi_match.ml

@@ -138,11 +138,18 @@ let choose_under_constrained ctx lb c ub =
   | Variance.Contravariant -> ub
   | Variance.Bivariant -> lb
   | Variance.Invariant ->
-    raise (Bimatch (Format.asprintf
-      "implicit instantiation of type parameter %s is under-constrained with%a\nwhere%a\nso that explicit type instantiation is required"
-      (Cons.name c)
-      display_constraint (lb, c, ub)
-      display_rel (lb,"=/=",ub)))
+    match normalize lb, normalize ub with
+    (* Ignore [Any] when choosing a bound for the solution *)
+    (* Restrict to [isolated] types only, at least for now *)
+    | t, Any when isolated t ->
+      assert (t <> Non);
+      lb
+    | _ ->
+      raise (Bimatch (Format.asprintf
+        "implicit instantiation of type parameter %s is under-constrained with%a\nwhere%a\nso that explicit type instantiation is required"
+        (Cons.name c)
+        display_constraint (lb, c, ub)
+        display_rel (lb,"=/=",ub)))
 
 let fail_over_constrained lb c ub =
   raise (Bimatch (Format.asprintf

src/mo_types/type.ml

@@ -1479,6 +1479,51 @@ and singleton_field co tf = singleton_typ co tf.typ
 
 and singleton t : bool = singleton_typ (ref S.empty) t
 
+(** A type is isolated if it has no proper supertypes nor proper subtypes (ignoring top [Any] and bottom [Non]). *)
+let rec isolated_typ co = function
+  | Con (c, ts) as t ->
+    (match Cons.kind c with
+    | Abs (_, bound) ->
+      (* Type parameters are isolated when unbounded. *)
+      bound = Any
+    | Def (tbs, def) ->
+      (* Cyclic definitions are isolated until proven otherwise. *)
+      S.mem t !co || begin
+        co := S.add t !co;
+        isolated_typ co (reduce tbs def ts)
+      end
+    )
+  | Mut _ -> true
+  | Named (_, t) -> isolated_typ co t
+  | Prim
+    ( Bool
+    | Nat8
+    | Nat16
+    | Nat32
+    | Nat64
+    | Int8
+    | Int16
+    | Int32
+    | Int64
+    | Float
+    | Char
+    | Text
+    | Blob
+    | Error
+    | Principal
+    | Region
+    (* All except Nat, Int, Null as they have proper super/subtypes: Nat <: Int, ?T <: Null *)
+    ) -> true
+  | Array t
+  | Async (_, _, t)
+  | Weak t -> isolated_typ co t
+  | Tup ts -> List.for_all (isolated_typ co) ts
+  | Func (_, _, _, ts1, ts2) ->
+    List.for_all (isolated_typ co) ts1 &&
+    List.for_all (isolated_typ co) ts2
+  | _ -> false
+
+and isolated t = isolated_typ (ref S.empty) t
 
 (* Least upper bound and greatest lower bound *)
 

src/mo_types/type.mli

@@ -224,6 +224,9 @@ val stable : typ -> bool
 
 val inhabited : typ -> bool
 val singleton : typ -> bool
+
+(** A type is isolated if it has no proper supertypes nor proper subtypes (ignoring top [Any] and bottom [Non]). *)
+val isolated : typ -> bool
 val span : typ -> int option
 
 

test/fail/lambdas-core.mo

@@ -1,6 +1,9 @@
 import Prim "mo:prim";
 func fail<T>() : T = Prim.trap("fail");
 func check<T>(t1 : T, t2 : T) : [T] = [t1, t2]; // used to check type equality
+func check3<T>(t1 : T, t2 : T, t3 : T) : [T] = [t1, t2, t3]; // used to check type equality
+
+type Order = { #less; #equal; #greater };
 
 // Mock functions for Array module
 module Array {
@@ -221,6 +224,7 @@ module Map {
   public func all<K, V>(_map : Map<K, V>, _predicate : (K, V) -> Bool) : Bool = true;
   public func any<K, V>(_map : Map<K, V>, _predicate : (K, V) -> Bool) : Bool = false;
   public func toText<K, V>(_map : Map<K, V>, _keyToText : K -> Text, _valueToText : V -> Text) : Text = "";
+  public func fromIter<K, V>(_iter : Iter<(K, V)>, _compare : (K, K) -> Order) : Map<K, V> = fail();
 };
 
 // Mock functions for pure Map module
@@ -405,19 +409,25 @@ let _ = Set.retainAll(set, natCompare, func n = n % 2 == 0);
 let _ = Set.forEach(set, func _ {});
 let _ = Set.filter(set, natCompare, func n = n % 2 == 0);
 let s1 = Set.map<Nat, Text>(set, func n = natToText(n));
+let s1i = Set.map(set, func n = natToText(n));
 let s2 : Set<Text> = Set.map(set, func n = natToText(n));
-let _ = check(s1, s2);
+let _ = check3(s1, s1i, s2);
 let s3 = Set.filterMap<Nat, Text>(
   set,
   textCompare,
   func n = if (n % 2 == 0) ?natToText(n) else null,
 );
+let s3i = Set.filterMap(
+  set,
+  textCompare,
+  func n = if (n % 2 == 0) ?natToText(n) else null,
+);
 let s4 : Set<Text> = Set.filterMap(
   set,
   textCompare,
   func n = if (n % 2 == 0) ?natToText(n) else null,
 );
-let _ = check(s3, s4);
+let _ = check3(s3, s3i, s4);
 let _ = Set.all(set, func n = n < 10);
 let _ = Set.any(set, func n = n > 5);
 
@@ -445,11 +455,13 @@ let _ = PureSet.any(pureSet, func n = n > 5);
 let _ = Map.forEach(mapInstance, func(key, value) {});
 let _ = Map.filter(mapInstance, natCompare, func(key, value) = key % 2 == 0);
 let m1 = Map.map<Nat, Text, Text>(mapInstance, func(key, value) = natToText(key));
+let m1i = Map.map(mapInstance, func(key, value) = natToText(key));
 let m2 : Map<Nat, Text> = Map.map(mapInstance, func(key, value) = natToText(key));
-let _ = check(m1, m2);
+let _ = check3(m1, m1i, m2);
 let _ = Map.all(mapInstance, func(k, v) = v == natToText(k));
 let _ = Map.any(mapInstance, func(k, v) = k >= 0);
 let _ = Map.toText(mapInstance, natToText, func t = t);
+let _ = Map.fromIter([(0, "0")].values(), natCompare);
 
 // pure Map module explicit type instantiation tests
 let _ = PureMap.all(pureMap, func(k, v) = v == natToText(k));

test/fail/lambdas-invariant.mo

@@ -0,0 +1,69 @@
+import Prim "mo:prim";
+
+module VarArray {
+  public func map<T, U>(_ : [var T], _ : (T) -> U) : [var U] = [var];
+};
+
+let va = [var 1, 2, 3];
+
+// Test that we can solve invariant U when the bound is an 'isolated' type, e.g.
+// Trying to solve:  Bool  <:  U  <:  Any
+// Should pick U = Bool, because Bool has no proper supertypes/subtypes (except Any and Non)
+let _ = VarArray.map(va, func x = x % 2 == 0); // Bool
+let _ = VarArray.map(va, func x = Prim.natToNat8(x) + 1); // NatX
+let _ = VarArray.map(va, func x = Prim.nat64ToInt64(Prim.natToNat64(x)) - 1); // IntX
+let _ = VarArray.map(va, func x = x % 2 == 0); // Float
+let _ = VarArray.map(va, func x = Prim.nat32ToChar(Prim.natToNat32(x))); // Char
+let _ = VarArray.map(va, func x = debug_show (x)); // Text
+let _ = VarArray.map(va, func x = Prim.encodeUtf8(debug_show (x))); // Blob
+let _ = VarArray.map(va, func x = Prim.principalOfBlob(Prim.encodeUtf8(debug_show (x)))); // Principal
+let _ = VarArray.map(va, func x = [Prim.natToNat16(x)]); // [Nat16]
+let _ = VarArray.map(va, func x = [var x]); // [var Nat]
+let _ = VarArray.map(va, func x = (Prim.intToInt32(x), debug_show (x))); // (Int32, Text)
+let _ = VarArray.map(va, func x = func(y : Nat8) : Bool = Prim.natToNat8(x) == y); // Nat8 -> Bool
+
+// Counter examples that should fail:
+func _m1() {
+  let _ = VarArray.map(va, func x = x); // Nat
+};
+func _m2() {
+  let _ = VarArray.map(va, func x = x : Int); // Int
+};
+func _m3() {
+  let _ = VarArray.map(va, func x = null); // Null
+};
+func _m4() {
+  let _ = VarArray.map(va, func x = ?Prim.natToNat8(x)); // ?Nat8
+};
+func _m5() {
+  let _ = VarArray.map(va, func x = [x]); // [Nat]
+};
+func _m6() {
+  let _ = VarArray.map(va, func x = { x }); // { x : Nat }
+};
+func _m7() {
+  let _ = VarArray.map(va, func x = #c(x)); // { #c : Nat }
+};
+
+// Termination check: should succeed
+type Bot = [Bot];
+let _ = VarArray.map(va, func x = [] : [Bot]); // [Bot]
+
+// Type variables: isolated when unbounded
+func tvUnbounded<Ok>(t : Ok) {
+  let _ = VarArray.map(va, func _ = t); // Ok
+};
+
+func tvBoundedToIsolated<Er <: Text>(t : Er) {
+  let _ = VarArray.map(va, func _ = t); // Er, should still fail because [var Er] =/= [var Text]
+};
+
+func tvBoundedToNat<Er <: Nat>(t : Er) {
+  let _ = VarArray.map(va, func _ = t); // Er, should fail
+};
+
+//SKIP comp
+//SKIP run
+//SKIP run-drun
+//SKIP run-ir
+//SKIP run-low

test/fail/ok/lambdas-invariant.tc.ok

@@ -0,0 +1,81 @@
+lambdas-invariant.mo:27.11-27.39: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  Nat  <:  U  <:  Any
+where
+  Nat  =/=  Any
+so that explicit type instantiation is required
+lambdas-invariant.mo:30.11-30.45: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  Int  <:  U  <:  Any
+where
+  Int  =/=  Any
+so that explicit type instantiation is required
+lambdas-invariant.mo:33.11-33.42: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  Null  <:  U  <:  Any
+where
+  Null  =/=  Any
+so that explicit type instantiation is required
+lambdas-invariant.mo:36.11-36.56: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  ?Nat8  <:  U  <:  Any
+where
+  ?Nat8  =/=  Any
+so that explicit type instantiation is required
+lambdas-invariant.mo:39.11-39.41: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  [Nat]  <:  U  <:  Any
+where
+  [Nat]  =/=  Any
+so that explicit type instantiation is required
+lambdas-invariant.mo:42.11-42.43: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  {x : Nat}  <:  U  <:  Any
+where
+  {x : Nat}  =/=  Any
+so that explicit type instantiation is required
+lambdas-invariant.mo:45.11-45.43: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  {#c : Nat}  <:  U  <:  Any
+where
+  {#c : Nat}  =/=  Any
+so that explicit type instantiation is required
+lambdas-invariant.mo:58.11-58.39: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  Er  <:  U  <:  Any
+where
+  Er  =/=  Any
+so that explicit type instantiation is required
+lambdas-invariant.mo:62.11-62.39: type error [M0098], cannot implicitly instantiate function of type
+  <T, U>([var T], T -> U) -> [var U]
+to argument of type
+  ([var Nat], Nat -> U)
+because implicit instantiation of type parameter U is under-constrained with
+  Er  <:  U  <:  Any
+where
+  Er  =/=  Any
+so that explicit type instantiation is required

test/fail/ok/lambdas-invariant.tc.ret.ok

@@ -0,0 +1 @@
+Return code 1