"rewriting did not change type" 视觉上相同类型的错误

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)

视觉上 hswapMaybePreservesMapJust 的两个参数的相同左侧 map (\x1 => Just (g x1)) x 看起来很有希望应用 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)

我检查了并尝试使用 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

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.

为什么 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。

"rewriting did not change type" 视觉上相同类型的错误

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

functor

theorem-proving

idris