How to write Traversal for GADT?

Question

Is it possible to write a Traversal for a GADT? I have:

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

I want to write traversal for Tagged tag field. I tried:

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)

but it fails:

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

How can I prove mt ~ Just t in FooTagged case without unsafeCoerce?

UPDATE:

Using type family to specify traversal's focus seems to work:

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)

Are there other solutions?

UPDATE 2:

It should probably be TaggedType 'Nothing = Void instead of TaggedType 'Nothing = () in the last clause there.

Answer 1

This compiles with AllowAmbiguousTypes. I am a bit suspicious of this code, though, because I can't clearly see how it will be used.

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)