Rule out messages with abstract types in the type checker

src/check_ir.ml

@@ -121,7 +121,9 @@ let check_shared env at t =
   then check env at (T.is_serialized t)
     "message argument is not serialized:\n  %s" (T.string_of_typ_expand t)
   else check env at (T.sub t T.Shared)
-    "message argument is not sharable:\n  %s" (T.string_of_typ_expand t)
+    "message argument is not sharable:\n  %s" (T.string_of_typ_expand t);
+  check env at (T.is_concrete t)
+    "message argument is not concrete:\n  %s" (T.string_of_typ_expand t)
 
 let rec check_typ env typ : unit =
   match typ with

src/type.ml

@@ -380,6 +380,32 @@ let avoid cons t =
   if cons = ConSet.empty then t else
   avoid' cons t
 
+let is_concrete t =
+  let good_cons = ref ConSet.empty in (* break the cycles *)
+  let rec go = function
+    | (Prim _ | Var _ | Any | Non | Shared | Pre) -> true
+    | Con (c, ts) ->
+      if ConSet.mem c !good_cons
+      then true
+      else begin
+        match Con.kind c with
+        | Abs _ -> false
+        | Def (_,t) ->
+          good_cons := ConSet.add c !good_cons; go t
+        end
+      && List.for_all go ts
+    | Array t -> go t
+    | Tup ts -> List.for_all go ts
+    | Func (s, c, tbs, ts1, ts2) ->
+      List.for_all go ts1 &&
+      List.for_all go ts2
+    | Opt t -> go t
+    | Async t -> go t
+    | Obj (s, fs) -> List.for_all (fun f -> go f.typ) fs
+    | Mut t -> go t
+    | Serialized t -> go t
+  in go t
+
 
 (* Equivalence & Subtyping *)
 

src/type.mli

@@ -120,6 +120,7 @@ val promote : typ -> typ
 exception Unavoidable of con
 val avoid : ConSet.t -> typ -> typ (* raise Unavoidable *)
 
+val is_concrete : typ -> bool
 
 (* Equivalence and Subtyping *)
 

src/typing.ml

