Skip to content

More compositional handling of rr::context assertions for ghost state

Currently, rr::context isn't very compositional: if you put it on an ADT definition, you also have to manually put it everywhere that ADT is used, e.g. in functions and other ADTs using it. Ideally, we should automatically include it.

One way would be to define one typeclass for every ADT that includes all the context items it needs (parameterized to handle generics) and require that everywhere the ADT is used. This should then also be exported in interface files.