Partial evaluator generates bad code when interacting with holes

[Z-snails]

trafficstars

While working on a fix for the partial evaluator, I found another bug with the partial evaulator :rofl:.

-- test.idr

COUNT : Nat

%spec count
test : (count : Nat) -> IO ()
test Z = putStrLn "Done"
test (S k) = putStrLn "\{show $ S k} to go" >> test k

main : IO ()
main = test COUNT

Steps to Reproduce

Compile the file

Expected Behavior

Warning about compiling a hole, and then runtime crash

Observed Behavior

On chez this does something very weird:

Exception: incorrect number of arguments 1 to #<procedure void>

On node this loops at runtime.

When you remove the %spec line, it warns about compiling the hole, then crashes as expected when it encounters the hole.

[dunhamsteve]

I hit a similar error today when trying to write a combinator parser. (No holes involved.)

What was happening for me is that there were recursive dependencies between lazy values. (Purescript detects this and errors out at compile time.) If you look at blodwen-lazy you can see where the void is coming from:

(define blodwen-lazy
  (lambda (f)
    (let ([evaluated #f] [res void])
      (lambda ()
        (if (not evaluated)
            (begin (set! evaluated #t)
                   (set! res (f))
                   (set! f void))
            (void))
        res))))

I think this code should just throw rather than silently return void instead of the desired value, but ideally we'd detect this at compile time. (You can put a raise in there to verify that this is the root cause.)

On node, the lazy implementation doesn't have a guard and just recurses indefinitely:

function __lazy(thunk) {
  let res;
  return function () {
    if (thunk === undefined) return res;
    res = thunk();
    thunk = undefined;
    return res;
  };
};

[dunhamsteve]

As another example, this will error in scheme with Exception in number->string: #<foreign> is not a number and overflow the stack on node:

bar : List Int
foo : List Int
foo = 1 :: bar
bar = 2 :: foo

main : IO ()
main = printLn foo