Skip to content

Commit

Permalink
turn overflow into error (WIP)
Browse files Browse the repository at this point in the history
  • Loading branch information
@crusso
crusso committed Dec 4, 2024
1 parent 6c6d38f commit 411b818
Show file tree
Hide file tree
Showing 3 changed files with 46 additions and 42 deletions.
79 changes: 44 additions & 35 deletions src/mo_frontend/typing.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -333,6 +333,15 @@ let disjoint_union env at code fmt env1 env2 =
with T.Env.Clash k -> error env at code fmt k


let sub env at t1 t2 =
try T.sub t1 t2 with _ -> error env at "M0XXX" "can't determine subtyping?"

let eq env at t1 t2 =
try T.eq t1 t2 with _ -> error env at "M0XXX" "can't determine type equality?"

let eq_kind env at k1 k2 =
try T.eq_kind k1 k2 with _ -> error env at "M0XXX" "can't determine type constructor equality?"

(* Coverage *)

let coverage' warnOrError category env f x t at =
Expand Down Expand Up @@ -562,7 +571,7 @@ let associated_region env typ at =
| Some r ->
Printf.sprintf "\n scope %s is %s" (T.string_of_typ_expand typ) (string_of_region r);
| None ->
if T.eq typ (T.Con(C.top_cap,[])) then
if eq env at typ (T.Con(C.top_cap,[])) then
Printf.sprintf "\n scope %s is the global scope" (T.string_of_typ_expand typ)
else ""

