"rewriting did not change type" error for visually same types

Question

I wrote a short function:

swapMaybe : Monad m => Maybe (m a) -> m (Maybe a)
swapMaybe Nothing = pure Nothing
swapMaybe (Just x) = map Just x

Then I tried to prove one of its properties:

import Interfaces.Verified

swapMaybePreservesMap : VerifiedMonad m => (g : a -> b) -> (x : Maybe (m a)) ->
                        swapMaybe (map (map g) x) = map (map g) (swapMaybe x)
swapMaybePreservesMap g Nothing = ?hswapMaybePreservesMapNothing
swapMaybePreservesMap g (Just x) = ?hswapMaybePreservesMapJust
    (functorComposition x g Just)
    (functorComposition x Just (map g))

:t hswapMaybePreservesMapJust gives following type:

  a : Type
  b : Type
  g : a -> b
  m : Type -> Type
  x : m a
  constraint : VerifiedMonad m
--------------------------------------
hswapMaybePreservesMapJust : (map (\x1 => Just (g x1)) x = map Just (map g x)) ->
                             (map (\x1 => Just (g x1)) x = map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x)) ->
                             map Just (map g x) = map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x)

Visually the same left side map (\x1 => Just (g x1)) x of both parameters of hswapMaybePreservesMapJust looks promising for applying rewrite.

However, it fails:

swapMaybePreservesMap g (Just x) = rewrite (functorComposition x g Just) in 
    (functorComposition x Just (map g))

The error:

When checking right hand side of swapMaybePreservesMap with expected type
        swapMaybe (map (map g) (Just x)) = map (map g) (swapMaybe (Just x))

rewriting map (\x1 => Just (g x1)) x to map Just (map g x) did not change type map Just (map g x) =
                                                                               map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x)

I checked this question and tried to explicitly specify the result type with the, moving rewrite parameters to let and eta-expand map g. Also without success, though:

swapEq : {x : a} -> {y : a} -> x = y -> y = x
swapEq eq = rewrite eq in Refl

swapMaybePreservesMap : VerifiedMonad n => (g : a -> b) -> (x : Maybe (n a)) ->
                        swapMaybe (map (\z => map g z) x) = map (\z => map g z) (swapMaybe x)
swapMaybePreservesMap g Nothing = ?hswapMaybePreservesMapNothing
swapMaybePreservesMap g xx@(Just x) = let
    pr1 = (swapEq $ functorComposition x g Just)
    pr2 = (functorComposition x Just (\z => map g z))
    in the (swapMaybe (map (\z => map g z) xx) = map (\z => map g z) (swapMaybe xx))
        (rewrite pr1 in pr2)

... with following message:

When checking right hand side of swapMaybePreservesMap with expected type
        swapMaybe (map (\z => map g z) (Just x)) = map (\z8 => map g z8) (swapMaybe (Just x))

When checking argument value to function Prelude.Basics.the:
        rewriting map Just (map g x) to map (\x1 => Just (g x1)) x did not change type map Just (map g x) =
                                                                                       map (\z11 => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g z11) (map Just x)

As I've read in the docs:

rewrite prf in expr

If we have prf : x = y, and the required type for expr is some property of x, the rewrite ... in syntax will search for x in the required type of expr and replace it with y.

Why rewrite is not working in this case?

Is it because of actually different values at the left side of the parameters (maybe some implicit parameters are not shown) or somethhing else? Maybe it's better to apply some Elab tactics script explicitly?

Answer 1

Finally I found the reason - it's different type constraints in swapMaybe and swapMaybePreservesMap. Following implementation gives a clear error:

swapMaybePreservesMap : VerifiedMonad m => (g : a -> b) -> (x : Maybe (m a)) ->
    swapMaybe (map (map g) x) = map (map g) (swapMaybe x)
swapMaybePreservesMap g Nothing = ?outOfScope
swapMaybePreservesMap g (Just x) = trans
    (sym $ functorComposition x g Just)
    (functorComposition x Just (map g))

The message:

When checking right hand side of swapMaybePreservesMap with expected type
        swapMaybe (map (map g) (Just x)) = map (map g) (swapMaybe (Just x))

When checking an application of function trans:
        Type mismatch between
                map (map g . Just) x = (map (map g) . map Just) x (Type of functorComposition x Just (map g))
        and
                map (\x1 => Just (g x1)) x = map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x) (Expected type)

        Specifically:
                Type mismatch between
                        map (map g) (map Just x)
                and
                        map (\meth => Prelude.Maybe implementation of Prelude.Functor.Functor, method map g meth) (map Just x)

Applying VerifiedMonad type constraint to swapMaybe instead of Monad makes type checker happy (with swapMaybePreservesMap implementation from above):

swapMaybe : Monad m => Maybe (m a) -> m (Maybe a)
swapMaybe Nothing = pure Nothing
swapMaybe (Just x) = map Just x

However, it'd be nice to prove some property of a function, working with some Monad, which holds only for VerifiedMonad.