From e919a1eba38d1af5192c33cd6e2d9d9f2f5606c9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Suzanne=20Dup=C3=A9ron?= Date: Tue, 17 Dec 2019 16:02:21 +0000 Subject: [PATCH] Fixes unsoundness in old typer (expected type for the expression as a whole was not checked for ascriptions) --- src/bin/expect_tests/typer_error_tests.ml | 4 ++-- src/passes/4-typer-old/typer.ml | 9 ++++++--- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/bin/expect_tests/typer_error_tests.ml b/src/bin/expect_tests/typer_error_tests.ml index 5a407316f..75cbe96a3 100644 --- a/src/bin/expect_tests/typer_error_tests.ml +++ b/src/bin/expect_tests/typer_error_tests.ml @@ -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]"} |} ] ; diff --git a/src/passes/4-typer-old/typer.ml b/src/passes/4-typer-old/typer.ml index 7792edcdb..7093f1d24 100644 --- a/src/passes/4-typer-old/typer.ml +++ b/src/passes/4-typer-old/typer.ml @@ -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 =