_UNBOUND_REL_i

[yforster]

I am trying to debug a large meta-program written in MetaCoq using the printing effect, and I'm running into an issue where print_id prints _UNBOUND_REL_0.

The meta program has the guard checker turned off, but otherwise, apart from being fairly long, doesn't do anything specific.

I am not using the TemplateMonad, so we're looking at a pure Coq program.

Could this be a bug in reduction effects, or a bug in reduction? I could try to minimise, but given the complexity of the program that would take some while, so I'm doing a shot into the dark here, maybe somebody (@JasonGross @herbelin?) has an idea what's going on :)

[SkySkimmer]

Which reduction machine? I think some of them don't have the local env at hand.

[yforster]

I'm using cbv

[SkySkimmer]

Indeed it seems cbv has a delayed substitution instead of a local env

[herbelin]

This suggests a bug somewhere (e.g. the 0 suggests an invalid lift (-1) or something like that), but more details would be needed. What is the context of binders, what subexpressions is being reduced, what should be the expected term being printed instead of _UNBOUND_REL_0?

[SkySkimmer]

I guess around https://github.com/coq/coq/blob/ae57be8165c4d3b475106983c504280cc3e6bc4c/pretyping/cbv.ml#L967 and other cases where cbv goes under binders we would need to push_rel in the info.env