Fix RecursiveEvaluator not erasing types (Stainless #1135)

[gsps]

Fixes Inox-side issue of Stainless issue 1135 (epfl-lara/stainless#1135). While issues on the Inox side weren't directly observed, we should really be operating on fully-erased values, so that expressions such as Set[Int](1) == Set[{ x: Object | (T(x)): @unchecked }](1) evaluate to true.

@samarion I didn't make any changes to Lambda so far. Should we adapt normalizeLambda to erase parameter types?

[samarion]

I thought about this a bit more and now I'm wondering if we're not at risk of breaking choose (and forall) evaluation by erasing type parameters in function invocations.

Maybe the rule should rather be that values have their types erased? Actually I remember thinking at some point that we need to change the evaluation of Equals to avoid the need to normalize values immediately, which could help clarify at which point dropping dependent types is required.

[gsps]

What's the deal with https://github.com/epfl-lara/inox/blob/master/src/main/scala/inox/evaluators/RecursiveEvaluator.scala#L525 anyways? It seems that lookup is contextual on the tps stored in rctx via newTypes in the FunctionInvocation case. But the corresponding update methods for the chooses map (withoutChooses and newChooses) don't get called anywhere? So it seems the chooses in rctx get initialized from the model once, here, and that's it: https://github.com/epfl-lara/inox/blob/master/src/main/scala/inox/evaluators/ContextualEvaluator.scala#L85

Is newTypes related to polymorphic recursion, or what's going on? Shouldn't choose merely depend on the value arguments of the surrounding function?

[samarion]

Huh, well I don't know what withoutChooses and newChooses are supposed to do. As you say, chooses are only copied over from the solver output before evaluation starts.

Is newTypes related to polymorphic recursion, or what's going on? Shouldn't choose merely depend on the value arguments of the surrounding function?

Well, ideally you'd want chooses to depend only on values. But since there's no way to really erase types in Inox, we unfortunately have type-dependent chooses (e.g. choose((x: T) => true) where T is a type parameter). I don't think we can fix that without adding a Top type to Inox and basically moving type encoding into Inox. That's where the newTypes comes into play: it allows us to get type-dependent choose results as reported in the model.

But that's only the story for chooses which exist in the model. Erasing types is fine for those, however, we also support evaluating chooses which don't exist in the model:

inox/src/main/scala/inox/evaluators/SolvingEvaluator.scala

Line 36 in 11911e8

def onChooseInvocation(choose: Choose): Expr = {

If we erase types, then we won't be able to take dependent types into account when evaluating such chooses. For example, in the following program you would want to call to get to return a positive integer. If you erase the type, then the semantics change:

def get[T](): T = choose((x: T) => true)
get[{x: Int => x > 0}]()