(lam0 ...n.... (Var n+1)) Correct binders, Out-of-scope variable

(lam0 ...n.... lam1 ...n.... (Var n+n)) Mix of correct and wrong binders, Well-scoped variable

(lam1 ...n.... lam0 ...n.... (Var n+n)) Mix of wrong and correct binders, well-scoped variable

(lam1 ...n.... lam0 ...n.... (Var n+n+1)) Mix of correct and wrong binders, out-of-scope variable

(force (builtin ifThenElse) (con bool True) (con bool True) var99

Both branches are evaluated *before* the predicate, so it is clear that this should fail in every case.

(force (builtin ifThenElse) (con bool True) (delay true) (delay var99)

The branches are *lazy*. The evaluation result (success or failure) depends on how the machine ignores the irrelevant to the computation) part of the environment.

(force (builtin ifThenElse) (con bool True) (lam x (con bool True)) (lam x (con unit ()))

The branches are *lazy*. Note that the branches have **different** types. The machine cannot catch such a type error.

addInteger true

this relates to the immediate vs deferred unlifting. this used to be an immediate type error but now it is deferred until saturation.

(builtin addInteger) (con integer 1) (con integer 1) (con integer 1)

Interesting because it involves a (builtin) over-saturation type-error, which the machine can recognize.

(lam x x) (con integer 1) (con integer 1)

Interesting because it involves a (lambda) over-saturation type-error, which the machine can recognize.