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 ]
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/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 []       = ⦇ [] ⦈
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)