视觉上相同类型的“重写没有改变类型”错误

Question

我写了一个简短的函数：

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

然后我试图证明它的一个属性：

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给出以下类型：

  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)

在视觉上，map (\x1 => Just (g x1)) x的两个参数的左侧hswapMaybePreservesMapJust看起来很有希望应用rewrite。

但是，它失败了：

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

错误：

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)

我检查了this question并试图用the明确指定结果类型，将rewrite参数移动到let和eta-expand map g。但也没有成功：

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)

......以下消息：

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)

正如我在docs中读到的那样：

rewrite prf in expr

如果我们有prf : x = y，并且expr所需的类型是x的某些属性，则rewrite ... in语法将在所需类型的x中搜索expr并将其替换为y。

为什么rewrite在这种情况下不起作用？

是因为参数左侧实际上有不同的值（可能没有显示某些隐式参数）还是其他的？也许最好明确地应用一些Elab战术脚本？

Answer 1

最后我找到了原因 - 它在swapMaybe和swapMaybePreservesMap中有不同的类型约束。以下实施给出了明确的错误：

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))

消息：

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)

将VerifiedMonad类型约束应用于swapMaybe而不是Monad使得类型检查器开心（使用上面的swapMaybePreservesMap实现）：

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

然而，证明一个函数的某些属性是很好的，使用一些Monad，它只适用于VerifiedMonad。