I find that Pedal's type system is growing increasingly complex. The logic started in TIFA, was partially included in CAIT, became relevant to many functions in the Toolkit, and is now also a very big part of Assertions. I've backed into supporting both static types and runtime types, from a wide variety of sources:

• Inferred types from static analysis (half of TIFA's business)
• AST annotation nodes (the new optional static typing feature)
• Python type functions (e.g., list, int)
• A JSON-encoded representation from CORGIS
• String representations of the types (which at some point in Python's future, will be the only representation of AST annotations!)
• The Python typing module (well, not really, but we could)

It seems like it might be time to promote Pedal's type system to something more sophisticated and customizable, extracting it out of TIFA into its own Tool. I'm imagining a system where the savvy teacher could set flags and make modifications to the Type system in order to achieve certain experiences - for example, you might disable support for my wacky [int] list annotations or allow None to be used for certain types (default Optional behavior). The main value would be a consistent API for other Tools to refer to types, and make it clear what type-consuming functions are allowed to consume (e.g., can you pass in a string-represented-type to assert_is_instance?).

I'm not sure this is the right time for this change, since we're hitting the semester soon. However, I don't know that we can rewrite the last major Toolkit submodule (functions) without making some kind of coherent decision here. But perhaps we can push it off until later if we're a little clever. Regardless, we need to make some decisions about this long term!