hcomp symbols in interface not hidden under --cubical-compatible

[sattlerc]

From #7044 (comment):

When printing the signatures of the interface, I see Inner.hcomp-T. Why is that generated without --cubical-compatible?

Test case:

module Inner where

data T : Set where
  t : T

Running

agda-quicker Inner.agda -v 5 | grep hcomp

shows that cubical-related code is executed:

Generated name: [...] "hcomp-T" [...]

[andreasabel]

I suppose a check for --cubical-compatible is missing here:

agda/src/full/Agda/TypeChecking/Rules/Data.hs

Lines 333 to 335 in 5e47be6

	comp <- if nofIxs /= 0 || (Info.defAbstract i == AbstractDef)
	then return emptyCompKit
	else inTopContext $ defineCompData d con params names fields dataT boundary

and here:

agda/src/full/Agda/TypeChecking/Rules/Record.hs

Lines 377 to 379 in 5e47be6

	-- we define composition here so that the projections are already in the signature.
	escapeContext impossible npars $ do
	addCompositionForRecord name haveEta con tel (map argFromDom fs) ftel rect