Ok so I implemented both ideas:

elem2 _ [] = False elem2 x [y,: ys] = x == y || elem2 x ys

let [x,y,z,w,: ws] = "hello there" in ws -- yields "o there"

In fact it was easier to implement both ideas than make a special case of `(:)`. So these work

let [x,:+ xs] = [1,2,3,:+ Nily] in xs

let [x,`ConsSet` xs] = [1,2,3,`ConsSet` NilSet] in xs

with decls

infixr 5 :+ data Listy a = Nily | a :+ (Listy a) deriving (Eq, Show, Read)

infixr 5 `ConsSet` data Set a = NilSet | ConsSet a (Set a) deriving (Eq, Show, Read)

On Wed, 30 Jun 2021 at 19:00, Anthony Clayden wrote:

Ok thank you for the feedback, I get the message not to re-purpose currently valid syntax.

...

[x, y ,: ys ] -- ? not currently valid

We could make list syntax work harder

...

[x, y ,:+ ys ]

Means desugar the commas by applying constructor `:+` instead of `:`. That could be in general any constructor starting `:`.

Or indeed could be a pattern synonym starting `:`, which is a 'smart constructor' to build the list maintaining some invariant.