To my knowledge, the flag --erased-cubical enforces that any definition imported from a module that sets --cubical can only be used in an erased context. If this understanding is correct, I don't think this is very practical.

For some context, I am writing a shallowly embedded DSL in Cubical Agda for verified parsing that currently makes heavy use of the Cubical standard library.

As originally written, the DSL is not extractable to Haskell because it uses the Path type in several of its primitive constructions. To alleviate that concern, I am currently refactoring to replace mentions of Path with Data.Equality, and similar changes, so that I can then extract a verified parser to Haskell. This refactor has gone reasonably well so far, but I find myself quite frustrated and needing to duplicate much of the Cubical standard library to play nicely with --erased-cubical.

For instance, we encode strings as a List type (imported from Cubical.Data.List) over an alphabet. However, Cubical.Data.List sets the flag --cubical, which means that any of its functions (even the one's that don't really use any Cubical features, such as _++_ or length) are not available in a module that I want to extract to Haskell. This is quite frustrating for my refactor, and it means I can either rewrite everything from scratch, or I can duplicate a version of the Cubical standard repo with the same interface but with --erased-cubical set.

I have so far chosen the latter approach, where I make an erased version of the Cubical library, however this feels like the morally wrong approach. Moreover, it is very mechanistic. I am simply setting the flag, changing any modules fromCubical.<module> to Erased.<module>, and putting an erasure annotation on anything that is truly leveraging cubical type theory. It seems like this process could be automated

Perhaps, I have misunderstood how cubical erasure works and this code duplication can already be avoided

If I am not mistaken, and this duplication is not currently avoidable for my use case. My hopes is that the analysis for --erased-cubical is not computed on a module-wide level, but is a finer-grained analysis, perhaps for individual terms. It seems silly to have to do some import dance to be allowed to use a function that never really depended on cubical in the first place