Eta-expand mismatched cubical primitives (#7071)

Explanation from the test case:

Eta-expansion was not kicking in for hcomp/transp for record values,
since they look like neutrals (both are headed by a Def, and neither
primHComp/primTransp have copatterns in their definition).

src/full/Agda/TypeChecking/Conversion.hs

@@ -324,38 +324,89 @@ compareTerm' cmp a m n =
             then do
               whenProfile Profile.Conversion $ tick "compare at eta record"
               sig <- getSignature
-              let ps = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
-              -- Andreas, 2010-10-11: allowing neutrals to be blocked things does not seem
-              -- to change Agda's behavior
-              --    isNeutral Blocked{}          = False
-                  isNeutral (NotBlocked _ Con{}) = return False
-              -- Andreas, 2013-09-18 / 2015-06-29: a Def by copatterns is
-              -- not neutral if it is blocked (there can be missing projections
-              -- to trigger a reduction.
-                  isNeutral (NotBlocked r (Def q _)) = do    -- Andreas, 2014-12-06 optimize this using r !!
-                    not <$> usesCopatterns q -- a def by copattern can reduce if projected
-                  isNeutral _                   = return True
-                  isMeta b = case ignoreBlocking b of
-                               MetaV{} -> True
-                               _       -> False
+
+              transp <- getPrimitiveName' builtinTrans
+              hcomp <- getPrimitiveName' builtinHComp
+
+              let
+                ps = fromMaybe __IMPOSSIBLE__ $ allApplyElims es
+                -- Andreas, 2010-10-11: allowing neutrals to be blocked things does not seem
+                -- to change Agda's behavior
+                --    isNeutral Blocked{}          = False
+                isNeutral (NotBlocked _ Con{}) = return False
+
+                -- Andreas, 2013-09-18 / 2015-06-29: a Def by copatterns is
+                -- not neutral if it is blocked (there can be missing projections
+                -- to trigger a reduction.
+                isNeutral (NotBlocked r (Def q _)) = do    -- Andreas, 2014-12-06 optimize this using r !!
+                  not <$> usesCopatterns q -- a def by copattern can reduce if projected
+                isNeutral _                   = return True
+
+                -- Amy, 2024-01-29: Is this blocked application headed by one of the
+                -- cubical primitives that behave as though they are copattern matching?
+                isCubicalPrimHead (NotBlocked r (Def q _)) -- Amy, 2024-01-29: optimise this using r !!
+                  | Just q == transp || Just q == hcomp
+                  = Just q
+                isCubicalPrimHead _ = Nothing
+
+                isMeta b = case ignoreBlocking b of
+                  MetaV{} -> True
+                  _       -> False
 
               reportSDoc "tc.conv.term" 30 $ prettyTCM a <+> "is eta record type"
               m <- reduceB m
               mNeutral <- isNeutral m
               n <- reduceB n
               nNeutral <- isNeutral n
+
+              let
+                h1 = isCubicalPrimHead m
+                h2 = isCubicalPrimHead n
+
+                mCub = isJust (isCubicalPrimHead m)
+                nCub = isJust (isCubicalPrimHead n)
+
+              when (mCub || nCub) $
+                reportSDoc "tc.conv.term.cubical" 30 $ vcat
+                  [ ("m (" <> prettyTCM mNeutral <> ", " <> prettyTCM mCub <> ", " <> prettyTCM h1 <> "):")
+                  , nest 2 (prettyTCM m)
+                  , ("n (" <> prettyTCM nNeutral <> ", " <> prettyTCM nCub <> ", " <> prettyTCM h2 <> "):")
+                  , nest 2 (prettyTCM n)
+                  , "at type"
+                  , nest 2 (prettyTCM a')
+                  , "same head:" <+> prettyTCM (h1 == h2)
+                  ]
+
               if | isMeta m || isMeta n -> do
                      whenProfile Profile.Conversion $ tick "compare at eta-record: meta"
                      compareAtom cmp (AsTermsOf a') (ignoreBlocking m) (ignoreBlocking n)
-                 | mNeutral && nNeutral -> do
+
+                 -- Amy, 2024-01-29 (fixing issue pointed out by Tom Jack):
+                 --
+                 -- Cubical primitives reduce to something awful, so we would like to skip comparing them (causes
+                 -- "timeout" in GroupPath).
+                 --
+                 -- We would also like to skip comparing a cubical primitive against something that is *small* and
+                 -- actually neutral (causes "timeout" in KleinBottle cohomology groups, comparing a 93KiB(!) transport
+                 -- against an application of set-truncation recursion to a metavariable)
+                 --
+                 -- The condition for skipping eta expansion is thus:
+                 --   (a) both are neutrals (which in this case also includes a "suspended"/copattern transp/hcomp)
+                 --   (b) if both are headed by a cubical primitive, then they are the same primitive.
+                 --
+                 -- So we will skip expanding transp A φ u0 = transp A' φ' u0', since it's definitionally injective; We
+                 -- will skip expanding transp A φ u0 = f ?, since it's wasted work; but we will not skip
+                 -- transp A φ u0 = hcomp u u0', since those must both compute if they are to be equal.
+                 | mNeutral && nNeutral && (not (mCub && nCub) || h1 == h2) -> do
                      whenProfile Profile.Conversion $ tick "compare at eta-record: both neutral"
                      -- Andreas 2011-03-23: (fixing issue 396)
                      -- if we are dealing with a singleton record,
                      -- we can succeed immediately
                      let profUnitEta = whenProfile Profile.Conversion $ tick "compare at eta-record: both neutral at unit"
-                     ifM (isSingletonRecordModuloRelevance r ps) (profUnitEta) $ do
+                     ifM (isSingletonRecordModuloRelevance r ps) profUnitEta $ do
                        -- do not eta-expand if comparing two neutrals
                        compareAtom cmp (AsTermsOf a') (ignoreBlocking m) (ignoreBlocking n)
+
                  | otherwise -> do
                      whenProfile Profile.Conversion $ tick "compare at eta-record: eta-expanding"
                      (tel, m') <- etaExpandRecord r ps $ ignoreBlocking m

src/full/Agda/TypeChecking/Monad/Signature.hs

@@ -1395,7 +1395,7 @@ projectionArgs :: Definition -> Int
 projectionArgs = maybe 0 (max 0 . pred . projIndex) . isRelevantProjection_
 
 -- | Check whether a definition uses copatterns.
-usesCopatterns :: (HasConstInfo m) => QName -> m Bool
+usesCopatterns :: (HasConstInfo m, HasBuiltins m) => QName -> m Bool
 usesCopatterns q = defCopatternLHS <$> getConstInfo q
 
 -- | Apply a function @f@ to its first argument, producing the proper

test/Succeed/EtaHComp.agda

@@ -0,0 +1,42 @@
+{-# OPTIONS --cubical #-}
+module EtaHComp where
+
+open import Agda.Primitive renaming (Set to Type)
+open import Agda.Builtin.Cubical.Path
+open import Agda.Builtin.Cubical.Id
+open import Agda.Builtin.Cubical.Glue; open Helpers public
+open import Agda.Primitive.Cubical
+  renaming (primIMax to _∨_ ; primIMin to _∧_ ; primINeg to ~_ ; primComp to comp ; primHComp to hcomp ; primTransp to transp)
+open import Agda.Builtin.Sigma
+open import Agda.Builtin.Nat
+
+data S¹ : Type where
+  base : S¹
+  loop : base ≡ base
+
+_×_ : (A : Type) (B : Type) → Type
+A × B = Σ A (λ _ → B)
+infixr 5 _×_
+
+T = PathP (λ i → S¹ × S¹) (base , base) (base , base)
+
+t1 : T
+t1 = λ j → transp (λ _ → S¹ × S¹) i0
+             (hcomp (λ i → λ { (j = i0) → (base , base)
+                             ; (j = i1) → (base , base)
+                             })
+                    (base , base))
+
+t4 : T
+t4 = (λ j → hcomp {A = S¹ × S¹}
+                  (λ i → λ { (j = i0) → (base , base)
+                           ; (j = i1) → (base , base)
+                           })
+                  (base , base))
+
+-- Eta-expansion was not kicking in for hcomp/transp for record values,
+-- since they look like neutrals (both are headed by a Def, and neither
+-- primHComp/primTransp have copatterns in their definition).
+
+test : PathP (λ i → T) t1 t4
+test = refl