diff options
| author | Alasdair | 2019-02-20 22:31:51 +0000 |
|---|---|---|
| committer | Alasdair | 2019-02-20 22:41:31 +0000 |
| commit | 7253269fb62712e7e8fd94d5d0264d5bed9e8406 (patch) | |
| tree | 9119cd23ce556f0b9b1ffcf719d11fa5dcdbbd77 /test | |
| parent | 09c8c3e212e5959461312d28240f2ae843a19e81 (diff) | |
Fix bug with missing satisfiablity check in subtyping
Thanks to Mark for finding this bug. Regression test is
complex_exist_sat in test/typecheck/pass/
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/complex_exist_sat.sail | 7 | ||||
| -rw-r--r-- | test/typecheck/pass/complex_exist_sat/v1.expect | 8 | ||||
| -rw-r--r-- | test/typecheck/pass/complex_exist_sat/v1.sail | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/complex_exist_sat/v2.expect | 8 | ||||
| -rw-r--r-- | test/typecheck/pass/complex_exist_sat/v2.sail | 3 |
5 files changed, 29 insertions, 0 deletions
diff --git a/test/typecheck/pass/complex_exist_sat.sail b/test/typecheck/pass/complex_exist_sat.sail new file mode 100644 index 00000000..65c3b6a9 --- /dev/null +++ b/test/typecheck/pass/complex_exist_sat.sail @@ -0,0 +1,7 @@ +val foo : int -> {'q, 'q in {0, 1}. atom(2 * 'q)} + +function foo(x) = 2 + +val bar : int -> {'q, 'q in {0, 1}. atom(2 * 'q)} + +function bar(x) = 0 diff --git a/test/typecheck/pass/complex_exist_sat/v1.expect b/test/typecheck/pass/complex_exist_sat/v1.expect new file mode 100644 index 00000000..b1937f47 --- /dev/null +++ b/test/typecheck/pass/complex_exist_sat/v1.expect @@ -0,0 +1,8 @@ +Type error: +[[96mcomplex_exist_sat/v1.sail[0m]:3:18-19 +3[96m |[0mfunction foo(x) = 3 + [91m |[0m [91m^[0m + [91m |[0m Tried performing type coercion from int(3) to {('q : Int), 'q in {0, 1}. int((2 * 'q))} on 3 + [91m |[0m Coercion failed because: + [91m |[0m Constraint 3 == (2 * 'ex1#) is not satisfiable + [91m |[0m diff --git a/test/typecheck/pass/complex_exist_sat/v1.sail b/test/typecheck/pass/complex_exist_sat/v1.sail new file mode 100644 index 00000000..f36f2dda --- /dev/null +++ b/test/typecheck/pass/complex_exist_sat/v1.sail @@ -0,0 +1,3 @@ +val foo : int -> {'q, 'q in {0, 1}. atom(2 * 'q)} + +function foo(x) = 3
\ No newline at end of file diff --git a/test/typecheck/pass/complex_exist_sat/v2.expect b/test/typecheck/pass/complex_exist_sat/v2.expect new file mode 100644 index 00000000..27af46d2 --- /dev/null +++ b/test/typecheck/pass/complex_exist_sat/v2.expect @@ -0,0 +1,8 @@ +Type error: +[[96mcomplex_exist_sat/v2.sail[0m]:3:18-19 +3[96m |[0mfunction foo(x) = 4 + [91m |[0m [91m^[0m + [91m |[0m Tried performing type coercion from int(4) to {('q : Int), 'q in {0, 1}. int((2 * 'q))} on 4 + [91m |[0m Coercion failed because: + [91m |[0m int(4) is not a subtype of {('q : Int), 'q in {0, 1}. int((2 * 'q))} + [91m |[0m diff --git a/test/typecheck/pass/complex_exist_sat/v2.sail b/test/typecheck/pass/complex_exist_sat/v2.sail new file mode 100644 index 00000000..e3e18e8c --- /dev/null +++ b/test/typecheck/pass/complex_exist_sat/v2.sail @@ -0,0 +1,3 @@ +val foo : int -> {'q, 'q in {0, 1}. atom(2 * 'q)} + +function foo(x) = 4
\ No newline at end of file |