`dischargeCekValue` doesn't handle open terms correctly

[effectfully]

dischargeCekValue has the following code:

                  -- var is free, leave it alone
                  (Var () named)

which means that

(\0 \0 var 2) (delay (var 1))

evaluates to

[1 :-> delay (var 1)] (\0 var 2)

which then discharges to

\0 delay (var 1)

which is variable capture.

[danbaruka]

Hi, I think I understand the issue and why variable capture happens during discharge under lambdas. I’d be happy to work on a fix if no one is already on it. Let me know

[basetunnel]

In a similar way, partially applied built-ins are problematic when evaluating open terms:

(λ. λ. var 2) ((force ifThenElse) True (delay (var 1)))

evaluates to

λ. (force IfThenElse) True (var 1)

Right now, discharging partially applied built-ins is free:

dischargeCekValue = ...
  where
    goValue = \case
      ...
      VBuiltin _ term _ -> term

But to support evaluation of open terms, shifting term here is necesary.