Fix #7146: fix and harden instance Pretty NamedBinding

Do deep pattern matching to prevent bit-rotting of this function in
the future.  It stated to malfunction when cohesion was added.

src/full/Agda/Syntax/Concrete.hs

@@ -271,8 +271,10 @@ dropTypeAndModality (DomainFree x) = [DomainFree $ setModality defaultModality x
 data BoundName = BName
   { boundName       :: Name
   , bnameFixity     :: Fixity'
-  , bnameTactic     :: TacticAttribute -- From @tactic attribute
+  , bnameTactic     :: TacticAttribute
+      -- ^ From @\@tactic@ attribute.
   , bnameIsFinite   :: Bool
+      -- ^ The @\@finite@ cannot be parsed, it comes from the builtin @Partial@ only.
   }
   deriving Eq
 

src/full/Agda/Syntax/Concrete/Pretty.hs

@@ -84,11 +84,14 @@ prettyRelevance a = (pretty (getRelevance a) <>)
 prettyQuantity :: LensQuantity a => a -> Doc -> Doc
 prettyQuantity a = (pretty (getQuantity a) <+>)
 
+instance Pretty Lock where
+  pretty = \case
+    IsLock LockOLock -> "@lock"
+    IsLock LockOTick -> "@tick"
+    IsNotLock -> empty
+
 prettyLock :: LensLock a => a -> Doc -> Doc
-prettyLock a doc = case getLock a of
-  IsLock LockOLock -> "@lock" <+> doc
-  IsLock LockOTick -> "@tick" <+> doc
-  IsNotLock -> doc
+prettyLock a = (pretty (getLock a) <+>)
 
 prettyErased :: Erased -> Doc -> Doc
 prettyErased = prettyQuantity . asQuantity
@@ -285,8 +288,10 @@ instance Pretty LamClause where
       pretty' (RHS e)   = arrow <+> pretty e
       pretty' AbsurdRHS = empty
 
+-- Andreas, 2024-02-25
+-- Q: Can we always ignore the tactic and the finiteness here?
 instance Pretty BoundName where
-  pretty BName{ boundName = x } = pretty x
+  pretty (BName x _fix _tac _fin) = pretty x
 
 data NamedBinding = NamedBinding
   { withHiding   :: Bool
@@ -300,29 +305,31 @@ isLabeled x
   | otherwise              = Nothing
 
 instance Pretty a => Pretty (Binder' a) where
-  pretty (Binder mpat n) = let d = pretty n in case mpat of
-    Nothing  -> d
-    Just pat -> d <+> "@" <+> parens (pretty pat)
+  pretty (Binder mpat n) =
+    applyWhenJust mpat (\ pat -> (<+> ("@" <+> parens (pretty pat)))) $ pretty n
 
 instance Pretty NamedBinding where
-  pretty (NamedBinding withH x) = prH $
-    if | Just l <- isLabeled x -> text l <+> "=" <+> pretty xb
-       | otherwise             -> pretty xb
-
+  pretty (NamedBinding withH
+           x@(Arg (ArgInfo h (Modality r q c) _o _fv (Annotation lock))
+               (Named _mn xb@(Binder _mp (BName _y _fix t _fin))))) =
+    applyWhen withH prH $
+    applyWhenJust (isLabeled x) (\ l -> (text l <+>) . ("=" <+>)) (pretty xb)
+      -- isLabeled looks at _mn and _y
+      -- pretty xb prints also the pattern _mp
     where
+    prH = (pretty r <>)
+        . prettyHiding h mparens
+        . (coh <+>)
+        . (qnt <+>)
+        . (lck <+>)
+        . (tac <+>)
+    coh = pretty c
+    qnt = pretty q
+    tac = pretty t
+    lck = pretty lock
+    -- Parentheses are needed when an attribute @... is printed
+    mparens = applyUnless (null coh && null qnt && null lck && null tac) parens
 
-    xb = namedArg x
-    bn = binderName xb
-    prH | withH     = prettyRelevance x
-                    . prettyHiding x mparens
-                    . prettyCohesion x
-                    . prettyQuantity x
-                    . prettyTactic bn
-        | otherwise = id
-    -- Parentheses are needed when an attribute @... is present
-    mparens
-      | noUserQuantity x, null (bnameTactic bn) = id
-      | otherwise = parens
 
 instance Pretty LamBinding where
     pretty (DomainFree x) = pretty (NamedBinding True x)

test/Fail/Issue3945.err

@@ -1,4 +1,4 @@
 Issue3945.agda:10,8-25
 Incorrect cohesion annotation in lambda
-when checking that the expression λ @♭ a → flat a has type
+when checking that the expression λ (@♭ a) → flat a has type
 A → Flat A

test/Fail/Issue5033.err

@@ -1,3 +1,3 @@
 Issue5033.agda:4,10-29
 Missing binding for primLockUniv primitive.
-when checking that the expression ∀ _ → Set is a type
+when checking that the expression ∀ (@tick _) → Set is a type

test/Fail/Issue7146.agda

@@ -0,0 +1,34 @@
+-- Andreas, 2024-02-25, issue #7146, printer bugs:
+-- Missing parenthesis in domain-free module parameter with cohesion.
+-- Missing printing of @lock attribute.
+
+{-# OPTIONS --cohesion --erasure --guarded #-}
+
+import Agda.Builtin.Bool
+open import Agda.Builtin.Sigma
+
+primitive
+  primLockUniv : Set₁
+
+postulate
+  Tick : primLockUniv
+  Foo  : @♭ Set → Tick → Set
+
+module @0 Bool where
+
+  -- Trigger an error here printing the module telescope, e.g.
+  -- "Not supported: open public in hard compile-time mode".
+
+  open module M (@♭ A) (@lock l) (_ : Foo A l) {@ω B = C : Set} {D : C → Set} {p@(u , v) : Σ C D}
+    = Agda.Builtin.Bool public
+
+-- Expect to fail.
+--
+-- Error was:
+-- when checking the module application
+-- module M @♭ A l (_ : Foo A l) ...
+--
+-- This misprints the module parameters, correct is:
+-- module M (@♭ A) (@lock l) ...
+--
+-- Should print the module telescope correctly.

test/Fail/Issue7146.err

@@ -0,0 +1,7 @@
+Issue7146.agda:22,3-23,31
+Not supported: open public in hard compile-time mode (for instance
+in erased modules)
+when checking the module application
+module M (@♭ A) (@lock l) (_ : Foo A l) {@ω B = C : Set}
+         {D : C → Set} {p @ (u , v) : Σ C D}
+  = Agda.Builtin.Bool