balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fixes unsoundness in old typer (expected type for the expression as a whole was not checked for ascriptions)

Browse Source
This commit is contained in:
Suzanne Dupéron 2019-12-17 16:02:21 +00:00
parent 7ea6aadc2c
commit e919a1eba3
2 changed files with 8 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/bin/expect_tests/typer_error_tests.ml
View File

@ -7,5 +7,5 @@ let%expect_test _ =
run_ligo_bad [ "compile-contract" ; "../../test/contracts/error_typer_2.mligo" ; "foo" ] ;
[%expect {| ligo: in file "error_typer_2.mligo", line 3, characters 24-39. different type constructors: Expected these two n-ary type constructors to be the same, but they're different {"a":"(TO_list(string))","b":"(TO_option(int))"} |} ] ;
(* run_ligo_bad [ "compile-contract" ; "../../test/contracts/error_typer_3.mligo" ; "foo" ] ;
* [%expect …some type error… ] ; *)
run_ligo_bad [ "compile-contract" ; "../../test/contracts/error_typer_3.mligo" ; "foo" ] ;
[%expect {| ligo: in file "error_typer_3.mligo", line 3, characters 34-53. tuples have different sizes: Expected these two types to be the same, but they're different (both are tuples, but with a different number of arguments) {"a":"tuple[int , string , bool]","b":"tuple[int , string]"} |} ] ;

9
src/passes/4-typer-old/typer.ml
View File

@ -464,8 +464,6 @@ and type_expression' : environment -> ?tv_opt:O.type_value -> I.expression -> O.
| None -> ok ()
| Some tv' -> O.assert_type_value_eq (tv' , ae.type_annotation) in
ok(ae)
(* Sum *)
| E_constructor (c, expr) ->
let%bind (c_tv, sum_tv) =
@ -793,7 +791,12 @@ and type_expression' : environment -> ?tv_opt:O.type_value -> I.expression -> O.
(Some tv)
(Some expr'.type_annotation)
(internal_assertion_failure "merge_annotations (Some ...) (Some ...) failed") in
ok {expr' with type_annotation}
(* check type annotation of the expression as a whole (e.g. let x : t = (v : t') ) *)
let%bind () =
match tv_opt with
| None -> ok ()
| Some tv' -> O.assert_type_value_eq (tv' , type_annotation) in
ok @@ {expr' with type_annotation}
and type_constant (name:I.constant) (lst:O.type_value list) (tv_opt:O.type_value option) : (O.constant * O.type_value) result =