Tabled trait resolution

This PR introduces:

Tabled Logic Solver
Trait Instance Confirmation
Better error messages from WF check

1. Tabled Logic Solver

To implement trait instance confirmation, we need to achieve two goals: 1) find possible solutions for a given query as many as we want, and 2) ensure termination even in cases that include cycles. Therefore, I replaced the implementation of the trait solver with a tabled logic solver. The specific algorithm is based on Tabled Typeclass Resolution. While the paper proposes an algorithm that stops searching other solutions once a single solution is found, the implementation in Fe stops searching when either a specified maximum number of solutions is reached or solutions converge. A maximum number of solutions needs to be given to ensure that the solutions do not diverge infinitely(The current setting is 3). This algorithm is a variant of a SLG solver, for an introduction to a SLG solver, XSB: Extending Prolog with Tabled Logic Programming would be useful.

NOTE: The new solver performs a bunch of UnifictaionTable::clone, but the unification table here is actually PersistentUnificationTable, which provides very cheap clone implementation(O(1)).

NOTE2: It would be better for the solver to return solutions on-demand as an iterator rather than specifying a maximum number. However, this would complicate the implementation (especially making integration with salsa more challenging), and it should suffice to know whether the solutions are unique or ambiguous for now. Therefore, I have opted for a simpler implementation. Once v2 is deployed, I plan to revisit this approach.

2. Trait Instance Confirmation

In previous implementations, the results of trait resolution were not correctly integrated into the type inference phase(see #996). To resolve this, I introduced a phase where, if ambiguity arises during trait instance selection, the selection is deferred and type inference for the body proceeds. Once the type inference for the body is complete, the pending trait instances are confirmed. E.g.,

extern {
    fn todo() -> !
}

struct S<T> {
    t: T,
}

impl<T> S<T> {
    fn new() -> Self {
        todo()
    }
}

trait Trait<T, U> {
    fn foo(self) -> (T, U)
}

impl<T> Trait<T, i32> for S<T> {
    fn foo(self) -> (T, i32) {
        (self.t, 1)
    }
}

impl<T> Trait<u32, u32> for S<T> {
    fn foo(self) -> (u32, u32) {
        (1, 1)
    }
}

fn bar() -> (u64, i32) {
    let s = S::new()

    let (x, y) = s.foo()
    (x, y)
}

During type inference, ambiguity remains regarding whether to choose impl<T> Trait<T, i32> for S<T> or impl<T> Trait<u32, u32> for S<T> for s.foo(), but, this PR makes it possible to perform type inference correctly without requiring any additional type annotation.

To resolve pending confirmations, a fixed point computation is required, as confirmation of one pending trait instance may enable another pending trait instance confirmation. Since solutions are narrowed in each iteration of confirmation and trait instance equality is defined as $\alpha$-equivalence, the termination of this fixed point computation is guaranteed.

NOTE: This PR provides a means to resolve ambiguity in Trait Instances(i.e., selecting proper impl for a given trait), but it does not provide a solution for ambiguity in Traits themselves. That would make it quite difficult/complicated to continue type inference when a trait itself is ambiguous.

3. Better error messages from WF check

This PR also improves error messages from WF checks, which now output unsatisfied trait bounds (when possible) if a type or trait instance is ill-formed. E.g.,

enum Option<T> {
    Some(T),
    None
}

trait Clone {
    fn clone(self) -> Self
}

impl<T> Clone for Option<T>
where T: Clone
{
    fn clone(self) -> Self {
        use Option::*

        match self {
            Some(t) => Some(t.clone())
            None => None
        }
    }
}

fn foo<T>(opt: Option<T>) {
    let x = opt.clone()
}

↓

error[6-0003]: trait bound is not satisfied
   ┌─ foo.fe:24:17
   │
24 │     let x = opt.clone();
   │                 ^^^^^
   │                 │
   │                 `Option<T>` doesn't implement `Clone`
   │                 trait bound `T: Clone` is not satisfied

ethereum / fe