Skip to content

Proto/Michelson: fix injectivity of types

Context

Closes #1962 (closed).

As described in the origin issue, some type parameters of Script_typed_ir.ty are made a little bit more concrete, so that they differ from the typechecker's point of view.

This allows to remove some impossible branches that were previously closed by assertion failures.

The chosen implementation strategy is rather straightforward: for each concerned type, add a tag (unboxed to cut the overhead in memory cost), make it a structure or expose its definition, so that the type is made unique. And then just solve all the compilation errors that this created. In some places, a trade-off had to be made between keeping the impacts low, or making the design more intuitive.

In the end, types used in Script_typed_ir come from three kinds of places depending on their definition site:

Finally, has_lazy_storage has been enriched by removing the True_f variant, and explicitly replacing it with the concerned cases (big_map and sapling_state).

Notes:

  • in order to keep the commit sequence clear, the compilation fails on some commits;
  • num differs from the other types, but n num and z num are still not distinguishable, because it was not needed to solve the issue.

Checklist

  • N/A Document the interface of any function added or modified.
  • N/A Document any change to the user interface, including configuration parameters.
  • N/A Provide automatic testing.
  • N/A For new features and bug fixes, add an item in the appropriate changelog.
  • Select suitable reviewers using the Reviewers field below.
  • Select as Assignee the next person who should take action on that MR.
Edited by Nicolas Ayache

Merge request reports