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 tFooTagged의 경우를 unsafeCoerce없이?

는

UPDATE :

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) 

는 다른 솔루션이 있습니다

탐색의 초점을 지정하는 유형 제품군을 사용하여이 작동하는 것 같다?

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