With RebindableSyntax, ApplicativeDo should eliminate return/pure

In a module with -XApplicativeDo, -XRebindableSyntax, and local definitions for everything in the Functor-Applicative-Monad hierarchy, do-notation always desugars to "join (... (return ...))" (or /s/return/pure/). This forces the result to have at least the constraints of join, which in my case is "IxMonad m".

{-# LANGUAGE RebindableSyntax, ApplicativeDo #-}

module My where

-- straightforward definitions of fmap, pure, (<*>), join, return, (>>=), 
-- (>>) and fail in terms of IxFunctor, IxPointed, IxApplicative, IxMonad

fPure m = do
  a <- m
  b <- m
  pure (a, b)

fReturn m = do
  a <- m
  b <- m
  return (a, b)

According to -ddump-ds, these desugar to:

fPure :: IxMonad m => m k1 k1 a -> m k1 k1 (a, a)
fPure m = My.join ( My.(<*>) (My.fmap (\a b -> My.pure (a, b)) m) m )

fReturn :: IxMonad m => m k1 k1 a -> m k1 k1 (a, a)
fReturn m = My.join ( My.(<*>) (My.fmap (\a b -> My.return (a, b)) m) m )

But I would expect:

fPure m = My.(<*>) (My.fmap (\a b -> (a, b)) m) m

fReturn m = -- same

It appears that when "return" is not from base, ApplicativeDo only partially desugars to the specification, and the final "return" or "pure" remains in the output.