[wires]

There is a payoff between strictness and usability. To be more precise in the type system beyond what typedefs has now, you need to involve more complicated stuff such as dependent types or refinement types. I don't have the answer, but having (co)products and recursion seems like a reasonable starting point.

[nsonha]

by all levels of strictness I don't mean being as strict as possible. I meant it should accommodate for less strict usages as well as strict usages.