Display multiple example types for things with nontrivial (non-parametric) polymorphism

[byorgey]

Closes #169. Previously, we did this:

Disco> :type \x. x - 2
λx. x - 2 : ℤ → ℤ

However, this was a lie since in fact \x. x - 2 is more general than that; but showing only one possible monomorphic type was still better than showing some generic monstrosity like forall a. (N <: a, subtractive a) => a -> a.

Now, with this PR, we do this:

Disco> :type \x. x - 2
This expression has multiple possible types.  Some examples:
λx. x - 2 : ℤ → ℤ
λx. x - 2 : ℚ → ℚ

See #169 for more context and examples.

Briefly, in this PR, we:

• Change the solver to return a list of solution substitutions instead of just a single one
• Add a "solution limit" counter to the solver so it can stop early once it has hit the limit for the number of solutions we want.
  • In some cases (e.g. when checking a provided type) we just want one.
  • In other cases (when inferring a type) we set an arbitrary bound of 16.
  • This is not really ideal --- in theory we would want to use some kind of proper backtracking logic monad like LogicT but that seems difficult/impossible to incorporate into polysemy (https://stackoverflow.com/questions/62627695/running-the-nondet-effect-once-in-polysemy; https://github.com/polysemy-research/polysemy/issues/246).
• "Thin" the resulting list of solutions by throwing away any solutions which are supertypes of another solution in the list.
• Add pretty-printing that distinguishes between a single solution and multiple solutions

It is still possible to make the solver blow up in case there are many possible container variables to instantiate. e.g. expressions like \x. \y. \z. \w. (set(x), set(y), set(z), set(w)) take a very long time to typecheck. I have some ideas for how to improve this situation, but for now it's an uncommon corner case.

[byorgey]

@justingrubbs , @LeitMoth I'd love for you to take a look at this when you get a chance (no rush). I certainly don't expect you to read and understand all the code changes, though you're welcome to look at it in whatever detail you like. But see if the overall idea makes sense, play with some examples, see if you can break it, that kind of thing.