Refactor generics type checking to be symbolic

[jemc]

We took our approach to typechecking generics from this paper, written for Pony, but never adopted by Pony: https://www.ponylang.io/media/papers/formalizing-generics-for-pony.pdf

In particular, we used "partial reification" of type parameters to exhaustively check every combination of reference capabilities.

This made a lot of things easier to implement, but in other ways it's not so great:

• It took lots of iteration and refactoring over the years to try to improve compiler performance, and performance is still bad for types that have many type parameters, since it's combinatorial complexity for each added one.

• There is no known strategy for handling multiple reference capabilities in a single type argument (for example, in Array(A) where A is reified as (String'ref | U64'val), we have no partial reification which covers that case, since we have only typechecked with ref and val separately but never in a union)

After a discussion with Sylvan on this topic, it seems the only way past these difficulties is to make generics type checking fully symbolic rather than partially symbolic and partially reified as it is now.

So we're looking at our 3rd major rewrite of the way we do type inference and type checking. Yay.

[jemc]

This document explaining how constraint solving works in the Swift compiler is likely to be helpful: https://github.com/apple/swift/blob/main/docs/TypeChecker.md

[jemc]

(Assigned myself because I'll definitely be the one to work on this, and it needs to be done fairly soon, though I may not start putting pen to paper immediately because I need to do more research and thinking - so there may not be immediate progress on this issue yet)

[jemc]

Watched this short video over lunch today, which includes some useful information on approaches to optimize general constraint-solving problems: https://youtu.be/lCrHYT_EhDs?t=1205