Float DefP clauses above catch-alls (#7097)

src/full/Agda/TypeChecking/CompiledClause/Compile.hs

@@ -9,6 +9,7 @@ import Control.Monad
 import Control.Monad.Trans.Identity
 
 import Data.Maybe
+import Data.List (partition)
 import qualified Data.Map as Map
 
 import Agda.Syntax.Common
@@ -127,7 +128,6 @@ compileWithSplitTree t cs = case t of
         -- collapse record pattern splits
   SplittingDone n -> compile cs
     -- after end of split tree, continue with left-to-right strategy
-
   where
     compiles :: LazySplit -> SplitTrees -> Case Cls -> Case CompiledClauses
     compiles lz ts br@Branches{ projPatterns = cop
@@ -310,15 +310,35 @@ splitC n (Cl ps b) = caseMaybe mp fallback $ \case
 -- @
 expandCatchAlls :: Bool -> Int -> Cls -> Cls
 expandCatchAlls single n cs =
-  -- Andreas, 2013-03-22
-  -- if there is a single case (such as for record splits)
-  -- we force expansion
-  if single then doExpand =<< cs else
   case cs of
-  _                | all (isCatchAllNth . clPats) cs -> cs
-  c@(Cl ps b) : cs | not (isCatchAllNth ps) -> c : expandCatchAlls False n cs
-                   | otherwise -> map (expand c) expansions ++ c : expandCatchAlls False n cs
-  _ -> __IMPOSSIBLE__
+    _ -- Andreas, 2013-03-22
+      -- if there is a single case (such as for record splits)
+      -- we force expansion
+      | single -> doExpand =<< cs
+
+      -- If all clauses have a variable at the nth argument, expansion
+      -- would have no effect
+      | all (isCatchAllNth . clPats) cs -> cs
+
+    c@(Cl ps b):cs
+      -- If the head clause does not have a catch-all pattern for the
+      -- nth argument, we can keep it at the head and do no expansion
+      | not (isCatchAllNth ps) -> c : expandCatchAlls False n cs
+
+      -- If there's a DefP clause for this argument later on, then it
+      -- should take priority over catch-all clauses, so we rotate them
+      -- out of the way.
+      -- DefP clauses are always inserted by the system and should
+      -- "defeat" user-written inexact patterns.
+      | (defps@(_:_), rest) <- partition isDefPNth (c:cs)
+      -> defps ++ expandCatchAlls False n rest
+
+      -- If the head clause *does* have an irrefutable pattern for the
+      -- nth argument, and there's nothing more important after, then we
+      -- duplicate the subsequent overlapping clauses with c's RHS
+      -- instead.
+      | otherwise -> map (expand c) expansions ++ c : expandCatchAlls False n cs
+    _ -> __IMPOSSIBLE__
   where
     -- In case there is only one branch in the split tree, we expand all
     -- catch-alls for this position
@@ -339,6 +359,10 @@ expandCatchAlls single n cs =
     classify (DefP _ q _) = Right (Right q)
     classify _            = __IMPOSSIBLE__
 
+    isDefPNth cl = case unArg <$> listToMaybe (drop n (clPats cl)) of
+      Just DefP{} -> True
+      _ -> False
+
     -- All non-catch-all patterns following this one (at position n).
     -- These are the cases the wildcard needs to be expanded into.
     expansions = nubOn (classify . unArg . snd)

test/Fail/Issue7033a.agda

@@ -0,0 +1,20 @@
+{-# OPTIONS --cubical --safe #-}
+module Issue7033a where
+
+open import Agda.Primitive.Cubical
+  renaming (primIMax to _∨_ ; primIMin to _∧_ ; primINeg to ~_ ; primComp to comp ; primHComp to hcomp ; primTransp to transp)
+
+data ⊥ : Set where
+data ⊤ : Set where tt : ⊤
+data D : Set where
+  base  : D
+  loop  : PathP (λ _ → D) base base
+  other : D
+
+onS¹ : D → Set
+onS¹ base     = ⊤
+onS¹ (loop i) = ⊤
+onS¹ _        = ⊥
+
+JEEPERS! : ⊥
+JEEPERS! = transp (λ i → onS¹ (hcomp {φ = ~ i} (λ { j (i = i0) → base }) base)) i0 tt

test/Fail/Issue7033a.err

@@ -0,0 +1,7 @@
+Issue7033a.agda:20,12-86
+hcomp (λ i → isOneEmpty) (transp (λ i → Set) i0 (onS¹ base)) !=< ⊥
+when checking that the expression
+transp
+(λ i₁ → onS¹ (hcomp {φ = ~ i₁} (λ { j (i₁ = i0) → base }) base)) i0
+tt
+has type ⊥

test/Fail/Issue7033b.agda

@@ -0,0 +1,19 @@
+{-# OPTIONS --cubical --safe #-}
+module Issue7033b where
+
+open import Agda.Primitive.Cubical
+  renaming (primIMax to _∨_ ; primIMin to _∧_ ; primINeg to ~_ ; primComp to comp ; primHComp to hcomp ; primTransp to transp)
+
+data ⊥ : Set where
+data ⊤ : Set where tt : ⊤
+
+data D : ⊤ → Set where
+    c1 : D tt
+    c2 : D tt
+
+isC1 : {A : ⊤} → D A → Set
+isC1 c1 = ⊤
+isC1 _  = ⊥
+
+JEEPERS! : ⊥
+JEEPERS! = transp (λ i → isC1 (transp (λ j → D tt) (~ i) c1)) i0 tt

test/Fail/Issue7033b.err

@@ -0,0 +1,5 @@
+Issue7033b.agda:19,12-68
+⊤ !=< ⊥
+when checking that the expression
+transp (λ i₁ → isC1 (transp (λ j → D tt) (~ i₁) c1)) i0 tt has type
+⊥