Skip to content

Fix RecursiveEvaluator not erasing types (Stainless #1135)

Viktor Kuncak requested to merge fix-stainless-1135 into scala-2.13

Created by: gsps

Fixes Inox-side issue of Stainless issue 1135 (https://github.com/epfl-lara/stainless/issues/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?

Merge request reports