What generation condition for types?
Currently a new RefinedC type is automatically generated on a struct if either:
- it has a refinement (i.e., at least one
- it has a
rc::ptr_typeannotation (in which case there can be no
rc::refined_by, and the refinement is
One might wonder, can we relax this? And would this be useful in practice?
I have tried relaxing this behaviour but there is no obvious way to do this. The problem is that we explicitly rely on the fact that no types are generated in two cases:
- nested structs, as for
- and union cases (which are also nested structs), as
One solution is to add a
rc::only_nested annotation that instructs the front end not to generate a type. However that is a bit annoying in the case of unions. However there is no easy way to avoid this since the front end does not distinguish structs that are nested from those that appear at the top level.
Another possible solution (not tried yet) is to move the
rc::union_tag annotation into structs (and not have it as field annotation). This annotation would also disable the generation of a type, while keeping the information we need for the struct.