Fix #7177: only setScope when scope is not null

src/full/Agda/Syntax/Scope/Base.hs

@@ -634,13 +634,41 @@ mapNameSpaceM fd fm fs ns = update ns <$> fd (nsNames ns) <*> fm (nsModules ns)
 
 instance Null Scope where
   empty = emptyScope
-  null  = __IMPOSSIBLE__
-    -- TODO: define when needed, careful about scopeNameSpaces!
+  -- -- Use default implementation of null
+  -- null Scope{ scopeName, scopeParents, scopeNameSpaces, scopeImports, scopeDatatypeModule } = and
+  --   [ null scopeName
+  --   , null scopeParents
+  --   , null scopeNameSpaces || all (null . snd) scopeNameSpaces
+  --   , null scopeImports
+  --   , null scopeDatatypeModule
+  --   ]
 
 instance Null ScopeInfo where
   empty = emptyScopeInfo
-  null  = __IMPOSSIBLE__
-    -- TODO: define when needed, careful about _scopeModules!
+  -- -- Use default implementation of null
+  -- null ScopeInfo
+  --   { _scopeCurrent
+  --   , _scopeModules
+  --   , _scopeVarsToBind
+  --   , _scopeLocals
+  --   , _scopePrecendence
+  --   , _scopeInverseName
+  --   , _scopeInverseModule
+  --   , _scopeInScope
+  --   , _scopeFixities
+  --   , _scopePolarities
+  --   } = and
+  --   [ null _scopeCurrent
+  --   , null _scopeModules || all null (Map.values _scopeModules)
+  --   , null _scopeVarsToBind
+  --   , null _scopeLocals
+  --   , null _scopePrecendence
+  --   , null _scopeInverseName
+  --   , null _scopeInverseModule
+  --   , null _scopeInScope
+  --   , null _scopeFixities
+  --   , null _scopePolarities
+  --   ]
 
 -- | The empty scope.
 emptyScope :: Scope

src/full/Agda/TypeChecking/Rules/Term.hs

@@ -1411,7 +1411,7 @@ checkOrInferMeta
 checkOrInferMeta i newMeta mt = do
   case A.metaNumber i of
     Nothing -> do
-      setScope (A.metaScope i)
+      unlessNull (A.metaScope i) setScope
       (cmp , t) <- maybe ((CmpEq,) <$> workOnTypes newTypeMeta_) return mt
       (x, v) <- newMeta cmp t
       setMetaNameSuggestion x (A.metaNameSuggestion i)

src/full/Agda/Utils/Null.hs

@@ -45,15 +45,18 @@ import Text.PrettyPrint.Annotated (Doc, isEmpty)
 import Agda.Utils.Bag (Bag)
 import qualified Agda.Utils.Bag as Bag
 
+import Agda.Utils.Unsafe (unsafeComparePointers)
 import Agda.Utils.Impossible
 
 class Null a where
   empty :: a
   null  :: a -> Bool
   -- ^ Satisfying @null empty == True@.
 
+  -- | The default implementation of 'null' compares with 'empty',
+  --   first trying pointer equality, then falling back to 'Eq' equality.
   default null :: Eq a => a -> Bool
-  null = (== empty)
+  null a = unsafeComparePointers a empty || a == empty
 
 instance Null () where
   empty  = ()

test/interaction/Issue7177.agda

@@ -0,0 +1,32 @@
+-- Andreas, 2024-03-10, issue #7177
+-- Correct scope when introducing underscores
+-- via pattern synonyms.
+
+open import Agda.Builtin.Bool
+open import Agda.Builtin.Equality
+
+data D : Set where
+  c : { i : true ≡ false } → D
+
+pattern ff {i} = c {i}
+
+works : D
+works = c
+
+-- yellow:
+-- _i_6 : true ≡ false
+
+test : D
+test = ff
+
+-- yellow:
+-- _i_8
+--   : Agda.Builtin.Bool.Bool.true Agda.Builtin.Equality.≡
+--     Agda.Builtin.Bool.Bool.false
+
+-- No scope for underscore.
+
+-- Expected output:
+--
+-- _i_6 : true ≡ false  [ at ... ]
+-- _i_8 : true ≡ false  [ at ... ]

test/interaction/Issue7177.in

@@ -0,0 +1,2 @@
+top_command (cmd_load currentFile [])
+

test/interaction/Issue7177.out

@@ -0,0 +1,6 @@
+(agda2-status-action "")
+(agda2-info-action "*Type-checking*" "" nil)
+(agda2-highlight-clear)
+(agda2-status-action "")
+(agda2-info-action "*All Goals*" "_i_6 : true ≡ false [ at Issue7177.agda:14,9-10 ] _i_8 : true ≡ false [ at Issue7177.agda:20,8-10 ] " nil)
+((last . 1) . (agda2-goals-action '()))