From 63104a44d1fe490f1f25e30ebac776f6327f2d50 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 30 Jul 2026 10:01:01 +0100
Subject: [PATCH 1/5] [ refactor ] make `Data.List.Base.[_]` a pattern synonym

---
 CHANGELOG.md            | 3 +++
 src/Data/List/Base.agda | 6 ++++--
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index eb838bcbe1..a9aeb5f8d0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -147,6 +147,9 @@ Non-backwards compatible changes
   their definitions and signatures updated to use `IsMagmaHomomorphism` and
   `IsMonoidHomomorphism` respectively
 
+* In `Data.List.Base`: the function definition `[_]` has been turned into
+  a `pattern` synonym, with a companion function definition `pure` instead.
+
 * In `Data.List.DifferenceList.Base`: `take` and `drop` are deprecated
   because they do not have a lawful relationship to their `Data.List`
   counterparts. Consider using `viaList` if you want a lawful lifting
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 79b87608d3..3718e4a5ad 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -42,6 +42,8 @@ private
 open import Agda.Builtin.List public
   using (List; []; _∷_)
 
+pattern [_] x = x ∷ []
+
 ------------------------------------------------------------------------
 -- Operations for transforming lists
 
@@ -156,8 +158,8 @@ length = foldr (const suc) 0
 ------------------------------------------------------------------------
 -- Operations for constructing lists
 
-[_] : A → List A
-[ x ] = x ∷ []
+pure : A → List A
+pure = [_]
 
 fromMaybe : Maybe A → List A
 fromMaybe (just x) = [ x ]

From e11556307b8462a3440bedb4337a00709ebd99ba Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 30 Jul 2026 10:04:27 +0100
Subject: [PATCH 2/5] knock-ons

---
 src/Data/List/Effectful.agda                     | 6 +++---
 src/Data/List/Relation/Unary/Any/Properties.agda | 2 +-
 src/Text/Format/Generic.agda                     | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Data/List/Effectful.agda b/src/Data/List/Effectful.agda
index 874dc68205..55b98ca218 100644
--- a/src/Data/List/Effectful.agda
+++ b/src/Data/List/Effectful.agda
@@ -9,8 +9,8 @@
 module Data.List.Effectful where
 
 open import Data.Bool.Base using (false; true)
-open import Data.List.Base
-  using (List; map; [_]; ap; []; _∷_; _++_; concat; concatMap)
+open import Data.List.Base as List
+  using (List; map; ap; []; _∷_; _++_; concat; concatMap)
 open import Data.List.Properties
   using (++-identityʳ; ++-assoc; map-cong; concatMap-cong; map-concatMap
         ; concatMap-pure)
@@ -43,7 +43,7 @@ functor = record { _<$>_ = map }
 applicative : RawApplicative {ℓ} List
 applicative = record
   { rawFunctor = functor
-  ; pure = [_]
+  ; pure = List.pure
   ; _<*>_  = ap
   }
 
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 1b67ab6925..e2fbe0f1f4 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -13,7 +13,7 @@ open import Data.Bool.ListAction using (any)
 open import Data.Bool.Properties using (T-∨; T-≡)
 open import Data.Empty using (⊥)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.List.Base as List hiding (find; and; or; all; any)
+open import Data.List.Base as List hiding (find; and; or; all; any; pure)
 open import Data.List.Effectful as List using (monad)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional
diff --git a/src/Text/Format/Generic.agda b/src/Text/Format/Generic.agda
index 50b8580871..29a1756fe1 100644
--- a/src/Text/Format/Generic.agda
+++ b/src/Text/Format/Generic.agda
@@ -11,7 +11,7 @@ module Text.Format.Generic where
 open import Level using (0ℓ)
 open import Effect.Applicative
 open import Data.Char.Base using (Char)
-open import Data.List.Base as List hiding (sum)
+open import Data.List.Base as List hiding (sum; pure)
 open import Data.Maybe.Base as Maybe
 open import Data.Nat.Base
 open import Data.Nat.ListAction using (sum)

