title: How to process a recursive GADT with kind :: '[SomeDataKind]
body: <p>I think this is the furthest into the Haskell type system extensions that I've even been and I've run into an error that I haven't been able to figure out. Apologies in advance for the length, it's the shortest example I could create that still illustrates the issue I'm having. I have a recursive GADT whose kind is a promoted list, something like the following:</p>
  
  <p><strong>GADT Definition</strong></p>
  
  <pre><code>{-# 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 -&gt; Maybe (SomeData subparts) -&gt; SomeData ('A ': subparts)
      MkB :: Maybe Char -&gt; Maybe (SomeData subparts) -&gt; SomeData ('B ': subparts)
      MkC :: Maybe Char -&gt; Maybe (SomeData subparts) -&gt; SomeData ('C ': subparts)
  deriving instance Show (SomeData parts)
  </code></pre>
  
  <p><strong>Problem</strong></p>
  
  <p>What I'm trying to do is traverse the data and perform some operations, for instance propagate the first <code>Just</code> <code>Char</code> found up to the top.</p>
  
  <p><strong>Annoying missing features - needed for the next section</strong></p>
  
  <p>Now, because there is apparently no record syntax support for GADTs (<a href="https://ghc.haskell.org/trac/ghc/ticket/2595" rel="nofollow noreferrer">https://ghc.haskell.org/trac/ghc/ticket/2595</a>) you need to write them manually, so here they are:</p>
  
  <pre><code>getVal :: SomeData parts -&gt; 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 -&gt; SomeData parts -&gt; 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) -&gt; Maybe (SomeData rest)
  getSubData (MkA _ sub) = sub
  getSubData (MkB _ sub) = sub
  getSubData (MkC _ sub) = sub
  </code></pre>
  
  <p><strong>Test Data</strong></p>
  
  <p>So, the thing I want to do. Walk down the structure from the top until I find a value that is <code>Just</code>. So given the following initial values:</p>
  
  <pre><code>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)
  </code></pre>
  
  <p><strong>Expected Result</strong></p>
  
  <p>I would like have something like this:</p>
  
  <pre><code>&gt; abc
  MkA Nothing (Just (MkB Nothing (Just (MkC (Just 'C') Nothing))))
  &gt; propogate abc
  MkA (Just 'C') (Just (MkB (Just 'C') (Just (MkC (Just 'C') Nothing))))
  </code></pre>
  
  <p><strong>Previous Attempts</strong></p>
  
  <p>I took a few stabs at it, first with a regular function:</p>
  
  <pre><code>propogate sd =
      case getVal sd of
          Just _val -&gt;
              sd
          Nothing -&gt;
              let
                  newSubData = fmap propogate (getSubData sd)
                  newVal = join . fmap getVal $ newSubData
              in
                  updateVal newVal sd
  </code></pre>
  
  <p>This gives the error:</p>
  
  <pre><code>Broken.hs:(70,1)-(81,35): error: …
      • Occurs check: cannot construct the infinite type: rest ~ p : rest
        Expected type: SomeData rest -&gt; SomeData (p : rest)
          Actual type: SomeData (p : rest) -&gt; SomeData (p : rest)
      • Relevant bindings include
          propogate :: SomeData rest -&gt; SomeData (p : rest)
            (bound at Broken.hs:70:1)
  Compilation failed.
  </code></pre>
  
  <p>I also tried a typeclass and attempting to match on the structure:</p>
  
  <pre><code>class Propogate sd where
      propogateTypeClass :: sd -&gt; 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 -&gt;
                  sd
              Nothing -&gt;
                  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
  </code></pre>
  
  <p>This results in the error:</p>
  
  <pre><code>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.
  </code></pre>
  
  <p>I've also tried combinations of matching on <code>SomeData '[]</code> and <code>SomeData '[p]</code> to no avail.</p>
  
  <p>I'm hoping I'm missing something simple but I haven't found documentation anywhere on how to process a structure like this and I'm at the limits of my understand if the Haskell type system, for now anyways :). Once again, sorry for the long post and any help would be greatly appreciated :)</p>