lean4
lean4 copied to clipboard
feat: `opaque_repr` attribute to suppress "trivial structure" opt
This adds an attribute @[opaque_repr] which is used by both the old and new compilers to suppress the "trivial structure" optimization (which deletes mk and proj applications for newtype structures), replacing the existing is_runtime_builtin_type() function. (There is a TODO(Leo): use an attribute? comment in the code, so I am hopeful that this is a desirable direction.)
I have renamed the function to has_opaque_repr_attr though because it's not actually about builtin types, and the provided test case shows where it is useful in user code: when you are making an opaque type (i.e. a type where the mk / val / casesOn will be overridden using implemented_by), the compiler's trivial structure optimization can cause calls to the overridden functions to be removed.
The attribute name is slightly more generic than "suppress trivial structure optimization", and is intended as a general purpose attribute to put on types to direct the compiler that it should not make any assumptions about the type layout, with the default (non-overridden) behavior being that of a boxed inductive type.
@digama0 sent me the following explanation of the underlying issue here, which I'll quote here in the hope it is useful:
Right now the compiler has what can only be described as a bug where it deletes constructors and projections of "trivial wrapper structures" in the style of ULift or Inhabited even if those constructors have an @[extern] or @[implemented_by] implementation, resulting in unsound behavior. The only reason this works for core data types like Array and String is because they are explicitly exempted in a hardcoded list in the compiler. The PR replaces this list with an attribute so that user types can also avoid the issue.