brendanzab / moniker

Automagical variable binding library for Rust
Apache License 2.0
68 stars 7 forks source link

Bug with nested letrecs? #84

Open gmorpheme opened 3 years ago

gmorpheme commented 3 years ago

I think there may be a bug in the handling of nested recursive bindings with embeds... i.e. nested letrecs as in the test I've added here:

https://github.com/curvelogic/moniker/commit/39d7c569a614ef9dca0707cc0360e618e6a1fddd

(I may be misunderstanding or there may be a way to combine Nest<> or something else to fix this but I'm not seeing it at present.)

When opening the pattern, state depth is not incremented when entering the second scope's pattern so bound variables which actually identify the nested letrec are being looked up in the outer letrec. (Which fails in the test above because there are fewer bindings in the outer letrec than the index of the binding being sought.)

Culprit seems to be a missing .incr() on line 142 of scope.rs. Depth is incremented for unsafe_body but not for unsafe_pattern. I'm not clear in my head yet whether the obvious change of adding the .incr() for the pattern too (like this) is safe or correct but it doesn't seem to break any tests at least.

gmorpheme commented 3 years ago

The problem example, to save a couple of clicks:

    // expr =
    //      let test = let id = b
    //                      b = \x -> x
    //                  in id
    //      in
    //          test
gmorpheme commented 3 years ago

Speculative fix was indeed unsafe (counterexample), if for no other reason than it didn't make the compensating change in close_pattern.