Support cyclic global variables
Currently, it is hard to instantiate globalsG
in adequacy if an initialized type of one global variable refers to another (one needs to unfold the definition of initialized
) and impossible if there is a cycle.
This is a problem because building a cycle can happen by accident and the user would not know if they do not instantiate adequacy.
The right solution would be to use some ghost state to agree on the initialized types (leibniz equality should be enough).