[racket] Using Redex for type systems w/ unconstrained variables

Hi all,

I've hit a problem with using Redex for designing type systems and
wanted to see if anyone had any ideas for working around it.

Background: Redex now offers the nice `define-judgment-form` feature for
defining things like type rules. These judgments can specify either I or
O (input or output) for each of the positions (e.g., type environment,
term, type).

For something like STLC's type system, you would want a judgment like (I
I O) for environment, term, type. The type is an O because you want to
synthesize the type for each term.

This works out until you want to add something like `error` to your
calculus. The desired rule for such a feature might be:

  ---------------
  Γ ⊦ (error) : t

with an unconstrained type t for the result. This rule won't actually
work in Redex because it doesn't accept a non-terminal as a synthesized
type. For other reasons, setting the type to always be input will also
not work (to see why, try writing the rule for function application).

We've thought of four ways that we might work around this:

  * Add a bottom type to our language and use subtyping for cases like
    error above. This doesn't seem too bad for error, but isn't so
    natural for other constructs.

  * Re-formulate the type system as a bidirectional type system (ala the
    Local Type Inference paper) with both I and O judgments.

  * Add redundant type information to terms and use synthesis in all
    cases. This complicates the expression grammar unnecessarily.

  * Abandon Redex for typesetting and use something like Kanren or
    Racklog for the computational part of the type system.

None of the options seem great. Are there any other options for this use
case? Are we missing anything obvious?

Cheers,
Asumu