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:
- if the type was defined in a module in
lib_protocol
and aliased inAlpha_context
, then a tag is added in the initial module and brought all the way up toAlpha_context
(e.g.Script_string_repr.t
,Script_int_repr.t
); - if the type was defined in a module outside
lib_procotol
, then this means that the scope of the type spreads further than the protocol, and we should not change the its definition. So we create a new module inScript_typed_ir
and lift the operations used in the protocol (e.g.Script_typed_ir.Script_chain_id.t
); - if the type was defined as a product in
Script_typed_ir
, it is made a structure in order to differentiate it frompair
(e.g.Script_typed_ir.Script_address.t
,Script_typed_ir.Script_typed_contract.t
); - if the type was defined in
Script_typed_ir
not as a product, then the tag is added directly at its definition site (e.g.Script_typed_ir.set
,Script_typed_ir.map
).
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, butn num
andz 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.