The two expressions

y >> pure x

liftM (const x) y

have the same type signature in Haskell.
I was curious whether they were equivalent, but I could neither produce a proof of the fact nor a counter example against it.

If we rewrite the two expressions so that we can eliminate the x and y then the question becomes whether the two following functions are equivalent

flip (>>) . pure

liftM . const

Note that both these functions have type Monad m => a -> m b -> m a.

I used the laws that Haskell gives for monad, applicatives, and functors to transform both statements into various equivalent forms, but I was not able to produce a sequence of equivalences between the two.

For instance I found that y >> pure x can be rewritten as follows

y >>= const (pure x)

y *> pure x

(id <$ y) <*> pure x

fmap (const id) y <*> pure x

and liftM (const x) y can be rewritten as follows

fmap (const x) y

pure (const x) <*> y

None of these spring out to me as necessarily equivalent, but I cannot think of any cases where they would not be equivalent.

The other answer gets there eventually, but it takes a long-winded route. All that is actually needed are the definitions of liftM, const, and a single monad law: m1 >> m2 and m1 >>= _ -> m2 must be semantically identical. (Indeed, this is the default implementation of (>>), and it is rare to override it.) Then:

liftM (const x) y

= { definition of liftM* }

y >>= z -> pure (const x z)

= { definition of const }

y >>= z -> pure x

= { monad law }

y >> pure x

* Okay, okay, so the actual definition of liftM uses return instead of pure. Whatever.

Yes they are the same

Let's start with flip (>>) . pure, which is the pointfree version of x >> pure y you provide:

flip (>>) . pure

It is the case that flip (>>) is just (=<<) . const so we can rewrite this as:

((=<<) . const) . pure

Since function composition ((.)) is associative we can write this as:

(=<<) . (const . pure)

Now we would like to rewrite const . pure. We can notice that const is just pure on (a ->), that means since pure . pure is fmap pure . pure, const . pure is (.) pure . const, ((.) is fmap for the functor (a ->)).

(=<<) . ((.) pure . const)

Now we associate again:

((=<<) . (.) pure) . const

((=<<) . (.) pure) is the definition for liftM¹ so we can substitute:

liftM . const

And that is the goal. The two are the same.

^{1: The definition of liftM is liftM f m1 = do { x1 <- m1; return (f x1) }, we can desugar the do into liftM f m1 = m1 >>= return . f. We can flip the (>>=) for liftM f m1 = return . f =<< m1 and elide the m1 to get liftM f = (return . f =<<) a little pointfree magic and we get liftM = (=<<) . (.) return}

One more possible route, exploiting the applicative laws:

For instance I found that y >> pure x can be rewritten as follows [...]

fmap (const id) y <*> pure x

That amounts to...

fmap (const id) y <*> pure x

pure ($ x) <*> fmap (const id) y -- interchange law of applicatives

fmap ($ x) (fmap (const id) y) -- fmap in terms of <*>

fmap (($ x) . const id) y -- composition law of functors

fmap (const x) y

... which, as you noted, is the same as liftM (const x) y.

That this route requires only applicative laws and not monad ones reflects how (*>) (another name for (>>)) is an Applicative method.