@@ -163,17 +163,25 @@ and check_typ' env typ : T.typ =
     let ts2 = List.map (check_typ env') typs2 in
     let c = match typs2 with [{it = AsyncT _; _}] -> T.Promises | _ -> T.Returns in
     if sort.it = T.Sharable then begin
+      if not (binds = []) then
+        error env typ.at "shared functions cannot be polymorphic";
       let t1 = T.seq ts1 in
       if not (T.sub t1 T.Shared) then
         error env typ1.at "shared function has non-shared parameter type\n  %s"
           (T.string_of_typ_expand t1);
+      if not (T.is_concrete t1) then
+        error env typ1.at "shared function parameter contains abstract type\n  %s"
+          (T.string_of_typ_expand t1);
       (match ts2 with
       | [] -> ()
       | [T.Async t2] ->
         if not (T.sub t2 T.Shared) then
-          error env typ1.at "shared function has non-shared result type\n  %s"
+          error env typ2.at "shared function has non-shared result type\n  %s"
+            (T.string_of_typ_expand t2);
+        if not (T.is_concrete t2) then
+          error env typ2.at "shared function result contains abstract type\n  %s"
             (T.string_of_typ_expand t2);
-      | _ -> error env typ1.at "shared function has non-async result type\n  %s"
+      | _ -> error env typ2.at "shared function has non-async result type\n  %s"
           (T.string_of_typ_expand (T.seq ts2))
       )
     end;
@@ -467,15 +475,23 @@ and infer_exp'' env exp : T.typ =
         {env' with labs = T.Env.empty; rets = Some t2; async = false} in
       check_exp (adjoin_vals env'' ve) t2 exp;
       if sort.it = T.Sharable then begin
+        if not (typ_binds = []) then
+          error env exp.at "shared functions cannot be polymorphic";
         if not (T.sub t1 T.Shared) then
           error env pat.at "shared function has non-shared parameter type\n  %s"
             (T.string_of_typ_expand t1);
+        if not (T.is_concrete t1) then
+          error env pat.at "shared function parameter contains abstract type\n  %s"
+            (T.string_of_typ_expand t1);
         begin match t2 with
         | T.Tup [] -> ()
         | T.Async t2 ->
           if not (T.sub t2 T.Shared) then
             error env typ.at "shared function has non-shared result type\n  %s"
               (T.string_of_typ_expand t2);
+          if not (T.is_concrete t2) then
+            error env typ.at "shared function result contains abstract type\n  %s"
+              (T.string_of_typ_expand t2);
           if not (isAsyncE exp) then
             error env exp.at "shared function with async type has non-async body"
         | _ -> error env typ.at "shared function has non-async result type\n  %s"

test/fail/abstract-msgs.as

@@ -0,0 +1,21 @@
+// check that types with non-concrete types in messages are rejected
+{ let x : ?(shared <A <: Shared>A -> ()) = null; };
+{ let x : ?(shared <A <: Shared>() -> A) = null; };
+{ let x : ?(<A <: Shared>(shared A -> ()) -> ()) = null; };
+{ let x : ?(<A <: Shared>(shared () -> async A) -> ()) = null; };
+
+// Type aliases can have message arguments with type variables,
+// as long as they are instantiated with concrete types
+// So this whould be fine:
+{ type X<B> = shared B -> (); let x : ?(X<Int>) = null; };
+
+// But this not
+{ type X<B> = shared B -> (); let x : ?(<A <: Shared>X<A> -> ()) = null; };
+
+// check that functions with non-concrete types in messages are rejected
+{ shared func foo<A <: Shared>( x : A ) : () = (); };
+{ shared func foo<A <: Shared>() : ?A = null; };
+{ func foo<A <: Shared>() : () = {
+  { shared func bar( x : A ) : () = (); };
+  { shared func bar() : ?A = null; };
+}};

test/fail/asyncret2.as

@@ -1 +1 @@
-func call3<B <: Shared>(f : shared () -> async B) : async B { f(); };
+func call3(f : shared () -> async Int) : async Int { f(); };

test/fail/asyncret3.as

@@ -1 +1 @@
-shared func call4<B <: Shared>(f : shared () -> async B) : async B = f();
+shared func call4(f : shared () -> async Int) : async Int = f();

test/fail/ok/abstract-msgs.tc.ok

@@ -0,0 +1,12 @@
+abstract-msgs.as:2.13-2.40: type error, shared functions cannot be polymorphic
+abstract-msgs.as:3.13-3.40: type error, shared functions cannot be polymorphic
+abstract-msgs.as:4.34-4.35: type error, shared function parameter contains abstract type
+  A/2
+abstract-msgs.as:5.40-5.47: type error, shared function result contains abstract type
+  A/3
+abstract-msgs.as:8.48-8.50: type error, shared functions cannot be polymorphic
+abstract-msgs.as:9.41-9.45: type error, shared functions cannot be polymorphic
+abstract-msgs.as:11.22-11.27: type error, shared function parameter contains abstract type
+  A/9
+abstract-msgs.as:12.25-12.27: type error, shared function has non-async result type
+  ?A/9

test/fail/ok/asyncret1.tc.ok

@@ -1,2 +1,2 @@
-asyncret1.as:1.36-1.38: type error, shared function has non-async result type
+asyncret1.as:1.42-1.43: type error, shared function has non-async result type
   C

test/fail/ok/asyncret2.tc.ok

@@ -1,4 +1,4 @@
-asyncret2.as:1.63-1.66: type error, expression of type
-  async B/1
+asyncret2.as:1.54-1.57: type error, expression of type
+  async Int
 cannot produce expected type
-  B/1
+  Int

test/fail/ok/asyncret3.tc.ok

@@ -1 +1 @@
-asyncret3.as:1.70-1.73: type error, shared function with async type has non-async body
+asyncret3.as:1.61-1.64: type error, shared function with async type has non-async body

test/run-dfinity/nary-async.as

@@ -121,6 +121,7 @@ let _ : async (Int,)  = async {
 */
 
 
+/* Disabled: No generic messages are supported
 func Generic<T <: Shared>(t:Text, x:T,eq:(T,T)->Bool)  {
 
 shared func fu_u(x:T) : async T {
@@ -143,3 +144,4 @@ Generic<()>("<()>\n", (), func eq(i:(),j:()) : Bool = true);
 Generic<(Int,Bool)>("<(Int,Bool)>\n", (1,true),
 	            func eq((i,b):(Int,Bool),
 		            (j,c):(Int,Bool)) : Bool = i == j and b == c);
+*/

test/run-dfinity/ok/nary-async.dvm-run.ok

@@ -7,6 +7,4 @@ Top-level code done.
 0_1
 0_2
 0_3
-!!<Int>
-<()>
-<(Int,Bool)>
+!!

test/run-dfinity/ok/nary-async.run-ir.ok

@@ -6,6 +6,4 @@
 0_1
 0_2
 0_3
-!!<Int>
-<()>
-<(Int,Bool)>
+!!

test/run-dfinity/ok/nary-async.run-low.ok

@@ -6,6 +6,4 @@
 0_1
 0_2
 0_3
-!!<Int>
-<()>
-<(Int,Bool)>
+!!

test/run-dfinity/ok/nary-async.run.ok

@@ -6,6 +6,4 @@
 0_1
 0_2
 0_3
-!!<Int>
-<()>
-<(Int,Bool)>
+!!