Как написать Traversal для GADT?

Question

Можно ли написать 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 в FooTagged дело без unsafeCoerce?

ОБНОВИТЬ:

Использование семейства типов для указания фокуса обхода, кажется, работает:

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)