Skip to content

possible abstraction promise break in `tyThingLocalGREs` when dealing with `AConLike` that is a real data constructor

In the tyThingLocalGREs function introduced in the commit 3f374399, if the TyThing passed to the function is AConLike with a RealDataCon as payload, and that data constructor has record fields that are shared with the other constructors o the parent data type, the resulting GRE for that record field will not have all the constructors it is contained in (the recFieldCons field of RecFieldInfo in the IAmRecField case of GREInfo). Since the function tyThingLocalGREs is only called from the interactive context, this is not an issue because AConLike is never constructed there with a RealDataCon (at least from my understanding). However, such a potential abstraction leak could cause problems in the future.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information