Recompute blocker in equalSort (#7039)

Issue #7034 presents a case where a blocking meta gets solved by pruning, so we need to update blockers we are passing around when there is a chance that they got stale.

Fixes #7034.

src/full/Agda/TypeChecking/Conversion.hs

@@ -1272,6 +1272,7 @@ leqSort s1 s2 = do
                    , nest 2 $ fsep [ pretty s1 <+> "=<"
                                    , pretty s2 ]
                    ]
+                 blocker <- updateBlocker blocker
                  addConstraint blocker $ SortCmp CmpLeq s1 s2
 
     propEnabled <- isPropEnabled
@@ -1693,14 +1694,16 @@ equalSort s1 s2 = do
     let (s1,s2) = (ignoreBlocking s1b, ignoreBlocking s2b)
         blocker = unblockOnEither (getBlocker s1b) (getBlocker s2b)
 
-    let postponeIfBlocked = catchPatternErr $ \blocker ->
+    let postponeIfBlocked = catchPatternErr $ \blocker -> do
           if | blocker == neverUnblock -> typeError $ UnequalSorts s1 s2
              | otherwise -> do
                  reportSDoc "tc.conv.sort" 30 $ vcat
                    [ "Postponing constraint"
                    , nest 2 $ fsep [ prettyTCM s1 <+> "=="
                                    , prettyTCM s2 ]
                    ]
+                 -- Andreas, 2023-12-21, recomputing the blocker fixes issue #7034.
+                 blocker <- updateBlocker blocker
                  addConstraint blocker $ SortCmp CmpEq s1 s2
 
     propEnabled <- isPropEnabled

test/Succeed/Issue7034-2.agda

@@ -0,0 +1,29 @@
+-- Andreas, 2023-12-21, another test for #7034 by Christian Sattler
+
+{-# OPTIONS --two-level --rewriting --confluence-check #-}
+
+module Issue7034-2 where
+
+open import Agda.Primitive using (SSet)
+
+postulate
+  X : SSet
+  x : X
+  Eq : X → X → SSet
+
+{-# BUILTIN REWRITE Eq #-}
+
+module _ (B : SSet) where
+  record R : SSet where
+    field
+      b : B
+      g : B → X
+
+  postulate
+    r : R
+  open R r
+
+  postulate
+    rule : Eq (g b) x
+
+{-# REWRITE rule #-}

test/interaction/Issue7034.agda

@@ -0,0 +1,24 @@
+-- Andreas, 2023-12-21, issue #7034 reported and testcase by Christian Sattler
+--
+-- A meta that was designated as blocker for a constraint gets instantiated by pruning here.
+-- Solved by recomputing the blocker just in time.
+
+{-# OPTIONS --two-level #-}
+
+module Issue7034 where
+
+open import Agda.Primitive using (SSet)
+
+postulate
+  A : SSet
+  x : A
+
+foo : {!(y : A) → ?!}  -- give "(y : A) → ?" here
+foo = x
+
+-- WAS: internal error: an instantiated meta used as blocker for a constraint.
+
+-- Expected error:
+--
+-- (y : A) → ?1 (y = y) != A of type SSet
+-- when checking that the expression (y : A) → ? has type SSet

test/interaction/Issue7034.in

@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+goal_command 0 cmd_give "(y : A) → ?"

test/interaction/Issue7034.out

@@ -0,0 +1,9 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "?0 : SSet " nil)
+((last . 1) . (agda2-goals-action '(0)))
+(agda2-info-action "*Error*" "1,1-12 (y : A) → ?1 (y = y) != A of type SSet when checking that the expression (y : A) → ? has type SSet" nil)
+(agda2-highlight-load-and-delete-action)
+(agda2-status-action "")