From b9c43570388bdf9e1e7de5edd6dc6dfdadf2017f Mon Sep 17 00:00:00 2001
From: Shunsuke Shibayama <sbym1346@gmail.com>
Date: Wed, 23 Aug 2023 12:12:55 +0900
Subject: [PATCH] fix: refinement subtyping

---
 crates/erg_compiler/context/compare.rs | 8 +++++++-
 tests/should_ok/slice.er               | 2 ++
 tests/test.rs                          | 5 +++++
 3 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 tests/should_ok/slice.er

diff --git a/crates/erg_compiler/context/compare.rs b/crates/erg_compiler/context/compare.rs
index 45377aef..50670c7e 100644
--- a/crates/erg_compiler/context/compare.rs
+++ b/crates/erg_compiler/context/compare.rs
@@ -630,7 +630,13 @@ impl Context {
                 let l = Type::Refinement(l.clone().into_refinement());
                 self.structural_supertype_of(&l, rhs)
             }
-            // ({I: Int | True} :> Int) == true, ({N: Nat | ...} :> Int) == false, ({I: Int | I >= 0} :> Int) == false
+            // {1, 2, 3} :> {1} or {2, 3} == true
+            (Refinement(_refine), Or(l, r)) => {
+                self.supertype_of(lhs, l) && self.supertype_of(lhs, r)
+            }
+            // ({I: Int | True} :> Int) == true
+            // {N: Nat | ...} :> Int) == false
+            // ({I: Int | I >= 0} :> Int) == false
             (Refinement(l), r) => {
                 if l.pred.mentions(&l.var) {
                     match l.pred.can_be_false() {
diff --git a/tests/should_ok/slice.er b/tests/should_ok/slice.er
new file mode 100644
index 00000000..16462ba1
--- /dev/null
+++ b/tests/should_ok/slice.er
@@ -0,0 +1,2 @@
+_ = [1, 2, 3][1] + 1
+_ = ["c"] + ["a", "b"][1..1000]
diff --git a/tests/test.rs b/tests/test.rs
index c94119e2..eab03b61 100644
--- a/tests/test.rs
+++ b/tests/test.rs
@@ -263,6 +263,11 @@ fn exec_self_type() -> Result<(), ()> {
     expect_success("tests/should_ok/self_type.er", 0)
 }
 
+#[test]
+fn exec_slice() -> Result<(), ()> {
+    expect_success("tests/should_ok/slice.er", 0)
+}
+
 #[test]
 fn exec_structural_example() -> Result<(), ()> {
     expect_success("examples/structural.er", 0)