[ fix agda#5633 ] Take into account that C.LHSWith can be nested

src/full/Agda/Syntax/Common.hs

@@ -2894,6 +2894,15 @@ instance Null ExpandedEllipsis where
   null  = (== NoEllipsis)
   empty = NoEllipsis
 
+instance Semigroup ExpandedEllipsis where
+  NoEllipsis <> e          = e
+  e          <> NoEllipsis = e
+  (ExpandedEllipsis r1 k1) <> (ExpandedEllipsis r2 k2) = ExpandedEllipsis (r1 <> r2) (k1 + k2)
+
+instance Monoid ExpandedEllipsis where
+  mempty  = NoEllipsis
+  mappend = (<>)
+
 instance KillRange ExpandedEllipsis where
   killRange (ExpandedEllipsis _ k) = ExpandedEllipsis noRange k
   killRange NoEllipsis             = NoEllipsis

src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs

@@ -2711,7 +2711,7 @@ hasExpandedEllipsis core = case core of
   C.LHSProj{}       -> hasExpandedEllipsis $ namedArg $ C.lhsFocus core -- can this ever be ExpandedEllipsis?
   C.LHSWith{}       -> hasExpandedEllipsis $ C.lhsHead core
   C.LHSEllipsis r p -> case p of
-    C.LHSWith _ wps _ -> ExpandedEllipsis r (length wps)
+    C.LHSWith p wps _ -> hasExpandedEllipsis p <> ExpandedEllipsis r (length wps)
     C.LHSHead{}       -> ExpandedEllipsis r 0
     C.LHSProj{}       -> ExpandedEllipsis r 0
     C.LHSEllipsis{}   -> __IMPOSSIBLE__

test/interaction/Issue5633.agda

@@ -0,0 +1,11 @@
+data ⊤ : Set where
+  tt : ⊤
+
+f : ⊤ → ⊤
+f tt = tt
+
+foo : ⊤ → ⊤
+foo t with f t
+... | x with f t
+... | y with f t
+... | z = {!z!}

test/interaction/Issue5633.in

@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_make_case "z"

test/interaction/Issue5633.out

@@ -0,0 +1,8 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : ⊤ " nil)
+((last . 1) . (agda2-goals-action '(0)))
+((last . 2) . (agda2-make-case-action '("... | tt = ?")))
+((last . 1) . (agda2-goals-action '(0)))