From 914402c868b208296ef2aefce04206574fc2ada3 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Thu, 30 Jul 2026 10:33:58 +0100
Subject: [PATCH 3/5] fix: one last knock-on?

---
 src/IO.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/IO.agda b/src/IO.agda
index 90b25d1c07..a3d3702631 100644
--- a/src/IO.agda
+++ b/src/IO.agda
@@ -63,7 +63,7 @@ module Colist where
 
 module List where
 
-  open import Data.List.Base
+  open import Data.List.Base hiding (pure)
 
   sequence : List (IO A) → IO (List A)
   sequence []       = ⦇ [] ⦈

From 16b2e2503274a7ad4203875ed9e6657467ed2534 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 31 Jul 2026 09:30:26 +0100
Subject: [PATCH 4/5] rename: `pure` to `singleton` plus the other list-like
 containers

---
 CHANGELOG.md                      | 4 +++-
 src/Data/DifferenceList/Base.agda | 9 ++++++---
 src/Data/List/Base.agda           | 4 ++--
 src/Data/List/Fresh/NonEmpty.agda | 6 ++++--
 src/Data/List/NonEmpty/Base.agda  | 6 ++++--
 src/Data/Vec/Base.agda            | 6 ++++--
 6 files changed, 23 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a9aeb5f8d0..2cda2e9025 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -148,7 +148,9 @@ Non-backwards compatible changes
   `IsMonoidHomomorphism` respectively
 
 * In `Data.List.Base`: the function definition `[_]` has been turned into
-  a `pattern` synonym, with a companion function definition `pure` instead.
+  a `pattern` synonym, with a companion function definition `singleton` instead.
+  Similarly for `Data.List.NonEmpty.Base`, `Data.List.Fresh.NonEmpty`, and also
+  `Data.DifferenceList.Base`, where the notation `[_]` is introduced as `syntax`.
 
 * In `Data.List.DifferenceList.Base`: `take` and `drop` are deprecated
   because they do not have a lawful relationship to their `Data.List`
diff --git a/src/Data/DifferenceList/Base.agda b/src/Data/DifferenceList/Base.agda
index 73c15d0ef9..e4f973f9a7 100644
--- a/src/Data/DifferenceList/Base.agda
+++ b/src/Data/DifferenceList/Base.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.DifferenceList.Base where
+module Data.DifferenceList.BaseSYNTAX where
 
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base using (ℕ)
@@ -34,8 +34,11 @@ infixr 5 _∷_ _++_
 [] : DiffList A
 [] = id
 
-[_] : A → DiffList A
-[ x ] = x List.∷_
+singleton : A → DiffList A
+singleton = List._∷_
+
+singleton-syntax = singleton
+syntax singleton-syntax x = [ x ]
 
 _++_ : DiffList A → DiffList A → DiffList A
 _++_ = _∘′_
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 3718e4a5ad..940472f999 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -158,8 +158,8 @@ length = foldr (const suc) 0
 ------------------------------------------------------------------------
 -- Operations for constructing lists
 
-pure : A → List A
-pure = [_]
+singleton : A → List A
+singleton = [_]
 
 fromMaybe : Maybe A → List A
 fromMaybe (just x) = [ x ]
diff --git a/src/Data/List/Fresh/NonEmpty.agda b/src/Data/List/Fresh/NonEmpty.agda
index eeaa846c53..33a545231a 100644
--- a/src/Data/List/Fresh/NonEmpty.agda
+++ b/src/Data/List/Fresh/NonEmpty.agda
@@ -33,6 +33,8 @@ record List#⁺ (A : Set a) (R : Rel A r) : Set (a ⊔ r) where
     tail : List# A R
     {rel} : fresh A R head tail
 
+pattern [_] x = x ∷#⁺ []
+
 open List#⁺
 
 ------------------------------------------------------------------------
