Merge pull request #249 from nikomatsakis/chalk-248-test

add test for chalk#248

Author: nikomatsakis

src/test/slg.rs

@@ -1278,3 +1278,103 @@ fn negative_reorder() {
         }
     }
 }
+
+/// Test a tricky case for coinductive handling:
+///
+/// While proving C1, we try to prove C2, which recursively requires
+/// proving C1.  If you are naive, you will assume that C2 therefore
+/// holds -- but this is wrong, because C1 later fails when proving
+/// C3.
+#[test]
+fn coinductive_unsound1() {
+    test! {
+        program {
+            trait C1orC2 { }
+
+            #[auto]
+            trait C1 { }
+
+            #[auto]
+            trait C2 { }
+
+            #[auto]
+            trait C3 { }
+
+            forall<T> {
+                T: C1 if T: C2, T: C3
+            }
+
+            forall<T> {
+                T: C2 if T: C1
+            }
+
+            forall<T> {
+                T: C1orC2 if T: C1
+            }
+
+            forall<T> {
+                T: C1orC2 if T: C2
+            }
+        }
+
+        goal {
+            forall<X> { X: C1orC2 }
+        } first 10 with max 3 {
+            // FIXME(chalk#248) -- demonstrate bug in coinduction
+            r"[
+                Answer {
+                    subst: Canonical {
+                        value: ConstrainedSubst {
+                            subst: [],
+                            constraints: []
+                        }
+                        binders: []
+                    }
+                    delayed_literals: {}
+                }
+           ]"
+        }
+    }
+}
+
+/// The only difference between this test and `coinductive_unsound1`
+/// is the order of the final `forall` clauses.
+#[test]
+fn coinductive_unsound2() {
+    test! {
+        program {
+            trait C1orC2 { }
+
+            #[auto]
+            trait C1 { }
+
+            #[auto]
+            trait C2 { }
+
+            #[auto]
+            trait C3 { }
+
+            forall<T> {
+                T: C1 if T: C2, T: C3
+            }
+
+            forall<T> {
+                T: C2 if T: C1
+            }
+
+            forall<T> {
+                T: C1orC2 if T: C2
+            }
+
+            forall<T> {
+                T: C1orC2 if T: C1
+            }
+        }
+
+        goal {
+            forall<X> { X: C1orC2 }
+        } first 10 with max 3 {
+            r"[]"
+        }
+    }
+}