Skip to content

Commit

Permalink
refine static checks on migration function:
Browse files Browse the repository at this point in the history
  • Loading branch information
crusso committed Jan 8, 2025
1 parent 20be12c commit 1906f91
Show file tree
Hide file tree
Showing 4 changed files with 47 additions and 5 deletions.
11 changes: 6 additions & 5 deletions src/mo_frontend/typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -2593,7 +2593,7 @@ and check_migration env exp_opt =
| None -> ([],[])
| Some exp ->
let check_fields desc typ =
match T.promote typ with
match typ with
| T.Obj(T.Object, tfs) ->
if not (T.stable typ) then
local_error env exp.at "M0131"
Expand All @@ -2611,13 +2611,14 @@ and check_migration env exp_opt =
let typ = infer_exp env exp in
try
let sort, tbs, t_dom, t_rng = T.as_func_sub T.Local 0 typ in
(check_fields "consumes" t_dom,
check_fields "produces" t_rng)
if sort <> T.Local || tbs <> [] then raise (Invalid_argument "");
(check_fields "consumes" (T.normalize t_dom),
check_fields "produces" (T.promote t_rng))
with Invalid_argument _ ->
local_error env exp.at "M0097"
"expected function type, but expression produces type%a"
"expected non-generic, local function type, but migration expression produces type%a"
display_typ_expand typ;
([],[])
([], [])


and check_stab env sort exp_opt scope dec_fields =
Expand Down
24 changes: 24 additions & 0 deletions test/fail/migration-bad.mo
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
import Prim "mo:prim";

// test migration function restrictions

actor [()] a = { // reject, not a function
};

actor [func <T>(x:T) : T {x}] b = { // reject, a generic function
};

actor [func () : {} {{}}] c = { // reject, domain is not a record
};

actor [func ({}) : () {}] d = { // reject, co-domain is not a record
};


actor [func ({f:()->()}) : () {}] e = { // reject domain is unstable
};

actor [func () : {f:()->()}{ {f = func(){}} }]
f = { // reject, co-domain is unstable
stable let f : Any = ()
};
16 changes: 16 additions & 0 deletions test/fail/ok/migration-bad.tc.ok
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
migration-bad.mo:5.8-5.10: type error [M0097], expected non-generic, local function type, but migration expression produces type
()
migration-bad.mo:8.8-8.29: type error [M0097], expected non-generic, local function type, but migration expression produces type
<T>T -> T
migration-bad.mo:11.8-11.25: type error [M0093], expected object type, but migration expression consumes non-object type
()
migration-bad.mo:14.8-14.25: type error [M0093], expected object type, but migration expression produces non-object type
()
migration-bad.mo:18.8-18.33: type error [M0093], expected object type, but migration expression produces non-object type
()
migration-bad.mo:18.8-18.33: type error [M0131], expected stable type, but migration expression consumes non-stable type
{f : () -> ()}
migration-bad.mo:21.8-21.46: type error [M0131], expected stable type, but migration expression produces non-stable type
{f : () -> ()}
migration-bad.mo:21.8-21.46: type error [M0093], expected object type, but migration expression consumes non-object type
()
1 change: 1 addition & 0 deletions test/fail/ok/migration-bad.tc.ret.ok
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Return code 1

0 comments on commit 1906f91

Please sign in to comment.