Expand Down Expand Up @@ -759,7 +768,7 @@ and check_typ' env typ : T.typ =
error env typ2.at "M0168"
"cannot compute intersection of types containing recursive or forward references to other type definitions"
in
if not env.pre && T.sub t T.Non && not (T.sub t1 T.Non || T.sub t2 T.Non) then
if not env.pre && sub env typ.at t T.Non && not (sub env typ1.at t1 T.Non || sub env typ2.at t2 T.Non) then
warn env typ.at "M0166"
"this intersection results in type%a\nbecause operand types are inconsistent,\nleft operand is%a\nright operand is%a"
display_typ t
Expand All @@ -773,7 +782,7 @@ and check_typ' env typ : T.typ =
error env typ2.at "M0168"
"cannot compute union of types containing recursive or forward references to other type definitions"
in
if not env.pre && T.sub T.Any t && not (T.sub T.Any t1 || T.sub T.Any t2) then
if not env.pre && sub env typ.at T.Any t && not (sub env typ1.at T.Any t1 || sub env typ2.at T.Any t2) then
warn env typ.at "M0167"
"this union results in type%a\nbecause operand types are inconsistent,\nleft operand is%a\nright operand is%a"
display_typ t
Expand Down Expand Up @@ -862,7 +871,7 @@ and check_typ_binds env typ_binds : T.con list * T.bind list * Scope.typ_env * S
List.iter2 (fun c k ->
match Cons.kind c with
| T.Abs (_, T.Pre) -> T.set_kind c k
| k' -> assert (T.eq_kind k k')
| k' -> assert (eq_kind env Source.no_region k k')
) cs ks;
let env' = add_typs env xs cs in
let _ = List.map (fun typ_bind -> check_typ env' typ_bind.it.bound) typ_binds in
Expand Down Expand Up @@ -891,7 +900,7 @@ and check_typ_bounds env (tbs : T.bind list) (ts : T.typ list) ats at =
| tb::tbs', t::ts', at'::ats' ->
if not env.pre then
let u = T.open_ ts tb.T.bound in
if not (T.sub t u) then
if not (sub env at' t u) then
local_error env at' "M0046"
"type argument%a\ndoes not match parameter bound%a"
display_typ_expand t
Expand Down Expand Up @@ -1132,7 +1141,7 @@ let check_lit env t lit at suggest =
lit := BlobLit s
| t, _ ->
let t' = T.Prim (infer_lit env lit at) in
if not (T.sub t' t) then
if not (sub env at t' t) then
error env at "M0050"
"literal of type%a\ndoes not have expected type%a%s"
display_typ t'
Expand Down Expand Up @@ -1254,7 +1263,7 @@ and infer_exp'' env exp : T.typ =
assert (!ot = Type.Pre);
if not (Operator.has_binop op t) then
error_bin_op env exp.at t1 t2
else if op = Operator.SubOp && T.eq t T.nat then
else if op = Operator.SubOp && eq env exp.at t T.nat then
warn env exp.at "M0155" "operator may trap for inferred type%a"
display_typ_expand t;
ot := t
Expand All @@ -1267,8 +1276,8 @@ and infer_exp'' env exp : T.typ =
let t = Operator.type_relop op (T.lub (T.promote t1) (T.promote t2)) in
if not (Operator.has_relop op t) then
error_bin_op env exp.at t1 t2;
if not (T.eq t t1 || T.eq t t2) && not (T.sub T.nat t1 && T.sub T.nat t2) then
if T.eq t1 t2 then
if not (eq env exp1.at t t1 || eq env exp2.at t t2) && not (sub env exp1.at T.nat t1 && sub env exp2.at T.nat t2) then
if eq env exp.at t1 t2 then
warn env exp.at "M0061"
"comparing abstract type%a\nto itself at supertype%a"
display_typ_expand t1
Expand Down Expand Up @@ -1362,7 +1371,7 @@ and infer_exp'' env exp : T.typ =
begin match env.pre, typ_opt with
| false, (_, Some typ) ->
let t' = check_typ env' typ in
if not (T.sub t t') then
if not (sub env exp.at t t') then
local_error env exp.at "M0192"
"body of type%a\ndoes not match expected type%a"
display_typ_expand t
Expand Down Expand Up @@ -1396,11 +1405,11 @@ and infer_exp'' env exp : T.typ =
let ambiguous_fields ft1 ft2 =
homonymous_fields ft1 ft2 &&
(* allow equivalent type fields *)
T.(match ft1.typ, ft2.typ with
match ft1.T.typ, ft2.T.typ with
(* homonymous type fields are ambiguous when unequal *)
| Typ c1, Typ c2 -> not (T.eq ft1.typ ft2.typ)
| T.Typ c1, T.Typ c2 -> not (eq env exp.at ft1.T.typ ft2.T.typ)
(* homonymous value fields are always ambiguous *)
| _ -> true)
| _ -> true
in

(* field disjointness of stripped bases *)
Expand Down Expand Up @@ -1643,7 +1652,7 @@ and infer_exp'' env exp : T.typ =
let _, tfs = T.as_obj_sub ["next"] t1 in
let t = T.lookup_val_field "next" tfs in
let t1, t2 = T.as_mono_func_sub t in
if not (T.sub T.unit t1) then raise (Invalid_argument "");
if not (sub env exp1.at T.unit t1) then raise (Invalid_argument "");
let t2' = T.as_opt_sub t2 in
let ve = check_pat_exhaustive warn env t2' pat in
check_exp_strong (adjoin_vals env ve) T.unit exp2
Expand Down Expand Up @@ -1715,7 +1724,7 @@ and infer_exp'' env exp : T.typ =
let t1 = infer_exp_promote env exp1 in
(try
let (t2, t3) = T.as_async_sub s t0 t1 in
if not (T.eq t0 t2) then begin
if not (eq env exp.at t0 t2) then begin
local_error env exp1.at "M0087"
"ill-scoped await: expected async type from current scope %s, found async type from other scope %s%s%s"
(T.string_of_typ_expand t0)
Expand Down Expand Up @@ -1748,7 +1757,7 @@ and infer_exp'' env exp : T.typ =
| IgnoreE exp1 ->
if not env.pre then begin
check_exp_strong env T.Any exp1;
if T.sub exp1.note.note_typ T.unit then
if sub env exp1.at exp1.note.note_typ T.unit then
warn env exp.at "M0089" "redundant ignore, operand already has type ()"
end;
T.unit
Expand Down Expand Up @@ -1812,14 +1821,14 @@ and check_exp' env0 t exp : T.typ =
ot := t;
check_exp env t exp1;
check_exp env t exp2;
if env.weak && op = Operator.SubOp && T.eq t T.nat then
if env.weak && op = Operator.SubOp && eq env exp.at t T.nat then
warn env exp.at "M0155" "operator may trap for inferred type%a"
display_typ_expand t;
t
| ToCandidE exps, _ ->
if not env.pre then begin
let ts = List.map (infer_exp env) exps in
if not (T.sub (T.Prim T.Blob) t) then
if not (sub env exp.at (T.Prim T.Blob) t) then
error env exp.at "M0172" "to_candid produces a Blob that is not a subtype of%a"
display_typ_expand t;
if not (T.shared (T.seq ts)) then
Expand Down Expand Up @@ -1881,7 +1890,7 @@ and check_exp' env0 t exp : T.typ =
else
"Use keyword 'async*' (not 'async') to produce the expected type.")
end;
if not (T.eq t1 t1') then begin
if not (eq env exp.at t1 t1') then begin
local_error env exp.at "M0092"
"async at scope%a\ncannot produce expected scope%a%s%s"
display_typ_expand t1
Expand Down Expand Up @@ -1942,7 +1951,7 @@ and check_exp' env0 t exp : T.typ =
"%sshared function does not match expected %sshared function type"
(if sort = T.Local then "non-" else "")
(if s = T.Local then "non-" else "");
if not (T.sub t2 codom) then
if not (sub env Source.no_region t2 codom) then
error env exp.at "M0095"
"function return type%a\ndoes not match expected return type%a"
display_typ_expand t2
Expand All @@ -1957,7 +1966,7 @@ and check_exp' env0 t exp : T.typ =
t
| CallE (exp1, inst, exp2), _ ->
let t' = infer_call env exp1 inst exp2 exp.at (Some t) in
if not (T.sub t' t) then
if not (sub env exp1.at t' t) then
local_error env0 exp.at "M0096"
"expression of type%a\ncannot produce expected type%a"
display_typ_expand t'
Expand All @@ -1969,7 +1978,7 @@ and check_exp' env0 t exp : T.typ =
t
| _ ->
let t' = infer_exp env0 exp in
if not (T.sub t' t) then
if not (sub env exp.at t' t) then
begin
local_error env0 exp.at "M0096"
"expression of type%a\ncannot produce expected type%a%s"
Expand Down Expand Up @@ -2243,22 +2252,22 @@ and check_pat_aux' env t pat val_kind : Scope.val_env =
T.Env.singleton id.it (t, id.at, val_kind)
| LitP lit ->
if not env.pre then begin
let t' = if T.eq t T.nat then T.int else t in (* account for Nat <: Int *)
let t' = if eq env pat.at t T.nat then T.int else t in (* account for Nat <: Int *)
if T.opaque t' then
error env pat.at "M0110" "literal pattern cannot consume expected type%a"
display_typ_expand t;
if T.sub t' T.Non
if sub env pat.at t' T.Non
then ignore (infer_lit env lit pat.at)
else check_lit env t' lit pat.at false
end;
T.Env.empty
| SignP (op, lit) ->
if not env.pre then begin
let t' = if T.eq t T.nat then T.int else t in (* account for Nat <: Int *)
let t' = if eq env pat.at t T.nat then T.int else t in (* account for Nat <: Int *)
if not (Operator.has_unop op (T.promote t)) then
error env pat.at "M0111" "operator pattern cannot consume expected type%a"
display_typ_expand t;
if T.sub t' T.Non
if sub env pat.at t' T.Non
then ignore (infer_lit env lit pat.at)
else check_lit env t' lit pat.at false
end;
Expand Down Expand Up @@ -2308,7 +2317,7 @@ and check_pat_aux' env t pat val_kind : Scope.val_env =
T.Env.merge (fun _ -> Lib.Option.map2 merge_entries) ve1 ve2
| AnnotP (pat1, typ) ->
let t' = check_typ env typ in
if not (T.sub t t') then
if not (sub env pat.at t t') then
error env pat.at "M0117"
"pattern of type%a\ncannot consume expected type%a"
display_typ_expand t'
Expand Down Expand Up @@ -2544,7 +2553,7 @@ and check_system_fields env sort scope tfs dec_fields =
if vis = System then
begin
let (t1, _, _) = T.Env.find id.it scope.Scope.val_env in
if not (T.sub t1 t) then
if not (sub env id.at t1 t) then
local_error env df.at "M0127" "system function %s is declared with type%a\ninstead of expected type%a" id.it
display_typ t1
display_typ t
Expand Down Expand Up @@ -2704,7 +2713,7 @@ and infer_dec env dec : T.typ =
warn env dec.at "M0135"
"actor classes with non non-async return types are deprecated; please declare the return type as 'async ...'";
let t'' = check_typ env'' typ in
if not (T.sub t' t'') then
if not (sub env dec.at t' t'') then
local_error env dec.at "M0134"
"class body of type%a\ndoes not match expected type%a"
display_typ_expand t'
Expand Down Expand Up @@ -2732,7 +2741,7 @@ and check_block env t decs at : Scope.t =
and check_block_exps env t decs at =
match decs with
| [] ->
if not (T.sub T.unit t) then
if not (sub env at T.unit t) then
local_error env at "M0136" "empty block cannot produce expected type%a"
display_typ_expand t
| [dec] ->
Expand All @@ -2748,7 +2757,7 @@ and check_dec env t dec =
dec.note <- exp.note
| _ ->
let t' = infer_dec env dec in
if not (T.eq t T.unit || T.sub t' t) then
if not (eq env dec.at t T.unit || sub env dec.at t' t) then
local_error env dec.at "M0096"
"expression of type%a\ncannot produce expected type%a"
display_typ_expand t'
Expand Down Expand Up @@ -2910,7 +2919,7 @@ and infer_dec_typdecs env dec : Scope.t =
let c = T.Env.find id.it env.typs in
Scope.{ empty with
typ_env = T.Env.singleton id.it c;
con_env = infer_id_typdecs id c k;
con_env = infer_id_typdecs env dec.at id c k;
}
| ClassD (shared_pat, id, binds, pat, _typ_opt, obj_sort, self_id, dec_fields) ->
let c = T.Env.find id.it env.typs in
Expand All @@ -2933,14 +2942,14 @@ and infer_dec_typdecs env dec : Scope.t =
check_closed env id k dec.at;
Scope.{ empty with
typ_env = T.Env.singleton id.it c;
con_env = infer_id_typdecs id c k;
con_env = infer_id_typdecs env dec.at id c k;
}

and infer_id_typdecs id c k : Scope.con_env =
and infer_id_typdecs env at id c k : Scope.con_env =
assert (match k with T.Abs (_, T.Pre) -> false | _ -> true);
(match Cons.kind c with
| T.Abs (_, T.Pre) -> T.set_kind c k; id.note <- Some c
| k' -> assert (T.eq_kind k' k) (* may diverge on expansive types *)
| k' -> assert (eq_kind env at k' k) (* may diverge on expansive types *)
);
T.ConSet.singleton c

Expand Down
7 changes: 1 addition & 6 deletions test/fail/ok/polyrec.tc.ok
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1 @@
OOPS! You've triggered a compiler bug.
Please report this at https://github.com/dfinity/motoko/issues/new with the following details:

Motoko (source XXX)

Fatal error: exception Failure("subtyping: recursion too deep")
polyrec.mo:4.10-11.4: type error [M0XXX], can't determine type constructor equality?
2 changes: 1 addition & 1 deletion test/fail/ok/polyrec.tc.ret.ok
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
Return code 2
Return code 1

0 comments on commit 411b818

Please sign in to comment.