Invert primINeg when it appears in metavariable spines (#6645)

src/full/Agda/TypeChecking/Conversion.hs

@@ -439,9 +439,6 @@ compareTerm' cmp a m n =
               -- enough for the bases to agree.
 
               compareTerm cmp aty (mkUnglue m) (mkUnglue n)
-         -- FIXME(Amy): This rule is overly eager, which can cause us to lose solutions.
-         -- See #6632.
-         {-
          Def q es | Just q == mHComp, Just (sl:s:args@[phi,u,u0]) <- allApplyElims es
                   , Sort (Type lvl) <- unArg s
                   , Just unglueU <- mUnglueU, Just subIn <- mSubIn
@@ -452,7 +449,6 @@ compareTerm' cmp a m n =
               let mkUnglue m = apply unglueU $ [argH l] ++ map (setHiding Hidden) [phi,u]  ++ [argH bA,argN m]
               reportSDoc "conv.hcompU" 20 $ prettyTCM (ty,mkUnglue m,mkUnglue n)
               compareTerm cmp ty (mkUnglue m) (mkUnglue n)
-         -}
          Def q es | Just q == mSub, Just args@(l:a:_) <- allApplyElims es -> do
               ty <- el' (pure $ unArg l) (pure $ unArg a)
               out <- primSubOut

src/full/Agda/TypeChecking/MetaVars.hs

@@ -1637,6 +1637,7 @@ inverseSubst' skip args = map (mapFst unArg) <$> loop (zip args terms)
     let irr | isIrrelevant info = True
             | DontCare{} <- v   = True
             | otherwise         = False
+    ineg <- getPrimitiveName' builtinINeg
     case stripDontCare v of
       -- i := x
       Var i [] -> return $ (Arg info i, t) `cons` vars
@@ -1685,6 +1686,12 @@ inverseSubst' skip args = map (mapFst unArg) <$> loop (zip args terms)
       -- Distinguish args that can be eliminated (Con,Lit,Lam,unsure) ==> failure
       -- from those that can only put somewhere as a whole ==> neutralArg
       Var{}      -> neutralArg
+
+      -- primINeg i := x becomes i := primINeg x
+      -- (primINeg is a definitional involution)
+      Def qn es | Just [Arg _ (Var i [])] <- allApplyElims es, Just qn == ineg ->
+        pure $ (Arg info i, Def qn [Apply (defaultArg t)]) `cons` vars
+
       Def{}      -> neutralArg  -- Note that this Def{} is in normal form and might be prunable.
       t@Lam{}    -> failure t
       t@Lit{}    -> failure t

test/Succeed/PruneINeg.agda

@@ -0,0 +1,19 @@
+{-# OPTIONS --cubical #-}
+module PruneINeg where
+
+open import Agda.Primitive renaming (Set to Type)
+open import Agda.Primitive.Cubical renaming (primIMin to _∧_; primIMax to _∨_; primINeg to ~_; isOneEmpty to empty)
+open import Agda.Builtin.Cubical.Path
+
+refl : ∀ {ℓ₁} {A : Type ℓ₁} {x : A} → x ≡ x
+refl {x = x} i = x
+
+sym : ∀ {ℓ₁} {A : Type ℓ₁} {x y : A}
+    → x ≡ y → y ≡ x
+sym p i = p (~ i)
+
+module _ {A : Set} {x y : A} (p : x ≡ y) where
+  _ : sym p ≡ sym _
+  _ = refl
+  -- Need to solve a constraint like _ (~ i) := p (~ i) by expanding
+  -- (~ i) := t into i := ~ t in the meta spine