Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
aliemjay opened this issue Jul 13, 2022 · 3 comments
Open

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

aliemjay opened this issue Jul 13, 2022 · 3 comments

Comments

@aliemjay
Copy link
Member

aliemjay commented Jul 13, 2022

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))
+                )
+             )
+            ))
    )
   )
@shua
Copy link
Contributor

shua commented Jun 22, 2024

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

@lcnr
Copy link
Contributor

lcnr commented Jun 24, 2024

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

@shua
Copy link
Contributor

shua commented Jun 25, 2024

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

shua added a commit to shua/a-mir-formality that referenced this issue Jun 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants