[CN] Consider using non-det. monad instead of explicit continuations

[dc-mak]

The current implementation of backend/cn/lib/check.ml uses continuations to sort of dynamically let-normalise the core program.

This is done to avoid the need to handle join points and to terminate type checking early by ignoring the continuation in cases (symbolic) control flow is not meant to return to the parent AST node.

It has the downside of making the code a bit more fragile and less clear. Given that what we are essentially saying is that symbolic evaluation can return 0, 1, or many (i.e. for an if-expression, 2) symbolic values, using which the rest of the program must be checked, I wondered if this could be more cleanly implemented using a non-determinism/list monad: type checking passes if the program type checks with all values (including 0, vacuously).

It may also make any future specifications/formalisations of the type system easier.