[ fix #7048 ] Only define hcomp constructors when --cubical-compatible.

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

@@ -329,10 +329,13 @@ checkConstructor d uc tel nofIxs s con@(A.Axiom _ i ai Nothing c e) =
             let con = ConHead c IsData Inductive $ zipWith (<$) names $ map argFromDom $ telToList fields
 
             defineProjections d con params names fields dataT
+            -- Andreas, 2024-01-05 issue #7048:
+            -- Only define hcomp when --cubical-compatible.
+            cubicalCompatible <- optCubicalCompatible <$> pragmaOptions
             -- Cannot compose indexed inductive types yet.
-            comp <- if nofIxs /= 0 || (Info.defAbstract i == AbstractDef)
-                    then return emptyCompKit
-                    else inTopContext $ defineCompData d con params names fields dataT boundary
+            comp <- if cubicalCompatible && nofIxs == 0 && Info.defAbstract i == ConcreteDef
+                    then inTopContext $ defineCompData d con params names fields dataT boundary
+                    else return emptyCompKit
             return (con, comp, Just names)
 
         -- add parameters to constructor type and put into signature

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

@@ -375,8 +375,9 @@ checkRecDef i name uc (RecordDirectives ind eta0 pat con) (A.DataDefParams gpars
 
 
       -- 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
+      whenM (optCubicalCompatible <$> pragmaOptions) do
+        escapeContext impossible npars do
+          addCompositionForRecord name haveEta con tel (map argFromDom fs) ftel rect
 
       -- The confluence checker needs to know what symbols match against
       -- the constructor.