diff --git a/clash-lib/src/Clash/Core/TermLiteral.hs b/clash-lib/src/Clash/Core/TermLiteral.hs
index 22a4f9214e..1907e22fb1 100644
--- a/clash-lib/src/Clash/Core/TermLiteral.hs
+++ b/clash-lib/src/Clash/Core/TermLiteral.hs
@@ -52,7 +52,7 @@ import           Clash.Core.Term                 (Term(Literal, Data), collectAr
 import           Clash.Promoted.Nat
 import           Clash.Promoted.Nat.Unsafe
 import           Clash.Sized.Index               (Index)
-import           Clash.Sized.Vector              (Vec (Nil, Cons), fromList)
+import           Clash.Sized.Vector              (Vec (Nil, (:>)), fromList)
 import qualified Clash.Util.Interpolate          as I
 import qualified Clash.Verification.Internal     as Cv
 
@@ -193,7 +193,7 @@ instance (TermLiteral a, KnownNat n) => TermLiteral (Vec n a) where
       case constr of
         Data (MkData{dcName=Name{nameOcc}})
           | nameOcc == showt 'Nil -> Right []
-          | nameOcc == showt 'Cons ->
+          | nameOcc == showt '(:>) ->
             case lefts args of
               [_gadtProof, c0, cs0] -> do
                 c1 <- termToData @a c0
diff --git a/clash-lib/src/Clash/Core/Util.hs b/clash-lib/src/Clash/Core/Util.hs
index ea9c0533fc..251e258b3b 100644
--- a/clash-lib/src/Clash/Core/Util.hs
+++ b/clash-lib/src/Clash/Core/Util.hs
@@ -98,7 +98,7 @@ unsafeCoerceTy =
 
 -- | Create a vector of supplied elements
 mkVec :: DataCon -- ^ The Nil constructor
-      -> DataCon -- ^ The Cons (:>) constructor
+      -> DataCon -- ^ The (:>) constructor
       -> Type    -- ^ Element type
       -> Integer -- ^ Length of the vector
       -> [Term]  -- ^ Elements to put in the vector
@@ -128,7 +128,7 @@ mkVec nilCon consCon resTy = go
                    _ -> error "impossible"
 
 -- | Append elements to the supplied vector
-appendToVec :: DataCon -- ^ The Cons (:>) constructor
+appendToVec :: DataCon -- ^ The (:>) constructor
             -> Type    -- ^ Element type
             -> Term    -- ^ The vector to append the elements to
             -> Integer -- ^ Length of the vector
@@ -161,7 +161,7 @@ extractElems
   -> InScopeSet
   -- ^ (Superset of) in scope variables
   -> DataCon
-  -- ^ The Cons (:>) constructor
+  -- ^ The (:>) constructor
   -> Type
   -- ^ The element type
   -> Char
@@ -609,10 +609,10 @@ shouldSplit0 tcm (TyConApp tcNm tyArgs)
   -- Project the n'th value out of a vector
   --
   -- >>> mkVecSelector subj 0
-  -- case subj of Cons x xs -> x
+  -- case subj of x :> xs -> x
   --
   -- >>> mkVecSelector subj 2
-  -- case (case (case subj of Cons x xs -> xs) of Cons x xs -> xs) of Cons x xs -> x
+  -- case (case (case subj of x :> xs -> xs) of x :> xs -> xs) of x :> xs -> x
   mkVecSelector :: forall m . MonadUnique m => InScopeSet -> Term -> Integer -> m Term
   mkVecSelector is0 subj 0 =
     mkSelectorCase ($(curLoc) ++ "mkVecSelector") is0 tcm subj 2 1
diff --git a/clash-lib/src/Clash/Netlist.hs b/clash-lib/src/Clash/Netlist.hs
index 509dee4477..30a5f41b05 100644
--- a/clash-lib/src/Clash/Netlist.hs
+++ b/clash-lib/src/Clash/Netlist.hs
@@ -1056,10 +1056,10 @@ mkDcApplication declType [dstHType] bndr dc args = do
       Vector 0 _ -> return (HW.DataCon dstHType VecAppend [])
       Vector 1 _ -> case argExprsFiltered of
                       [e] -> return (HW.DataCon dstHType VecAppend [e])
-                      _ -> error $ $(curLoc) ++ "Unexpected number of arguments for `Cons`: " ++ showPpr args
+                      _ -> error $ $(curLoc) ++ "Unexpected number of arguments for `(:>)`: " ++ showPpr args
       Vector _ _ -> case argExprsFiltered of
                       [e1,e2] -> return (HW.DataCon dstHType VecAppend [e1,e2])
-                      _ -> error $ $(curLoc) ++ "Unexpected number of arguments for `Cons`: " ++ showPpr args
+                      _ -> error $ $(curLoc) ++ "Unexpected number of arguments for `(:>)`: " ++ showPpr args
       MemBlob _ _ ->
         case compare 6 (length argExprsFiltered) of
           EQ -> return (HW.DataCon dstHType (DC (dstHType,0)) argExprsFiltered)
diff --git a/clash-lib/src/Clash/Netlist/Util.hs b/clash-lib/src/Clash/Netlist/Util.hs
index 03c9c4a5b4..5dcc7ba710 100644
--- a/clash-lib/src/Clash/Netlist/Util.hs
+++ b/clash-lib/src/Clash/Netlist/Util.hs
@@ -538,7 +538,7 @@ mkADT builtInTranslation reprs m tyString tc args = case tyConDataCons (UniqMap.
 -- data Vec :: Nat -> Type -> Type
 --  where
 --   Nil  :: Vec 0 a
---   Cons :: forall m . (n ~ m + 1) => a -> Vec m a -> Vec n a
+--   (:>) :: forall m . (n ~ m + 1) => a -> Vec m a -> Vec n a
 --
 -- where we can generate a type for `m` when we know `n` (by doing `n-1`).
 --
diff --git a/clash-lib/src/Clash/Normalize/PrimitiveReductions.hs b/clash-lib/src/Clash/Normalize/PrimitiveReductions.hs
index f0dde3fabe..c348e5597e 100644
--- a/clash-lib/src/Clash/Normalize/PrimitiveReductions.hs
+++ b/clash-lib/src/Clash/Normalize/PrimitiveReductions.hs
@@ -184,7 +184,7 @@ vecTailTy vecNm =
 -- vector, the latter the tail.
 extractHeadTail
   :: DataCon
-  -- ^ The Cons (:>) constructor
+  -- ^ The (:>) constructor
   -> Type
   -- ^ Element type
   -> Integer
@@ -206,7 +206,7 @@ extractHeadTail consCon elTy n vec =
       in
         ( Case vec elTy [(pat, Var el)]
         , Case vec restTy [(pat, Var rest)] )
-    _ -> error "extractHeadTail: failed to instantiate Cons DC"
+    _ -> error "extractHeadTail: failed to instantiate (:>) DC"
  where
   tys = [(LitTy (NumTy n)), elTy, (LitTy (NumTy (n-1)))]
 
@@ -214,7 +214,7 @@ extractHeadTail consCon elTy n vec =
 mkVecCons
   :: HasCallStack
   => DataCon
-  -- ^ The Cons (:>) constructor
+  -- ^ The (:>) constructor
   -> Type
   -- ^ Element type
   -> Integer
@@ -235,7 +235,7 @@ mkVecCons consCon resTy n h t
                             , Left (primCo consCoTy)
                             , Left h
                             , Left t ]
-    _ -> error "mkVecCons: failed to instantiate Cons DC"
+    _ -> error "mkVecCons: failed to instantiate (:>) DC"
 
 -- | Create an empty vector
 mkVecNil
@@ -568,7 +568,7 @@ reduceTraverse n aTy fTy bTy dict fun arg (TransformContext is0 ctx) = do
 -- > (:>) <$> x0 <*> ((:>) <$> x1 <*> pure Nil)
 mkTravVec :: TyConName -- ^ Vec tcon
           -> DataCon   -- ^ Nil con
-          -> DataCon   -- ^ Cons con
+          -> DataCon   -- ^ (:>) con
           -> Term      -- ^ 'pure' term
           -> Term      -- ^ '<*>' term
           -> Term      -- ^ 'fmap' term
@@ -983,7 +983,7 @@ reduceUnconcat unconcatPrimInfo n m aTy _kn sm arg (TransformContext inScope _ct
                                   , Left (snd nextVec)
                                   ]
             -- let (mvec,nextVec) = splitAt sm arg
-            -- in Cons mvec (unconcat sm nextVec)
+            -- in mvec :> (unconcat sm nextVec)
             lBody = mkVecCons consCon innerVecTy n mvec nextUnconcat
             lb = Letrec lbs lBody
 
diff --git a/clash-lib/src/Clash/Normalize/Transformations/Case.hs b/clash-lib/src/Clash/Normalize/Transformations/Case.hs
index b23e8ca615..4ba0070986 100644
--- a/clash-lib/src/Clash/Normalize/Transformations/Case.hs
+++ b/clash-lib/src/Clash/Normalize/Transformations/Case.hs
@@ -670,8 +670,8 @@ caseOneAlt e = return e
 -- existential should be. For example, consider Vec:
 --
 --    data Vec :: Nat -> Type -> Type where
---      Nil       :: Vec 0 a
---      Cons x xs :: a -> Vec n a -> Vec (n + 1) a
+--      Nil     :: Vec 0 a
+--      x :> xs :: a -> Vec n a -> Vec (n + 1) a
 --
 -- Thus, 'null' (annotated with existentials) could look like:
 --
@@ -679,7 +679,7 @@ caseOneAlt e = return e
 --    null v =
 --      case v of
 --        Nil  {n ~ 0}                                     -> True
---        Cons {n1:Nat} {n~n1+1} (x :: a) (xs :: Vec n1 a) -> False
+--        (:>) {n1:Nat} {n~n1+1} (x :: a) (xs :: Vec n1 a) -> False
 --
 -- When it's applied to a vector of length 5, this becomes:
 --
@@ -687,7 +687,7 @@ caseOneAlt e = return e
 --    null v =
 --      case v of
 --        Nil  {5 ~ 0}                                     -> True
---        Cons {n1:Nat} {5~n1+1} (x :: a) (xs :: Vec n1 a) -> False
+--        (:>) {n1:Nat} {5~n1+1} (x :: a) (xs :: Vec n1 a) -> False
 --
 -- This function solves 'n1' and replaces every occurrence with its solution. A
 -- very limited number of solutions are currently recognized: only adds (such
diff --git a/clash-lib/src/Clash/Normalize/Transformations/Letrec.hs b/clash-lib/src/Clash/Normalize/Transformations/Letrec.hs
index eb8ef0b00c..c3b35f07a6 100644
--- a/clash-lib/src/Clash/Normalize/Transformations/Letrec.hs
+++ b/clash-lib/src/Clash/Normalize/Transformations/Letrec.hs
@@ -40,7 +40,7 @@ import qualified Data.Text.Extra as Text
 import GHC.Stack (HasCallStack)
 
 import Clash.Annotations.BitRepresentation.Deriving (dontApplyInHDL)
-import Clash.Sized.Vector as Vec (Vec(Cons), splitAt)
+import Clash.Sized.Vector as Vec (Vec((:>)), splitAt)
 
 import Clash.Annotations.Primitive (extractPrim)
 import Clash.Core.DataCon (DataCon(..))
@@ -151,9 +151,9 @@ removeUnusedExpr _ e@(Case _ _ [(DataPat _ [] xs,altExpr)]) =
      else return e
 
 -- Replace any expression that creates a Vector of size 0 within the application
--- of the Cons constructor, by the Nil constructor.
+-- of the (:>) constructor, by the Nil constructor.
 removeUnusedExpr _ e@(collectArgsTicks -> (Data dc, [_,Right aTy,Right nTy,_,Left a,Left nil],ticks))
-  | nameOcc (dcName dc) == Text.showt 'Vec.Cons
+  | nameOcc (dcName dc) == Text.showt '(Vec.:>)
   = do
     tcm <- Lens.view tcCache
     case runExcept (tyNatSize tcm nTy) of
diff --git a/clash-prelude/src/Clash/Explicit/SimIO.hs b/clash-prelude/src/Clash/Explicit/SimIO.hs
index d37df14a53..1beaf1eee1 100644
--- a/clash-prelude/src/Clash/Explicit/SimIO.hs
+++ b/clash-prelude/src/Clash/Explicit/SimIO.hs
@@ -279,9 +279,9 @@ getLine (File fp) (Reg r) = SimIO $ do
   return 0
  where
    rep :: String -> Vec m (Unsigned 8) -> Vec m (Unsigned 8)
-   rep []     vs          = vs
-   rep (x:xs) (Cons _ vs) = Cons (toEnum (fromEnum x)) (rep xs vs)
-   rep _      Nil         = Nil
+   rep []     vs        = vs
+   rep (x:xs) (_ :> vs) = toEnum (fromEnum x) :> rep xs vs
+   rep _      Nil       = Nil
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE getLine #-}
 {-# ANN getLine hasBlackBox #-}
diff --git a/clash-prelude/src/Clash/Sized/Vector.hs b/clash-prelude/src/Clash/Sized/Vector.hs
index 08af788a02..4c0c21b774 100644
--- a/clash-prelude/src/Clash/Sized/Vector.hs
+++ b/clash-prelude/src/Clash/Sized/Vector.hs
@@ -171,7 +171,7 @@ import Clash.XException           (ShowX (..), NFDataX (..), seqX, isX)
 
 #define CONS_PREC 5
 
-infixr CONS_PREC `Cons`
+infixr CONS_PREC :>
 -- | Fixed size vectors.
 --
 -- * Lists with their length encoded in their type
@@ -179,9 +179,7 @@ infixr CONS_PREC `Cons`
 --   ending at @'length' - 1@.
 data Vec :: Nat -> Type -> Type where
   Nil  :: Vec 0 a
-  Cons :: a -> Vec n a -> Vec (n + 1) a
-
-{-# COMPLETE Nil, (:>) #-}
+  (:>) :: a -> Vec n a -> Vec (n + 1) a
 
 -- | Tag for K1: @n ~ 0@ proof
 data N
@@ -197,7 +195,7 @@ instance KnownNat n => Generic (Vec n a) where
   type Rep (Vec n a) =
     D1 ('MetaData "Vec" "Clash.Data.Vector" "clash-prelude" 'False)
       (C1 ('MetaCons "Nil" 'PrefixI 'False) (K1 N (Dict (n ~ 0))) :+:
-       C1 ('MetaCons "Cons" 'PrefixI 'False)
+       C1 ('MetaCons "(:>)" 'PrefixI 'False)
         (S1 ('MetaSel 'Nothing
                 'NoSourceUnpackedness
                 'NoSourceStrictness
@@ -208,23 +206,23 @@ instance KnownNat n => Generic (Vec n a) where
                 'NoSourceStrictness
                 'DecidedLazy)
             (Rec0 (Vec (n-1) a))))
-  from Nil         = M1 (L1 (M1 (K1 Dict)))
-  from (Cons x xs) = M1 (R1 (M1 (M1 (K1 x) :*: M1 (K1 xs))))
+  from Nil       = M1 (L1 (M1 (K1 Dict)))
+  from (x :> xs) = M1 (R1 (M1 (M1 (K1 x) :*: M1 (K1 xs))))
   to (M1 g) = case compareSNat (SNat @n) (SNat @0) of
     SNatLE -> case leZero @n of
       Sub Dict -> Nil
     SNatGT -> case g of
-      R1 (M1 (M1 (K1 p) :*: M1 (K1 q))) -> Cons p q
+      R1 (M1 (M1 (K1 p) :*: M1 (K1 q))) -> p :> q
       L1 (M1 (K1 eqZero)) -> case eqZero of {}
 
 instance (KnownNat n, Typeable a, Data a) => Data (Vec n a) where
   gunfold k z _ = case compareSNat (SNat @n) (SNat @0) of
     SNatLE -> case leZero @n of
       Sub Dict -> z Nil
-    SNatGT -> k (k (z @(a -> Vec (n-1) a -> Vec n a) Cons))
-  toConstr Nil        = cNil
-  toConstr (Cons _ _) = cCons
-  dataTypeOf _        = tVec
+    SNatGT -> k (k (z @(a -> Vec (n-1) a -> Vec n a) (:>)))
+  toConstr Nil      = cNil
+  toConstr (_ :> _) = cCons
+  dataTypeOf _      = tVec
 
   gfoldl
     :: (forall d b. Data d => c (d -> b) -> d -> c b)
@@ -244,7 +242,7 @@ cNil :: Constr
 cNil = mkConstr tVec "Nil" [] Prefix
 
 cCons :: Constr
-cCons = mkConstr tVec "Cons" [] Prefix
+cCons = mkConstr tVec ":>" [] Infix
 
 instance NFData a => NFData (Vec n a) where
   rnf = foldl (\() -> rnf) ()
@@ -255,29 +253,40 @@ instance NFData a => NFData (Vec n a) where
 -- 3 :> 4 :> 5 :> Nil
 -- >>> let x = 3:>4:>5:>Nil
 -- >>> :t x
--- x :: Num a => Vec 3 a
+-- x :: Num b => Vec 3 b
 --
 -- Can be used as a pattern:
 --
--- >>> let f (x :> y :> _) = x + y
--- >>> :t f
--- f :: Num a => Vec ((n + 1) + 1) a -> a
+-- >>> :{
+-- f :: Num a => Vec (n + 2) a -> a
+-- f (x :> y :> _) = x + y
+-- :}
+--
 -- >>> f (3:>4:>5:>6:>7:>Nil)
 -- 7
 --
 -- Also in conjunctions with (':<'):
 --
--- >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
--- >>> :t g
--- g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
+-- >>> :{
+-- g :: Num a => Vec (n + 4) a -> a
+-- g (a :> b :> (_ :< y :< x)) = a + b + x + y
+-- :}
+--
 -- >>> g (1:>2:>3:>4:>5:>Nil)
 -- 12
-pattern (:>) :: a -> Vec n a -> Vec (n + 1) a
-pattern (:>) x xs <- ((\ys -> (head ys,tail ys)) -> (x,xs))
-  where
-    (:>) x xs = Cons x xs
+pattern Cons ::
+#if MIN_VERSION_base(4,15,0)
+  forall {n} a. () =>
+#else
+  forall n a. () =>
+#endif
+  forall m. n ~ (m + 1) =>
+  a -> Vec m a -> Vec n a
+pattern Cons x xs = (:>) x xs
 
-infixr CONS_PREC :>
+infixr CONS_PREC `Cons`
+{-# COMPLETE Nil, Cons #-}
+{-# DEPRECATED Cons "Use '(:>)' instead. 'Cons' will be removed in Clash 1.12" #-}
 
 instance Show a => Show (Vec n a) where
   showsPrec n = \case
@@ -287,7 +296,7 @@ instance Show a => Show (Vec n a) where
    where
     go :: Vec m a -> ShowS
     go Nil = showString "Nil"
-    go (x `Cons` xs) =
+    go (x :> xs) =
         showsPrec (CONS_PREC + 1) x
       . showString " :> "
       . go xs
@@ -302,14 +311,14 @@ instance ShowX a => ShowX (Vec n a) where
     go :: Vec m a -> ShowS
     go (isX -> Left _) = showString "undefined"
     go Nil = showString "Nil"
-    go (x `Cons` xs) =
+    go (x :> xs) =
         showsPrecX (CONS_PREC + 1) x
       . showString " :> "
       . go xs
 
 instance (KnownNat n, Eq a) => Eq (Vec n a) where
   (==) Nil _            = True
-  (==) v1@(Cons _ _) v2 = fold (&&) (zipWith (==) v1 v2)
+  (==) v1@(_ :> _) v2 = fold (&&) (zipWith (==) v1 v2)
 
 instance (KnownNat n, Ord a) => Ord (Vec n a) where
   compare x y = foldr f EQ $ zipWith compare x y
@@ -332,28 +341,28 @@ instance KnownNat n => Applicative (Vec n) where
   #-}
 
 instance KnownNat n => F.Foldable (Vec n) where
-  fold Nil      = mempty
-  fold z@Cons{} = fold mappend z
-  foldMap _ Nil      = mempty
-  foldMap f z@Cons{} = fold mappend (map f z)
+  fold Nil        = mempty
+  fold z@(_ :> _) = fold mappend z
+  foldMap _ Nil        = mempty
+  foldMap f z@(_ :> _) = fold mappend (map f z)
   foldr     = foldr
   foldl     = foldl
-  foldr1 _ Nil      = clashCompileError "foldr1: empty Vec"
-  foldr1 f z@Cons{} = foldr1 f z
-  foldl1 _ Nil      = clashCompileError "foldl1: empty Vec"
-  foldl1 f z@Cons{} = foldl1 f z
+  foldr1 _ Nil        = clashCompileError "foldr1: empty Vec"
+  foldr1 f z@(_ :> _) = foldr1 f z
+  foldl1 _ Nil        = clashCompileError "foldl1: empty Vec"
+  foldl1 f z@(_ :> _) = foldl1 f z
   toList    = toList
   null Nil  = True
   null _    = False
   length    = length
-  maximum Nil      = clashCompileError "maximum: empty Vec"
-  maximum z@Cons{} = fold (\x y -> if x >= y then x else y) z
-  minimum Nil      = clashCompileError "minimum: empty Vec"
-  minimum z@Cons{} = fold (\x y -> if x <= y then x else y) z
-  sum Nil      = 0
-  sum z@Cons{} = fold (+) z
-  product Nil      = 1
-  product z@Cons{} = fold (*) z
+  maximum Nil        = clashCompileError "maximum: empty Vec"
+  maximum z@(_ :> _) = fold (\x y -> if x >= y then x else y) z
+  minimum Nil        = clashCompileError "minimum: empty Vec"
+  minimum z@(_ :> _) = fold (\x y -> if x <= y then x else y) z
+  sum Nil        = 0
+  sum z@(_ :> _) = fold (+) z
+  product Nil        = 1
+  product z@(_ :> _) = fold (*) z
 
 #if MIN_VERSION_base(4,18,0)
 instance (KnownNat n, 1 <= n) => F1.Foldable1 (Vec n) where
@@ -375,8 +384,8 @@ instance KnownNat n => Traversable (Vec n) where
 {-# CLASH_OPAQUE traverse# #-}
 {-# ANN traverse# hasBlackBox #-}
 traverse# :: forall a f b n . Applicative f => (a -> f b) -> Vec n a -> f (Vec n b)
-traverse# _ Nil           = pure Nil
-traverse# f (x `Cons` xs) = Cons <$> f x <*> traverse# f xs
+traverse# _ Nil       = pure Nil
+traverse# f (x :> xs) = (:>) <$> f x <*> traverse# f xs
 
 instance (Default a, KnownNat n) => Default (Vec n a) where
   def = repeat def
@@ -395,7 +404,7 @@ instance (NFDataX a, KnownNat n) => NFDataX (Vec n a) where
    where
     go :: forall m b . (NFDataX b, KnownNat m) => Vec m b -> Bool
     go Nil = False
-    go (x `Cons` xs) = hasUndefined x || hasUndefined xs
+    go (x :> xs) = hasUndefined x || hasUndefined xs
 
   ensureSpine = map ensureSpine . lazyV
 
@@ -405,7 +414,7 @@ instance (NFDataX a, KnownNat n) => NFDataX (Vec n a) where
 -- >>> singleton 5
 -- 5 :> Nil
 singleton :: a -> Vec 1 a
-singleton = (`Cons` Nil)
+singleton = (:> Nil)
 
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE head #-}
@@ -451,12 +460,12 @@ singleton = (`Cons` Nil)
 #endif
 -}
 head :: Vec (n + 1) a -> a
-head (x `Cons` _) = x
+head (x :> _) = x
 #if !MIN_VERSION_base(4,16,0) || MIN_VERSION_base(4,17,0)
 head xs = unreachable xs
  where
   unreachable :: forall n a. 1 <= n => Vec n a -> a
-  unreachable (x `Cons` _) = x
+  unreachable (x :> _) = x
 #endif
 
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
@@ -503,12 +512,12 @@ head xs = unreachable xs
 #endif
 -}
 tail :: Vec (n + 1) a -> Vec n a
-tail (_ `Cons` xr) = xr
+tail (_ :> xr) = xr
 #if !MIN_VERSION_base(4,16,0) || MIN_VERSION_base(4,17,0)
 tail xs = unreachable xs
  where
   unreachable :: forall n a. 1 <= n => Vec n a -> Vec (n - 1) a
-  unreachable (_ `Cons` xr) = xr
+  unreachable (_ :> xr) = xr
 #endif
 
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
@@ -555,13 +564,13 @@ tail xs = unreachable xs
 #endif
 -}
 last :: Vec (n + 1) a -> a
-last (x `Cons` Nil)         = x
-last (_ `Cons` y `Cons` xr) = last (y `Cons` xr)
+last (x :> Nil)     = x
+last (_ :> y :> xr) = last (y :> xr)
 #if !MIN_VERSION_base(4,16,0) || MIN_VERSION_base(4,17,0)
 last xs = unreachable xs
  where
   unreachable :: 1 <= n => Vec n a -> a
-  unreachable ys@(Cons _ _) = last ys
+  unreachable ys@(_ :> _) = last ys
 #endif
 
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
@@ -608,13 +617,13 @@ last xs = unreachable xs
 #endif
 -}
 init :: Vec (n + 1) a -> Vec n a
-init (_ `Cons` Nil)         = Nil
-init (x `Cons` y `Cons` xr) = x `Cons` init (y `Cons` xr)
+init (_ :> Nil)     = Nil
+init (x :> y :> xr) = x :> init (y :> xr)
 #if !MIN_VERSION_base(4,16,0) || MIN_VERSION_base(4,17,0)
 init xs = unreachable xs
  where
   unreachable :: 1 <= n => Vec n a -> Vec (n - 1) a
-  unreachable ys@(Cons _ _) = init ys
+  unreachable ys@(_ :> _) = init ys
 #endif
 
 {-# INLINE shiftInAt0 #-}
@@ -675,9 +684,11 @@ infixl 5 :<
 --
 -- Also in conjunctions with (':>'):
 --
--- >>> let g (a :> b :> (_ :< y :< x)) = a + b +  x + y
--- >>> :t g
--- g :: Num a => Vec ((((n + 1) + 1) + 1) + 1) a -> a
+-- >>> :{
+-- g :: Num a => Vec (n + 4) a -> a
+-- g (a :> b :> (_ :< y :< x)) = a + b + x + y
+-- :}
+--
 -- >>> g (1:>2:>3:>4:>5:>Nil)
 -- 12
 pattern (:<) :: Vec n a -> a -> Vec (n+1) a
@@ -748,8 +759,8 @@ infixr 5 ++
 -- >>> (1:>2:>3:>Nil) ++ (7:>8:>Nil)
 -- 1 :> 2 :> 3 :> 7 :> 8 :> Nil
 (++) :: Vec n a -> Vec m a -> Vec (n + m) a
-Nil           ++ ys = ys
-(x `Cons` xs) ++ ys = x `Cons` xs ++ ys
+Nil       ++ ys = ys
+(x :> xs) ++ ys = x :> (xs ++ ys)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE (++) #-}
 {-# ANN (++) hasBlackBox #-}
@@ -769,7 +780,7 @@ splitAt n xs = splitAtU (toUNat n) xs
 splitAtU :: UNat m -> Vec (m + n) a -> (Vec m a, Vec n a)
 splitAtU UZero     ys = (Nil, ys)
 splitAtU (USucc s) ys = let (as, bs) = splitAtU s $ tail ys
-                        in  (head ys `Cons` as, bs)
+                        in  (head ys :> as, bs)
 
 -- | Split a vector into two vectors where the length of the two is determined
 -- by the context.
@@ -785,8 +796,8 @@ splitAtI = withSNat splitAt
 -- >>> concat ((1:>2:>3:>Nil) :> (4:>5:>6:>Nil) :> (7:>8:>9:>Nil) :> (10:>11:>12:>Nil) :> Nil)
 -- 1 :> 2 :> 3 :> 4 :> 5 :> 6 :> 7 :> 8 :> 9 :> 10 :> 11 :> 12 :> Nil
 concat :: Vec n (Vec m a) -> Vec (n * m) a
-concat Nil           = Nil
-concat (x `Cons` xs) = x ++ concat xs
+concat Nil       = Nil
+concat (x :> xs) = x ++ concat xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE concat #-}
 {-# ANN concat hasBlackBox #-}
@@ -813,7 +824,7 @@ unconcat n xs = unconcatU (withSNat toUNat) (toUNat n) xs
 unconcatU :: UNat n -> UNat m -> Vec (n * m) a -> Vec n (Vec m a)
 unconcatU UZero      _ _  = Nil
 unconcatU (USucc n') m ys = let (as,bs) = splitAtU m ys
-                            in  as `Cons` unconcatU n' m bs
+                            in  as :> unconcatU n' m bs
 
 -- | Split a vector of /(n * m)/ elements into a vector of \"vectors of length
 -- /m/\", where the length /m/ is determined by the context.
@@ -840,7 +851,7 @@ reverse :: Vec n a -> Vec n a
 reverse xs = go Nil xs
  where
   go :: i <= n => Vec (n - i) a -> Vec i a -> Vec n a
-  go a (y `Cons` ys) = go (y `Cons` a) ys
+  go a (y :> ys) = go (y :> a) ys
   go a Nil = a
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE reverse #-}
@@ -855,8 +866,8 @@ reverse xs = go Nil xs
 --
 -- <<doc/map.svg>>
 map :: (a -> b) -> Vec n a -> Vec n b
-map _ Nil           = Nil
-map f (x `Cons` xs) = f x `Cons` map f xs
+map _ Nil       = Nil
+map f (x :> xs) = f x :> map f xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE map #-}
 {-# ANN map hasBlackBox #-}
@@ -879,8 +890,8 @@ imap f = go 0
   where
     -- NOTE This has a black box called imap_go
     go :: Index n -> Vec m a -> Vec m b
-    go _ Nil           = Nil
-    go n (x `Cons` xs) = f n x `Cons` go (n+1) xs
+    go _ Nil       = Nil
+    go n (x :> xs) = f n x :> go (n+1) xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE imap #-}
 {-# ANN imap hasBlackBox #-}
@@ -943,7 +954,7 @@ ifoldr f z xs = head ws
 ifoldl :: KnownNat n => (a -> Index n -> b -> a) -> a -> Vec n b -> a
 ifoldl f z xs = last ws
   where
-    ws = z `Cons` izipWith (\i b a -> f a i b) xs (init ws)
+    ws = z :> izipWith (\i b a -> f a i b) xs (init ws)
 {-# INLINE ifoldl #-}
 
 -- | Generate a vector of indices.
@@ -1001,8 +1012,8 @@ elemIndex x = findIndex (x ==)
 -- third. This matters when 'zipWith' is used in a recursive setting. See
 -- 'lazyV' for more information.
 zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
-zipWith _ Nil           _  = Nil
-zipWith f (x `Cons` xs) ys = f x (head ys) `Cons` zipWith f xs (tail ys)
+zipWith _ Nil       _  = Nil
+zipWith f (x :> xs) ys = f x (head ys) :> zipWith f xs (tail ys)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE zipWith #-}
 {-# ANN zipWith hasBlackBox #-}
@@ -1112,8 +1123,8 @@ zipWith7 f ts us vs ws xs ys zs =
 -- associative, as @"'fold' f xs"@ produces a structure with a depth of
 -- O(log_2(@'length' xs@)).
 foldr :: (a -> b -> b) -> b -> Vec n a -> b
-foldr _ z Nil           = z
-foldr f z (x `Cons` xs) = f x (foldr f z xs)
+foldr _ z Nil       = z
+foldr f z (x :> xs) = f x (foldr f z xs)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE foldr #-}
 {-# ANN foldr hasBlackBox #-}
@@ -1153,7 +1164,7 @@ foldl f z0 xs0
  where
   go :: forall m. b -> Vec m a -> b
   go z Nil = z
-  go z (Cons x xs) =
+  go z (x :> xs) =
     let z1 = f z x
     in z1 `seq` go z1 xs
 {-# INLINE foldl #-}
@@ -1256,7 +1267,7 @@ fold f vs = fold' (toList vs)
 scanl :: (b -> a -> b) -> b -> Vec n a -> Vec (n + 1) b
 scanl f z xs = ws
   where
-    ws = z `Cons` zipWith (flip f) xs (init ws)
+    ws = z :> zipWith (flip f) xs (init ws)
 {-# INLINE scanl #-}
 
 -- | 'scanl' with no seed value
@@ -1341,7 +1352,7 @@ postscanr f z xs = init (scanr f z xs)
 mapAccumL :: (acc -> x -> (acc,y)) -> acc -> Vec n x -> (acc,Vec n y)
 mapAccumL f acc xs = (acc',ys)
   where
-    accs  = acc `Cons` accs'
+    accs  = acc :> accs'
     ws    = zipWith (flip f) xs (init accs)
     accs' = map fst ws
     ys    = map snd ws
@@ -1507,9 +1518,9 @@ index_int xs i@(I# n0)
                                     , " is larger than maximum index "
                                     , show ((length xs)-1)
                                     ])
-    sub (y `Cons` (!ys)) n = if isTrue# (n ==# 0#)
-                                then y
-                                else sub ys (n -# 1#)
+    sub (y :> (!ys)) n = if isTrue# (n ==# 0#)
+                         then y
+                         else sub ys (n -# 1#)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE index_int #-}
 {-# ANN index_int hasBlackBox #-}
@@ -1553,9 +1564,9 @@ replace_int xs i@(I# n0) a
                                       , " is larger than maximum index "
                                       , show (length xs - 1)
                                       ])
-    sub (y `Cons` (!ys)) n b = if isTrue# (n ==# 0#)
-                                 then b `Cons` ys
-                                 else y `Cons` sub ys (n -# 1#) b
+    sub (y :> (!ys)) n b = if isTrue# (n ==# 0#)
+                           then b :> ys
+                           else y :> sub ys (n -# 1#) b
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE replace_int #-}
 {-# ANN replace_int hasBlackBox #-}
@@ -1729,9 +1740,9 @@ select f s n xs = select' (toUNat n) $ drop f xs
   select' :: forall m j b. (s * m + 1 <= j + s) => UNat m -> Vec j b -> Vec m b
   select' m vs = case m of
     UZero -> Nil
-    USucc UZero -> head @(j - 1) vs `Cons` Nil
+    USucc UZero -> head @(j - 1) vs :> Nil
     USucc m'@(USucc _) -> case deduce @(s * (m - 1) + 1) @j Proxy Proxy of
-      Dict -> head @(j - 1) vs `Cons` select' m' (drop @s @(j - s) s vs)
+      Dict -> head @(j - 1) vs :> select' m' (drop @s @(j - s) s vs)
 
   deduce :: e + s <= k + s => p e -> p k -> Dict (e <= k)
   deduce _ _ = Dict
@@ -1767,7 +1778,7 @@ replicate n a = replicateU (toUNat n) a
 
 replicateU :: UNat n -> a -> Vec n a
 replicateU UZero     _ = Nil
-replicateU (USucc s) x = x `Cons` replicateU s x
+replicateU (USucc s) x = x :> replicateU s x
 
 -- | \"'repeat' @a@\" creates a vector with as many copies of /a/ as demanded
 -- by the context.
@@ -1808,7 +1819,7 @@ iterate SNat = iterateI
 iterateI :: forall n a. KnownNat n => (a -> a) -> a -> Vec n a
 iterateI f a = xs
   where
-    xs = init (a `Cons` ws)
+    xs = init (a :> ws)
     ws = map f (lazyV xs)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE iterateI #-}
@@ -1844,7 +1855,7 @@ unfoldr SNat = unfoldrI
 unfoldrI :: KnownNat n => (s -> (a,s)) -> s -> Vec n a
 unfoldrI f s0 = map fst xs
  where
-  xs = init (f s0 `Cons` ws)
+  xs = init (f s0 :> ws)
   ws = map (f . snd) (lazyV xs)
 {-# INLINE unfoldrI #-}
 
@@ -1900,7 +1911,7 @@ transpose = traverse# id
 --
 -- >>> let xs = (1:>2:>3:>4:>5:>6:>Nil)
 -- >>> :t xs
--- xs :: Num a => Vec 6 a
+-- xs :: Num b => Vec 6 b
 -- >>> :t stencil1d d2 sum xs
 -- stencil1d d2 sum xs :: Num b => Vec 5 b
 -- >>> stencil1d d2 sum xs
@@ -1922,7 +1933,7 @@ drawn from /xss/. The result matrix has /m + 1/ rows of /n + 1/ elements.
 
 >>> let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
 >>> :t xss
-xss :: Num a => Vec 4 (Vec 4 a)
+xss :: Num b => Vec 4 (Vec 4 b)
 
 #if __GLASGOW_HASKELL__ >= 902
 >>> :t stencil2d d2 d2 (sum . map sum) xss
@@ -1950,7 +1961,7 @@ stencil2d stY stX f xss = (map.map) f (windows2d stY stX xss)
 --
 -- >>> let xs = (1:>2:>3:>4:>5:>6:>Nil)
 -- >>> :t xs
--- xs :: Num a => Vec 6 a
+-- xs :: Num b => Vec 6 b
 -- >>> :t windows1d d2 xs
 -- windows1d d2 xs :: Num a => Vec 5 (Vec 2 a)
 -- >>> windows1d d2 xs
@@ -1972,7 +1983,7 @@ windows1d stX xs = map (take stX) (rotations xs)
 --
 -- >>> let xss = ((1:>2:>3:>4:>Nil):>(5:>6:>7:>8:>Nil):>(9:>10:>11:>12:>Nil):>(13:>14:>15:>16:>Nil):>Nil)
 -- >>> :t xss
--- xss :: Num a => Vec 4 (Vec 4 a)
+-- xss :: Num b => Vec 4 (Vec 4 b)
 -- >>> :t windows2d d2 d2 xss
 -- windows2d d2 d2 xss :: Num a => Vec 3 (Vec 3 (Vec 2 (Vec 2 a)))
 -- >>> windows2d d2 d2 xss
@@ -2134,9 +2145,9 @@ rotateLeftS :: KnownNat n
 rotateLeftS xs d = go (snatToInteger d `mod` natVal (asNatProxy xs)) xs
   where
     go :: Integer -> Vec k a -> Vec k a
-    go _ Nil           = Nil
-    go 0 ys            = ys
-    go n (y `Cons` ys) = go (n-1) (ys :< y)
+    go _ Nil       = Nil
+    go 0 ys        = ys
+    go n (y :> ys) = go (n-1) (ys :< y)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE rotateLeftS #-}
 {-# ANN rotateLeftS hasBlackBox #-}
@@ -2154,9 +2165,9 @@ rotateRightS :: KnownNat n
              -> Vec n a
 rotateRightS xs d = go (snatToInteger d `mod` natVal (asNatProxy xs)) xs
   where
-    go _ Nil            = Nil
-    go 0 ys             = ys
-    go n ys@(Cons _ _)  = go (n-1) (last ys :> init ys)
+    go _ Nil          = Nil
+    go 0 ys           = ys
+    go n ys@(_ :> _)  = go (n-1) (last ys :> init ys)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE rotateRightS #-}
 {-# ANN rotateRightS hasBlackBox #-}
@@ -2323,8 +2334,8 @@ lazyV :: KnownNat n
 lazyV = lazyV' (repeat ())
   where
     lazyV' :: Vec n () -> Vec n a -> Vec n a
-    lazyV' Nil           _  = Nil
-    lazyV' (_ `Cons` xs) ys = head ys `Cons` lazyV' xs (tail ys)
+    lazyV' Nil       _  = Nil
+    lazyV' (_ :> xs) ys = head ys :> lazyV' xs (tail ys)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE lazyV #-}
 {-# ANN lazyV hasBlackBox #-}
@@ -2384,7 +2395,7 @@ lazyV = lazyV' (repeat ())
 -- While the type of (':>') is:
 --
 -- >>> :t (:>)
--- (:>) :: a -> Vec n a -> Vec (n + 1) a
+-- (:>) :: b -> Vec n b -> Vec (n + 1) b
 --
 -- We thus need a @fold@ function that can handle the growing vector type:
 -- 'dfold'. Compared to 'foldr', 'dfold' takes an extra parameter, called the
@@ -2429,8 +2440,8 @@ dfold :: forall p k a . KnownNat k
 dfold _ f z xs = go (snatProxy (asNatProxy xs)) xs
   where
     go :: n <= k => SNat n -> Vec n a -> (p @@ n)
-    go _ Nil                        = z
-    go s (y `Cons` ys) =
+    go _ Nil       = z
+    go s (y :> ys) =
       let s' = s `subSNat` d1
       in  f s' y (go s' ys)
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
@@ -2611,8 +2622,8 @@ dtfold :: forall p k a . KnownNat k
 dtfold _ f g = go (SNat :: SNat k)
   where
     go :: forall n . SNat n -> Vec (2^n) a -> (p @@ n)
-    go _  (x `Cons` Nil) = f x
-    go sn xs@(Cons _ (Cons _ _)) =
+    go _  (x :> Nil) = f x
+    go sn xs@(_ :> (_ :> _)) =
       let sn' :: SNat (n - 1)
           sn'       = sn `subSNat` d1
           (xsL,xsR) = splitAt (pow2SNat sn') xs
@@ -2727,7 +2738,7 @@ concatBitVector# = go 0
  where
   go :: BitVector (n*m) -> Vec p (BitVector m) -> BitVector (n * m)
   go acc Nil = acc
-  go (BV accMsk accVal) ((BV xMsk xVal) `Cons` xs) =
+  go (BV accMsk accVal) ((BV xMsk xVal) :> xs) =
     let sh = fromInteger (natVal (Proxy @m)) :: Int in
     go (BV (shiftL accMsk sh .|. xMsk) (shiftL accVal sh .|. xVal)) xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
@@ -2820,8 +2831,8 @@ forceVX v =
 {-# INLINE forceVX #-}
 
 instance Lift a => Lift (Vec n a) where
-  lift Nil           = [| Nil |]
-  lift (x `Cons` xs) = [| x `Cons` $(lift xs) |]
+  lift Nil       = [| Nil |]
+  lift (x :> xs) = [| x :> $(lift xs) |]
 #if MIN_VERSION_template_haskell(2,16,0)
   liftTyped = liftTypedFromUntyped
 #endif
diff --git a/clash-prelude/src/Clash/Sized/Vector/ToTuple.hs b/clash-prelude/src/Clash/Sized/Vector/ToTuple.hs
index 7e7e92d9c7..adac72a2bc 100644
--- a/clash-prelude/src/Clash/Sized/Vector/ToTuple.hs
+++ b/clash-prelude/src/Clash/Sized/Vector/ToTuple.hs
@@ -51,7 +51,10 @@ class VecToTuple a where
   -- The following would produce a warning even though we can be sure
   -- no other pattern can ever apply:
   --
-  -- >>> (a :> b :> c :> Nil) = myVec
+  -- >>> :{
+  -- a, b, c :: Int
+  -- (a :> b :> c :> Nil) = myVec
+  -- :}
   --
   -- 'vecToTuple' can be used to work around the warning:
   --
diff --git a/clash-prelude/src/Clash/Tutorial.hs b/clash-prelude/src/Clash/Tutorial.hs
index ed9da61acb..023804bf59 100644
--- a/clash-prelude/src/Clash/Tutorial.hs
+++ b/clash-prelude/src/Clash/Tutorial.hs
@@ -2114,8 +2114,8 @@ Here is a list of Haskell features for which the Clash compiler has only
 
         @
         mapV :: (a -> b) -> Vec n a -> Vec n b
-        mapV _ Nil         = Nil
-        mapV f (Cons x xs) = Cons (f x) (mapV f xs)
+        mapV _ Nil       = Nil
+        mapV f (x :> xs) = f x :> mapV f xs
 
         topEntity :: Vec 4 Int -> Vec 4 Int
         topEntity = mapV (+1)
diff --git a/docs/developing-hardware/prelude.rst b/docs/developing-hardware/prelude.rst
index 555c35a9c9..d001715bc2 100644
--- a/docs/developing-hardware/prelude.rst
+++ b/docs/developing-hardware/prelude.rst
@@ -38,16 +38,6 @@ More generally, there is a ``Vec n a`` type which allows collections of
 arbitrary values to be used. These vectors are tagged with their length, to
 prevent out of bounds access at compile-time.
 
-.. warning::
-  The ``Vec n a`` type exports pattern synonyms for inserting at the left and
-  right of a vector. The types of the ``Cons`` constructor and ``(:>)`` pattern
-  are slightly different, and may behave differently in practice.
-
-  The ``Cons`` constructor has a more general type, allowing it to be used in
-  some cases where the pattern cannot be used. However, this additional power
-  comes at the cost of type inference. It is recommended that users use the
-  ``(:>)`` pattern by default, and only use ``Cons`` when necessary.
-
 Synthesis Domains
 -----------------
 
@@ -98,7 +88,7 @@ which can be used to define synchronous circuits. The first of these is
 
 .. _`Mealy machine`: https://en.wikipedia.org/wiki/Mealy_machine
 
-It is also possible to define a `Moore machine`_ using the ``moore`` function 
+It is also possible to define a `Moore machine`_ using the ``moore`` function
 in the Clash prelude. This differs to the Mealy machine by providing output
 based on the previous state (as oppoesd to the newly calculated state), and is
 specified by
@@ -169,4 +159,3 @@ changed to work with undefined values. Currently these are
   library. This allows evaluating values to normal form in code when undefined
   may be present. ``NFData`` can still be used, but will bubble up exceptions
   if undefined is encountered.
-
diff --git a/tests/shouldwork/Basic/T1316.hs b/tests/shouldwork/Basic/T1316.hs
index a5268d7c14..38620b253f 100644
--- a/tests/shouldwork/Basic/T1316.hs
+++ b/tests/shouldwork/Basic/T1316.hs
@@ -12,6 +12,6 @@ incr i = if i == maxBound then 0 else i + 1
 topEntity :: Index 10 -> Index 2
 topEntity j = case j < 1 of
   False ->
-    let xs = init (Cons 1 (Cons (incr (head xs)) Nil)) in last xs
+    let xs = init (1 :> (incr (head xs) :> Nil)) in last xs
   True ->
-    let ys = init (Cons 2 (Cons (incr (last ys)) Nil)) in head ys
+    let ys = init (2 :> (incr (last ys) :> Nil)) in head ys
diff --git a/tests/shouldwork/Basic/T1322.hs b/tests/shouldwork/Basic/T1322.hs
index c493a3712e..a77c08194f 100644
--- a/tests/shouldwork/Basic/T1322.hs
+++ b/tests/shouldwork/Basic/T1322.hs
@@ -14,18 +14,18 @@ topEntity :: Index 10 -> Index 3
 topEntity j = case j < 1 of
   False ->
     let xs :: Vec 1 (Index 3)
-        xs = init (Cons 1 (Cons (incr (head ys)) Nil))
+        xs = init (1 :> (incr (head ys) :> Nil))
         {-# NOINLINE xs #-}
         ys :: Vec 1 (Index 3)
-        ys = init (Cons 1 (Cons (incr (head xs)) Nil))
+        ys = init (1 :> (incr (head xs) :> Nil))
         {-# NOINLINE ys #-}
     in incr (incr (head xs))
   True ->
     let ys :: Vec 1 (Index 3)
-        ys = init (Cons 2 (Cons (incr (head xs)) Nil))
+        ys = init (2 :> (incr (head xs) :> Nil))
         {-# NOINLINE xs #-}
         xs :: Vec 1 (Index 3)
-        xs = init (Cons 2 (Cons (incr (head ys)) Nil))
+        xs = init (2 :> (incr (head ys) :> Nil))
         {-# NOINLINE ys #-}
     in incr (incr (head ys))
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
diff --git a/tests/shouldwork/Basic/T1340.hs b/tests/shouldwork/Basic/T1340.hs
index b13a88a0cf..c872589225 100644
--- a/tests/shouldwork/Basic/T1340.hs
+++ b/tests/shouldwork/Basic/T1340.hs
@@ -72,18 +72,14 @@ catLayout (BitLayout aBitCount aInFn aOutFn) (BitLayout bBitCount bInFn bOutFn)
   in BitLayout SNat inFn outFn
 
 vecLayout
-  :: forall n n' t
-  .  ( n' ~ (n - 1)
-     , 1 <= n
-     , KnownNat n
-     , KnownNat n' )
+  :: (1 <= n, KnownNat n)
   => Vec n (BitLayout t)
   -> BitLayout (Vec n t)
 vecLayout (BitLayout{..} :> others) = let
   headLayout = BitLayout SNat (headSigFn >>> inFn) (outFn >>> singletonSigFn)
   in case others of
-       Nil -> headLayout
-       _ -> headLayout `catLayout` vecLayout @n' others
+       Nil    -> headLayout
+       _ :> _ -> headLayout `catLayout` vecLayout others
 
 layout :: BitLayout (Vec Lanes Bit)
 layout = mkPos (0 :: Index (Lanes + 1))
diff --git a/tests/shouldwork/Basic/T1354B.hs b/tests/shouldwork/Basic/T1354B.hs
index ec1ca30ce8..ea9729d1b8 100644
--- a/tests/shouldwork/Basic/T1354B.hs
+++ b/tests/shouldwork/Basic/T1354B.hs
@@ -76,18 +76,14 @@ catLayout (BitLayout aBitCount aInFn aOutFn) (BitLayout bBitCount bInFn bOutFn)
   in BitLayout SNat inFn outFn
 
 vecLayout
-  :: forall n n' t
-  .  ( n' ~ (n - 1)
-     , 1 <= n
-     , KnownNat n
-     , KnownNat n' )
+  :: (1 <= n, KnownNat n)
   => Vec n (BitLayout t)
   -> BitLayout (Vec n t)
 vecLayout (BitLayout{..} :> others) = let
   headLayout = BitLayout SNat (headSigFn >>> inFn) (outFn >>> singletonSigFn)
   in case others of
-       Nil -> headLayout
-       _ -> headLayout `catLayout` vecLayout @n' others
+       Nil    -> headLayout
+       _ :> _ -> headLayout `catLayout` vecLayout others
 
 layout :: BitLayout (Vec Lanes Bit)
 layout = mkPos (0 :: Index (Lanes + 1))
diff --git a/tests/shouldwork/GADTs/Head.hs b/tests/shouldwork/GADTs/Head.hs
index 5ef2cd6aad..2b723d7f61 100644
--- a/tests/shouldwork/GADTs/Head.hs
+++ b/tests/shouldwork/GADTs/Head.hs
@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 head' :: Vec (n+1) (Signed 16) -> Signed 16
-head' (Cons x xs) = x
+head' (x :> xs) = x
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE head' #-}
 
diff --git a/tests/shouldwork/GADTs/HeadM.hs b/tests/shouldwork/GADTs/HeadM.hs
index 5da8827169..b23297f190 100644
--- a/tests/shouldwork/GADTs/HeadM.hs
+++ b/tests/shouldwork/GADTs/HeadM.hs
@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 head' :: Vec 3 (Signed 16) -> Signed 16
-head' (Cons x xs) = x
+head' (x :> xs) = x
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE head' #-}
 
diff --git a/tests/shouldwork/GADTs/Tail.hs b/tests/shouldwork/GADTs/Tail.hs
index 433287e111..ca254cd935 100644
--- a/tests/shouldwork/GADTs/Tail.hs
+++ b/tests/shouldwork/GADTs/Tail.hs
@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 tail' :: Vec (n+1) (Signed 16) -> Vec n (Signed 16)
-tail' (Cons x xs) = xs
+tail' (x :> xs) = xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE tail' #-}
 
diff --git a/tests/shouldwork/GADTs/TailM.hs b/tests/shouldwork/GADTs/TailM.hs
index 3112dbfeae..02fa50958f 100644
--- a/tests/shouldwork/GADTs/TailM.hs
+++ b/tests/shouldwork/GADTs/TailM.hs
@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 tail' :: Vec 3 (Signed 16) -> Vec 2 (Signed 16)
-tail' (Cons x xs) = xs
+tail' (x :> xs) = xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE tail' #-}
 
diff --git a/tests/shouldwork/GADTs/TailOfTail.hs b/tests/shouldwork/GADTs/TailOfTail.hs
index 73d61682b9..e9e9d3505b 100644
--- a/tests/shouldwork/GADTs/TailOfTail.hs
+++ b/tests/shouldwork/GADTs/TailOfTail.hs
@@ -6,7 +6,7 @@ import Clash.Prelude
 import Clash.Explicit.Testbench
 
 tailOfTail :: Vec (n+2) (Signed 16) -> Vec n (Signed 16)
-tailOfTail (Cons _ (Cons _ xs)) = xs
+tailOfTail (_ :> (_ :> xs)) = xs
 -- See: https://github.com/clash-lang/clash-compiler/pull/2511
 {-# CLASH_OPAQUE tailOfTail #-}
 
diff --git a/tests/shouldwork/Issues/T2542.hs b/tests/shouldwork/Issues/T2542.hs
index b839141ad8..5c1c294aba 100644
--- a/tests/shouldwork/Issues/T2542.hs
+++ b/tests/shouldwork/Issues/T2542.hs
@@ -9,7 +9,7 @@ import Clash.Prelude
 
 topEntity :: (Index 2, Index 2)
 topEntity = case reverse (indicesI @2) of
-  (a `Cons` b `Cons` Nil) -> (a,b)
+  (a :> b :> Nil) -> (a,b)
 
 assertIn :: String -> String -> IO ()
 assertIn needle haystack
diff --git a/tests/shouldwork/Numbers/HalfAsBlackboxArg.hs b/tests/shouldwork/Numbers/HalfAsBlackboxArg.hs
index e2b7b34ce9..87031b24ad 100644
--- a/tests/shouldwork/Numbers/HalfAsBlackboxArg.hs
+++ b/tests/shouldwork/Numbers/HalfAsBlackboxArg.hs
@@ -9,7 +9,7 @@ g :: KnownNat n => Vec n Half -> Half
 g v =
   case v of
     Nil -> Half 5
-    Cons a as -> a
+    a :> as -> a
 
 topEntity =
   ( g (replicate d3 (Half 7))