Error "Invalid name shadowing. Identifier 't' is already bound" when nesting parallelReduce()

[mrweiner]

Issue Overview

I'm experiencing an awkward error when nesting parallelReduce(). I'm not sure whether this is expected behavior or a bug. Specifically I'm encountering Example 4, but found the same error for a different situation in Example 3.

Example 1 - passes

A non-nested PR that uses participant A in multiple cases passes verification: https://github.com/reach-sh/reach-lang/blob/master/examples/multiple-pr-case/index.rsh

Example 2 - passes

When nested PRs use different participants in their cases, the code passes verification.

'reach 0.1';

const Common = ({
  doCase: Fun([UInt], Bool) });

export const main = Reach.App(
  {}, [Participant('A', {...Common}), Participant('B', {...Common})], (A, B) => {
    A.publish()
      .pay(1);
    commit();

    B.publish();
 
    const keepGoing =
      parallelReduce(true)
        .invariant(balance() == 1)
        .while(keepGoing)
        .case(
          A,
          (() => ({ when: true })),
          ((_) => {

            const keepGoingB = 
              parallelReduce(true)
                .invariant(balance() == 1)
                .while(keepGoingB)
                .case( 
                  B,
                  (() => ({ when: declassify(interact.doCase(1)) })),
                  () => { return true; }) 
                .timeout(1000, () => {
                  Anybody.publish();
                  return false;
                });
  
            return false; 

          })
        )
        .timeout(false);

    transfer(1).to(B);
    commit();
    exit();
  }
);

Example 3 - fails

When a case on the outer PR uses the same participant as a case on the inner PR, an error is thrown: reachc: error: ./index.rsh:24:29:const: Invalid name shadowing. Identifier 't' is already bound at ./index.rsh:15:21:id. It cannot be bound again at ./index.rsh:24:29:id

'reach 0.1';

const Common = ({
  doCase: Fun([UInt], Bool) });

export const main = Reach.App(
  {}, [Participant('A', {...Common}), Participant('B', {...Common})], (A, B) => {
    A.publish()
      .pay(1);
    commit();

    B.publish();
 
    const keepGoing =
      parallelReduce(true)
        .invariant(balance() == 1)
        .while(keepGoing)
        .case(
          A,
          (() => ({ when: true })),
          ((_) => {

            const keepGoingB = 
              parallelReduce(true)
                .invariant(balance() == 1)
                .while(keepGoingB)
                .case( 
                  A,
                  (() => ({ when: declassify(interact.doCase(1)) })),
                  () => { return true; }) 
                .timeout(1000, () => {
                  Anybody.publish();
                  return false;
                });
  
            return false; 

          })
        )
        .timeout(false);

    transfer(1).to(B);
    commit();
    exit();
  }
);

Example 4 - fails

When a case on the outer PR uses participant A, and the inner PR uses participant B in multiple cases, an error is thrown: reachc: error: ./index.rsh:24:29:application: Invalid name shadowing. Identifier 't' is already bound at ./index.rsh:15:21:id. It cannot be bound again at ./index.rsh:24:29:id. Given that examples 1 and 2 both pass verification, it seems like this should pass as well, yet it does not.

'reach 0.1';

const Common = ({
  doCase: Fun([UInt], Bool) });

export const main = Reach.App(
  {}, [Participant('A', {...Common}), Participant('B', {...Common})], (A, B) => {
    A.publish()
      .pay(1);
    commit();

    B.publish();
 
    const keepGoing =
      parallelReduce(true)
        .invariant(balance() == 1)
        .while(keepGoing)
        .case(
          A,
          (() => ({ when: true })),
          ((_) => {

            const keepGoingB = 
              parallelReduce(true)
                .invariant(balance() == 1)
                .while(keepGoingB)
                .case( 
                  B,
                  (() => ({ when: declassify(interact.doCase(1)) })),
                  () => { return true; }) 
                .case( 
                  B,
                  (() => ({ when: declassify(interact.doCase(2)) })),
                  () => { return true; }) 
                .timeout(1000, () => {
                  Anybody.publish();
                  return false;
                });
  
            return false; 

          })
        )
        .timeout(false);

    transfer(1).to(B);
    commit();
    exit(); 
  }
);

[jeapostrophe]

@chrisnevers Look at this too please, an internal macro variable is being exposed

[chrisnevers]

@mrweiner Thanks for opening this issue; it has been fixed in this recent commit.

[mrweiner]

Awesome, thanks Chris!