[ fix #5506 ] by turning the crashed case into a conservative handling

Note: apparently, the author of the blamed commit
8760d15 was convinced of some
invariant that was refuted by #5506.

It makes sense to go back and investigate whether the invariant was
assumed in error or whether something else breaks this invariant.

src/full/Agda/TypeChecking/Rules/LHS/Unify.hs

@@ -942,13 +942,15 @@ patternBindingForcedVars forced v = do
     noForced v = gets $ IntSet.disjoint (precomputedFreeVars v) . IntMap.keysSet
 
     bind md i = do
-      Just md' <- gets $ IntMap.lookup i
-      if related md POLE md'    -- The new binding site must be more relevant (more relevant = smaller).
-        then do                 -- The forcing analysis guarantees that there exists such a position.
+      gets (IntMap.lookup i) >>= \case
+        Just md' | related md POLE md' -> do
+          -- The new binding site must be more relevant (more relevant = smaller).
+          -- "The forcing analysis guarantees that there exists such a position."
+          -- Really? Andreas, 2021-08-18, issue #5506
           tell   $ IntMap.singleton i md
           modify $ IntMap.delete i
           return $ varP (deBruijnVar i)
-        else return $ dotP (Var i [])
+        _ -> return $ dotP (Var i [])
 
     go md v = ifM (noForced v) (return $ dotP v) $ do
       v' <- lift $ lift $ reduce v

test/Succeed/Issue5506.agda

@@ -0,0 +1,42 @@
+-- Andreas, 2021-08-18, issue #5506 reported by alexarice
+
+-- A crash in the forcing methodology introduced in 2.6.1
+-- that surfaced with the removal of auto-inlining in 2.6.2.
+
+-- {-# OPTIONS --no-forcing #-}   -- fixes
+-- {-# OPTIONS --auto-inline #-}  -- fixes
+
+{-# OPTIONS -v tc.lhs.unify.force:100 #-}
+
+open import Agda.Builtin.Nat
+
+data Unit : Set where
+  unit : Unit
+
+data Ctx : Nat → Set where  -- index needed
+  cons : (m : Nat) (A : Unit) → Ctx (suc m)
+
+mutual
+
+  data P : (n : Nat) (Γ : Ctx n) → Set
+
+  -- Needs to be mutual
+  {-# NOINLINE getFocus #-}
+  getFocus : (n : Nat) (A : Unit) → Unit
+  getFocus n A = A  -- needs to be A, not unit
+
+  data P where
+    c : (n : Nat)  -- n is forced
+        (A : Unit)
+      → P (suc n) (cons n (getFocus n A))
+
+test : (n : Nat) (Γ : Ctx n) → P n Γ → Nat
+test n Γ (c m A) = n + m
+  -- ^ n := suc m fixes the issue
+
+-- WAS:
+-- Panic: Pattern match failure in do expression at
+-- src/full/Agda/TypeChecking/Rules/LHS/Unify.hs:1313:7-14
+-- when checking that the pattern c _ _ _ _ has type P n Γ
+
+-- Expect: type-checks without errors.