@@ -41,8 +43,8 @@ open List#⁺
 uncons : List#⁺ A R → A × List# A R
 uncons (x ∷#⁺ xs) = x , xs
 
-[_] : A → List#⁺ A R
-[ x ] = x ∷#⁺ []
+singleton : A → List#⁺ A R
+singleton = [_]
 
 length : List#⁺ A R → ℕ
 length (x ∷#⁺ xs) = suc (List#.length xs)
diff --git a/src/Data/List/NonEmpty/Base.agda b/src/Data/List/NonEmpty/Base.agda
index 45fc692329..d11fcbac79 100644
--- a/src/Data/List/NonEmpty/Base.agda
+++ b/src/Data/List/NonEmpty/Base.agda
@@ -40,6 +40,8 @@ record List⁺ (A : Set a) : Set a where
     head : A
     tail : List A
 
+pattern [_] x = x ∷ []
+
 open List⁺ public
 
 ------------------------------------------------------------------------
@@ -48,8 +50,8 @@ open List⁺ public
 uncons : List⁺ A → A × List A
 uncons (hd ∷ tl) = hd , tl
 
-[_] : A → List⁺ A
-[ x ] = x ∷ []
+singleton : A → List⁺ A
+singleton = [_]
 
 infixr 5 _∷⁺_
 
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index 2143607444..df87a933c1 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -37,6 +37,8 @@ data Vec (A : Set a) : ℕ → Set a where
   []  : Vec A zero
   _∷_ : ∀ (x : A) (xs : Vec A n) → Vec A (suc n)
 
+pattern [_] x = x ∷ []
+
 infix 4 _[_]=_
 
 data _[_]=_ {A : Set a} : Vec A n → Fin n → A → Set a where
@@ -240,8 +242,8 @@ countᵇ p = count (T? ∘ p)
 ------------------------------------------------------------------------
 -- Operations for building vectors
 
-[_] : A → Vec A 1
-[ x ] = x ∷ []
+singleton : A → Vec A 1
+singleton = [_]
 
 replicate : (n : ℕ) → A → Vec A n
 replicate zero    x = []

From 96a1a85bd82de278f700fa80c413c8c70a0e1137 Mon Sep 17 00:00:00 2001
From: jamesmckinna <j.mckinna@hw.ac.uk>
Date: Fri, 31 Jul 2026 09:44:58 +0100
Subject: [PATCH 5/5] fix: tidy-up knock-ons, plus narrow `import`s

---
 src/Data/DifferenceList/Base.agda                | 2 +-
 src/Data/DifferenceList/Properties.agda          | 2 +-
 src/Data/List/Effectful.agda                     | 4 ++--
 src/Data/List/Relation/Unary/Any/Properties.agda | 2 +-
 src/Data/Tree/Binary.agda                        | 5 +++--
 src/IO.agda                                      | 4 +++-
 src/Text/Format/Generic.agda                     | 2 +-
 7 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/src/Data/DifferenceList/Base.agda b/src/Data/DifferenceList/Base.agda
index e4f973f9a7..88bdfc2014 100644
--- a/src/Data/DifferenceList/Base.agda
+++ b/src/Data/DifferenceList/Base.agda
@@ -6,7 +6,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-module Data.DifferenceList.BaseSYNTAX where
+module Data.DifferenceList.Base where
 
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base using (ℕ)
diff --git a/src/Data/DifferenceList/Properties.agda b/src/Data/DifferenceList/Properties.agda
index f49d8aec21..4328675e96 100644
--- a/src/Data/DifferenceList/Properties.agda
+++ b/src/Data/DifferenceList/Properties.agda
@@ -9,7 +9,7 @@
 module Data.DifferenceList.Properties where
 
 open import Data.DifferenceList.Base
-  using (DiffList; fromList; toList; viaList; []; _∷_; [_]; _++_; _∷ʳ_; map)
+  using (DiffList; fromList; toList; viaList; []; _∷_; singleton-syntax; _++_; _∷ʳ_; map)
 open import Data.List.Base as List using (List)
 open import Data.List.Properties using (++-assoc; ++-identityʳ)
 open import Data.Product.Base using (Σ; _,_)
diff --git a/src/Data/List/Effectful.agda b/src/Data/List/Effectful.agda
index 55b98ca218..c7fd87dfca 100644
--- a/src/Data/List/Effectful.agda
+++ b/src/Data/List/Effectful.agda
@@ -10,7 +10,7 @@ module Data.List.Effectful where
 
 open import Data.Bool.Base using (false; true)
 open import Data.List.Base as List
-  using (List; map; ap; []; _∷_; _++_; concat; concatMap)
+  using (List; map; ap; []; _∷_; singleton; _++_; concat; concatMap)
 open import Data.List.Properties
   using (++-identityʳ; ++-assoc; map-cong; concatMap-cong; map-concatMap
         ; concatMap-pure)
@@ -43,7 +43,7 @@ functor = record { _<$>_ = map }
 applicative : RawApplicative {ℓ} List
 applicative = record
   { rawFunctor = functor
-  ; pure = List.pure
+  ; pure = singleton
   ; _<*>_  = ap
   }
 
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index e2fbe0f1f4..1b67ab6925 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -13,7 +13,7 @@ open import Data.Bool.ListAction using (any)
 open import Data.Bool.Properties using (T-∨; T-≡)
 open import Data.Empty using (⊥)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Data.List.Base as List hiding (find; and; or; all; any; pure)
+open import Data.List.Base as List hiding (find; and; or; all; any)
 open import Data.List.Effectful as List using (monad)
 open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
 open import Data.List.Membership.Propositional
diff --git a/src/Data/Tree/Binary.agda b/src/Data/Tree/Binary.agda
index 037e879695..6ec5ddadf3 100644
--- a/src/Data/Tree/Binary.agda
+++ b/src/Data/Tree/Binary.agda
@@ -10,7 +10,8 @@ module Data.Tree.Binary where
 
 open import Level using (Level; _⊔_)
 open import Data.List.Base using (List)
-open import Data.DifferenceList as DiffList using (DiffList; []; _∷_; _∷ʳ_; _++_; [_])
+open import Data.DifferenceList as DiffList
+  using (DiffList; []; _∷_; _∷ʳ_; _++_)
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Function.Base
 
@@ -80,7 +81,7 @@ module Suffix where
 module Leaves where
 
   toDiffList : Tree N L → DiffList L
-  toDiffList (leaf x)     = [ x ]
+  toDiffList (leaf x)     = DiffList.[ x ]
   toDiffList (node l m r) = toDiffList l ++ toDiffList r
 
   toList : Tree N L → List L
diff --git a/src/IO.agda b/src/IO.agda
index a3d3702631..20262162e7 100644
--- a/src/IO.agda
+++ b/src/IO.agda
@@ -35,6 +35,7 @@ open import IO.Handle public
 module Colist where
 
   open import Codata.Musical.Colist.Base
+    using (Colist; []; _∷_; map)
 
   sequence : Colist (IO A) → IO (Colist A)
   sequence []       = pure []
@@ -63,7 +64,8 @@ module Colist where
 
 module List where
 
-  open import Data.List.Base hiding (pure)
+  open import Data.List.Base
+    using (List; []; _∷_; map)
 
   sequence : List (IO A) → IO (List A)
   sequence []       = ⦇ [] ⦈
diff --git a/src/Text/Format/Generic.agda b/src/Text/Format/Generic.agda
index 29a1756fe1..50b8580871 100644
--- a/src/Text/Format/Generic.agda
+++ b/src/Text/Format/Generic.agda
@@ -11,7 +11,7 @@ module Text.Format.Generic where
 open import Level using (0ℓ)
 open import Effect.Applicative
 open import Data.Char.Base using (Char)
-open import Data.List.Base as List hiding (sum; pure)
+open import Data.List.Base as List hiding (sum)
 open import Data.Maybe.Base as Maybe
 open import Data.Nat.Base
 open import Data.Nat.ListAction using (sum)