Here, conversion from IPLD of the type of motive will have the bound variable with index 0 representing True replaced with a constant reference because of the recrCtx at that point.
However, the IPLD representation of the expressions for (t : True) -> (Sort u) are identical in both meta and anon information, and so result in identical CIDs. Our caching in the converter only uses the CIDs alone as keys, which is not sufficient and results in a roundtrip failure when both the inductive True and the definition test are converted. It seems we need to add additional information to the key to account for the recrCtx to an extent. Simply adding the recrCtx itself though would result in cache misses in cases where the context isn't relevant to a particular expression, so we need some finer way of determining whether the recrCtx is indeed relevant to a particular IPLD expression. A bit more refactoring of the design of the IPLD representation may be necessary to get this to work.
Consider the following definition:
Here, conversion from IPLD of the type of
not_motivewill have the bound variable with index 0 forTrueremain as a bound variable.Now, consider the recursor rule associated with
True.intro:Here, conversion from IPLD of the type of
motivewill have the bound variable with index 0 representingTruereplaced with a constant reference because of therecrCtxat that point.However, the IPLD representation of the expressions for
(t : True) -> (Sort u)are identical in both meta and anon information, and so result in identical CIDs. Our caching in the converter only uses the CIDs alone as keys, which is not sufficient and results in a roundtrip failure when both the inductiveTrueand the definitiontestare converted. It seems we need to add additional information to the key to account for therecrCtxto an extent. Simply adding therecrCtxitself though would result in cache misses in cases where the context isn't relevant to a particular expression, so we need some finer way of determining whether therecrCtxis indeed relevant to a particular IPLD expression. A bit more refactoring of the design of the IPLD representation may be necessary to get this to work.