Test typing rules relying on metafunctions inside of judgments

[atgeller]

Certain typing rules in the typing judgment \vdash in InstructionTyping.rkt rely on meta-function calls inside recursive calls to \vdash in the premise. For example:

[(where ((t_1 ...) -> (t_2 ...)) tf)
   (⊢ (in-label C (t_1 ...)) (e ...) tf)
   -------------------------------------
   (⊢ C ((loop tf (e ...))) tf)]

However, this currently causes redex to reject derivations it should accept (see #racket/redex/issues/219). This makes testing the current judgment rules impossible. One workaround is to move the metafunction call into a separate where clause:

(where C_2 (in-label C (t_2 ...)))
   (⊢ C_2 (e ...) tf)

However, this is undesirable, as it introduces extra variables and clauses, making the rules harder to read and making them look less like the rules in the paper.

Until the issue gets resolved, assuming it can be, the typing judgment should use the workaround for testing.