haskell - kind :: '[SomeDataKind] で再帰的な GADT を処理する方法

Question

これは、Haskell の型システムの拡張に最も深く関わっていると思いますが、理解できないエラーに遭遇しました。長さについて前もってお詫び申し上げます。これは、私が抱えている問題を説明するために作成できる最も短い例です。次のような昇格されたリストである再帰的 GADT があります。

GADTの定義

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}

data DataKind = A | B | C

-- 'parts' should always contain at least 1 element which is enforced by the GADT.
-- Lets call the first piece of data 'val' and the second 'subdata'.
-- All data constructors have these 2 fields, although some may have
-- additional fields which I've omitted for simplicity.
data SomeData (parts :: [DataKind]) where
    MkA :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('A ': subparts)
    MkB :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('B ': subparts)
    MkC :: Maybe Char -> Maybe (SomeData subparts) -> SomeData ('C ': subparts)
deriving instance Show (SomeData parts)

問題

私がやろうとしているのは、データをトラバースしていくつかの操作を実行することです。たとえば、最初Just Charに見つかったものを一番上に伝播します。

不足している厄介な機能 - 次のセクションで必要

さて、明らかに GADT ( https://ghc.haskell.org/trac/ghc/ticket/2595 ) のレコード構文サポートがないため、手動で記述する必要があります。

getVal :: SomeData parts -> Maybe Char
getVal (MkA val _) = val
getVal (MkB val _) = val
getVal (MkC val _) = val

-- The lack of record syntax for GADTs is annoying.
updateVal :: Maybe Char -> SomeData parts -> SomeData parts
updateVal val (MkA _val sub) = MkA val sub
updateVal val (MkB _val sub) = MkB val sub
updateVal val (MkC _val sub) = MkC val sub

-- really annoying...
getSubData :: SomeData (p ': rest) -> Maybe (SomeData rest)
getSubData (MkA _ sub) = sub
getSubData (MkB _ sub) = sub
getSubData (MkC _ sub) = sub

テストデータ

だから、私がやりたいこと。という値が見つかるまで、構造を上から下に歩いていきますJust。したがって、次の初期値が与えられます。

a :: SomeData '[ 'A ]
a = MkA (Just 'A') Nothing

b :: SomeData '[ 'B ]
b = MkB (Just 'B') Nothing

c :: SomeData '[ 'C ]
c = MkC (Just 'C') Nothing

bc :: SomeData '[ 'B, 'C ]
bc = MkB Nothing (Just c)

abc :: SomeData '[ 'A, 'B, 'C ]
abc = MkA Nothing (Just bc)

期待される結果

私はこのようなものが欲しいです:

> abc
MkA Nothing (Just (MkB Nothing (Just (MkC (Just 'C') Nothing))))
> propogate abc
MkA (Just 'C') (Just (MkB (Just 'C') (Just (MkC (Just 'C') Nothing))))

以前の試み

最初に通常の関数を使用して、いくつか試してみました。

propogate sd =
    case getVal sd of
        Just _val ->
            sd
        Nothing ->
            let
                newSubData = fmap propogate (getSubData sd)
                newVal = join . fmap getVal $ newSubData
            in
                updateVal newVal sd

これにより、次のエラーが発生します。

Broken.hs:(70,1)-(81,35): error: …
    • Occurs check: cannot construct the infinite type: rest ~ p : rest
      Expected type: SomeData rest -> SomeData (p : rest)
        Actual type: SomeData (p : rest) -> SomeData (p : rest)
    • Relevant bindings include
        propogate :: SomeData rest -> SomeData (p : rest)
          (bound at Broken.hs:70:1)
Compilation failed.

また、型クラスを試し、構造を一致させようとしました:

class Propogate sd where
    propogateTypeClass :: sd -> sd

-- Base case: We only have 1 element in the promoted type list.
instance Propogate (SomeData parts) where
    propogateTypeClass sd = sd    

-- Recursie case: More than 1 element in the promoted type list.
instance Propogate (SomeData (p ': parts)) where
    propogateTypeClass sd =
        case getVal sd of
            Just _val ->
                sd
            Nothing ->
                let
                    -- newSubData :: Maybe subparts
                    -- Recurse on the subdata if it exists.
                    newSubData = fmap propogateTypeClass (getSubData sd)
                    newVal = join . fmap getVal $ newSubData
                in
                    updateVal newVal sd

これにより、次のエラーが発生します。

Broken.hs:125:5-26: error: …
    • Overlapping instances for Propogate (SomeData '['A, 'B, 'C])
        arising from a use of ‘propogateTypeClass’
      Matching instances:
        instance Propogate (SomeData parts)
          -- Defined at Broken.hs:91:10
        instance Propogate (SomeData (p : parts))
          -- Defined at Broken.hs:95:10
    • In the expression: propogateTypeClass abc
      In an equation for ‘x’: x = propogateTypeClass abc
Compilation failed.

SomeData '[]また、マッチングの組み合わせを試してみましたがSomeData '[p]、役に立ちませんでした。

単純なものが欠けていることを願っていますが、このような構造を処理する方法に関するドキュメントはどこにも見つかりませんでした.Haskell型システムであるかどうかを理解するのは今のところ限界です:)。繰り返しますが、長い投稿で申し訳ありません。どんな助けでも大歓迎です:)