a-mir-formality icon indicating copy to clipboard operation
a-mir-formality copied to clipboard

OOM when evaluating `for<'b> &'a &'a (): 'b`

Open aliemjay opened this issue 3 years ago • 3 comments

The following test doesn't terminate. Same when when evaluating for<'b> &'b &'b (): 'a.

diff --git a/src/rust/test/wf--outlives.rkt b/src/rust/test/wf--outlives.rkt
index 0e11536..5d1623a 100644
--- a/src/rust/test/wf--outlives.rkt
+++ b/src/rust/test/wf--outlives.rkt
@@ -16,6 +16,9 @@
                                      (struct NoRef[(type T) (lifetime a)]
                                        where []
                                        { })
+                                     (struct NestedRef[(lifetime a) (lifetime b)]
+                                       where [(a : b)]
+                                       { })
                                      })] C)))
 
     ]
@@ -47,5 +50,16 @@
                 )
              )
             ))
+
+   (traced '()
+           (test-term-false
+            (rust:can-prove-where-clause-in-program
+             Rust/Program
+             (∀ [(lifetime a)]
+                where []
+                (for[(lifetime b)] ((NestedRef < a a >) : b))
+                )
+             )
+            ))
    )
   )

aliemjay avatar Jul 13 '22 09:07 aliemjay

This doesn't seem relevant to the current rust codebase anymore. I guess this can be closed?

shua avatar Jun 22 '24 15:06 shua

Given that this is a test case that caused a hang in the old impl, it may be useful to add it to the new one to make sure we don't encounter the same issue

lcnr avatar Jun 24 '24 19:06 lcnr

okay, I can take a look to see if it's represented in the current test cases

shua avatar Jun 25 '24 15:06 shua