Prior to Agda 2.6.3, the
--cubical-compatible flag did not
--without-K also implied the (internal) generation of
Cubical Agda-specific code. See Agda issue #5843 for the rationale
behind this change.
Compatibility with Cubical Agda consists of:
Due to specifics of the Cubical Agda implementation, several kinds of Agda definition need internal support code to be generated during their elaboration.
Occasionally, elaborator bugs can result in errors surfacing from these
internal definitions, despite the code being type-correct. To avoid
showing errors mentioning cubical definitions when the user-written code
is independent of Cubical Agda, these internal definitions are now gated