diff --git a/CHANGELOG.md b/CHANGELOG.md
index eb838bcbe1..2cda2e9025 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -147,6 +147,11 @@ 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 `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`
   counterparts. Consider using `viaList` if you want a lawful lifting
diff --git a/src/Data/DifferenceList/Base.agda b/src/Data/DifferenceList/Base.agda
index 73c15d0ef9..88bdfc2014 100644
--- a/src/Data/DifferenceList/Base.agda
+++ b/src/Data/DifferenceList/Base.agda
@@ -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/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/Base.agda b/src/Data/List/Base.agda
index 79b87608d3..940472f999 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 ∷ []
+singleton : A → List A
+singleton = [_]
 
 fromMaybe : Maybe A → List A
 fromMaybe (just x) = [ x ]
diff --git a/src/Data/List/Effectful.agda b/src/Data/List/Effectful.agda
index 874dc68205..c7fd87dfca 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; []; _∷_; 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 = [_]
+  ; pure = singleton
   ; _<*>_  = ap
   }
 
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/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/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 = []
diff --git a/src/IO.agda b/src/IO.agda
index 90b25d1c07..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 []
@@ -64,6 +65,7 @@ module Colist where
 module List where
 
   open import Data.List.Base
+    using (List; []; _∷_; map)
 
   sequence : List (IO A) → IO (List A)
   sequence []       = ⦇ [] ⦈