如何为GADT编写遍历？

Question

是否可以为GADT编写Traversal？我有：

{-# LANGUAGE TypeInType, GADTs, TypeFamilies, RankNTypes #-}

module GADT where

import Data.Kind

data Tag = TagA | TagB

data family Tagged (tag :: Tag)

data Foo (tag :: Maybe Tag) where
    Foo       :: Int -> Foo Nothing
    FooTagged :: Int -> Tagged tag -> Foo (Just tag)

我想编写Tagged tag字段的遍历。我试过：

type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s

tagged :: forall mt t. Traversal' (Foo mt) (Tagged t)
tagged _  foo@(Foo         _) = pure foo
tagged fn foo@(FooTagged i t) = fmap (\t' -> FooTagged i t') (fn t)

但它失败了：

* Could not deduce: tag ~ t
      from the context: mt ~ 'Just tag
        bound by a pattern with constructor:
                   FooTagged :: forall (tag :: Tag).
                                Int -> Tagged tag -> Foo ('Just tag),
                 in an equation for `tagged'
        at gadt.hs:19:16-28
      `tag' is a rigid type variable bound by
        a pattern with constructor:
          FooTagged :: forall (tag :: Tag).
                       Int -> Tagged tag -> Foo ('Just tag),
        in an equation for `tagged'
        at gadt.hs:19:16-28
      `t' is a rigid type variable bound by
        the type signature for:
          tagged :: forall (mt :: Maybe Tag) (t :: Tag).
                    Traversal' (Foo mt) (Tagged t)
        at gadt.hs:17:1-53
      Expected type: Tagged t
        Actual type: Tagged tag
    * In the first argument of `fn', namely `t'
      In the second argument of `fmap', namely `(fn t)'
      In the expression: fmap (\ t' -> FooTagged i t') (fn t)
    * Relevant bindings include
        t :: Tagged tag (bound at gadt.hs:19:28)
        fn :: Tagged t -> f (Tagged t) (bound at gadt.hs:19:8)
        tagged :: (Tagged t -> f (Tagged t)) -> Foo mt -> f (Foo mt)
          (bound at gadt.hs:18:1)
   |
19 | tagged fn foo@(FooTagged i t) = fmap (\t' -> FooTagged i t') (fn t)
   |                                                                  ^

如何证明mt ~ Just t在没有unsafeCoerce的FooTagged情况下

更新：

使用类型家族来指定遍历的焦点似乎是可行的：

type Traversal' s a = forall f. Applicative f => (a -> f a) -> s -> f s

type family TaggedType (m :: Maybe Tag) :: Type where
    TaggedType ('Just a) = Tagged a
    TaggedType 'Nothing  = ()

tagged :: forall mt. Traversal' (Foo mt) (TaggedType mt)
tagged _  foo@(Foo         _) = pure foo
tagged fn foo@(FooTagged i t) = fmap (\t' -> FooTagged i t') (fn t)

还有其他解决办法吗？

更新2:

在最后一个子句中，可能应该是TaggedType 'Nothing = Void而不是TaggedType 'Nothing = ()。

Answer 1

这是用AllowAmbiguousTypes编译的。不过，我对这段代码有点怀疑，因为我无法清楚地看到它将如何使用。

type family FromMaybe (t :: Tag) (x :: Maybe Tag) :: Tag where
  FromMaybe _ (Just tag) = tag
  FromMaybe t _          = t  

tagged :: forall mt t. Traversal' (Foo mt) (Tagged (FromMaybe t mt))
tagged _  foo@(Foo         _) = pure foo
tagged fn foo@(FooTagged i t) = fmap (\t' -> FooTagged i t') (fn t)