From 0bbdb18bfc2cf4b2f435cf5f2d5c09d774beba10 Mon Sep 17 00:00:00 2001
From: Andreas Abel <andreas.abel@ifi.lmu.de>
Date: Fri, 5 Jan 2024 11:12:58 +0100
Subject: [PATCH] [ fix #7048 ] Only define hcomp constructors when
 --cubical-compatible.

---
 src/full/Agda/TypeChecking/Rules/Data.hs   | 9 ++++++---
 src/full/Agda/TypeChecking/Rules/Record.hs | 5 +++--
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/src/full/Agda/TypeChecking/Rules/Data.hs b/src/full/Agda/TypeChecking/Rules/Data.hs
index c859c756986..56ebb8742ca 100644
--- a/src/full/Agda/TypeChecking/Rules/Data.hs
+++ b/src/full/Agda/TypeChecking/Rules/Data.hs
@@ -328,10 +328,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
diff --git a/src/full/Agda/TypeChecking/Rules/Record.hs b/src/full/Agda/TypeChecking/Rules/Record.hs
index 5055d6c413a..05d8ad124dd 100644
--- a/src/full/Agda/TypeChecking/Rules/Record.hs
+++ b/src/full/Agda/TypeChecking/Rules/Record.hs
@@ -374,8 +374,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.