Modular implicits about broom

[nilern]

This paper has all the details of a resolution algorithm. It seems to be essentially the same as our subtyping as long as the codomain of implicit functions is matched before the domain (which causes recursive resolution).

The major required change is support for backtracking; we should probably just put a Prolog 'trail' style undo stack in the typing context. That should be both easier to implement and more performant than an explicit substitution state that could be discarded immutably.

The paper also includes type well-formedness rules that ensure termination of resolution. We might eventually also want the equivalent of UndecidableInstances that just limits the resolution stack depth somewhat arbitrarily. Modular Implicits also seem to be a lot lazier about preventing nontermination.

[nilern]

Also need to be able to block the resolution of an implicit whose type contains unification variables until the moment those unification variables go out of scope. This mechanism should also be useful for generativity polymorphism (related to #9).

[nilern]

Actually using persistent union-find instead of a trail. Avoids complexity when undoing union operations and should only be slower by a constant factor. (Might even be faster since apparently a fast union-find might not be so fast when backtracking is required.)

[nilern]

Switched to mutable union-find with backtracking.