Rust: Add predicate for certain type information

[paldepind]

Motivated by performance problems seen in #20140 this PR introduces a new "phase" to type inference in the form of a new inferCertainType predicate.

Motivation

There's a lot of places where we approximate things in type inference. These inaccuracies cause us to sometimes infer multiple types for the same term. Inaccurate types can lead to other inaccurate types and things can spiral and blow up from there. In the worst case we end up with cycles in type inference.

In #20140 performance blew up in Sway at a place where several cycles in inference happened. This PR adds a reduced version of that problem, which was caused by a type coercion that we don't handle. I don't see an easy way to handle such coercions correctly, and more generally think it'll be hard to make our entire type inference 100% correct.

Proposed solution

This PR adds a new "phase" to type inference, which is just a new predicate called inferCertainType. The idea is that

• inferCertainType contains a subset of the type inference that is sure to be 100% correct. This implies that inferCertainType (ideally) never contains multiple types for the same node and path.
• inferType uses (and is a superset) of inferCertainType, but not the other way around. This means that we can use inferCertainType negated in inferType to eliminate or block inaccuracies when we actually have accurate information.

This PR implements a minimum viable version of the idea which is sufficient to fix the cycle in Sway (and the test). We infer certain type information only for 1/ annotated terms and 2/ very simple calls and let the information propagate along a few equalities. The PR also uses a negated inferCertainType to block inferTypeEquality from letting (wrong) type information flow to a node where we have complete correct type information. This is what cuts the cycle in the example.

Pros of this approach:

• We get a separation in the code between inaccurate and accurate inference rules.
• We can contain wrongly inferred types from propagating and prevent cycles.
• The above could also potentially result in better performance. We might also be able to guard expensive type inference with a not inferCertainType(n, _), i.e., if the simple and correct rules give us a type we can stop inference there.

Cons:

• The architecture is slightly more complicated.
• There is a bit of duplication in the certain and the uncertain part of type inference.

Results on #20140

With this PR the number of nodes with a type at the type path lenght limit in Sway is reduced from 76 and to 63.

When quick eval'ing inferType on Sway I see the following:

	nr of tuples	time	DCA
main	2,404,901	63s
#20140	5,458,859	107s	DCA
#20140 + this PR	2.414.244	70s	DCA

So this PR seems to remove the blowup caused by #20140 for Sway.

Future work

As mentioned this is just a minimum viable implementation.

• We should be able to move more stuff into inferCertainType.

• Right now inferCertainType(n, path) is only allowed to give results if we have complete information of the entire type tree for n. It would be nice to lift this requirement s.t. it is allowed to have results as long as the type specifically at path is certain.

  This will make it much easier to soundly include things in inferCertainType. For instance, then we can have a certain root type for Some(a) without necessarily having a certain type for the nested type.

  However, we still need to know when we have complete certain information of a node (to implement the block in inferTypeEquality). Ideally that could be derived from inferCertainType by checking if the type tree is complete, but that is more work to implement.