title: Constraining on the transitive children of an ADT
body: <p>I'd like to be able to define trees using mutually inductive datatypes, and then write a generic function which can only run on certain parts of the tree, depending on what a node's descendants can be. So, for instance, if I had datatypes</p>
  
  <pre><code>data A = A1 B | A2 C D
  newtype B = B String
  newtype C = C String
  newtype D = D Int
  </code></pre>
  
  <p>I want to be able to define a <code>HasString</code> predicate and a function <code>getString</code> like this:</p>
  
  <pre><code>getString :: (HasString x) =&gt; x -&gt; String
  </code></pre>
  
  <p>such that <code>HasString</code> is satisfied for <code>A1</code>, <code>B</code>, and <code>C</code>, but not for <code>D</code>.</p>
  
  <p>The standard way to do this sort of thing is just with a manual traversal:</p>
  
  <pre><code>class GetString t where
    getString :: t -&gt; String
  
  instance GetString B where
      getString (B s) = s
  
  -- .... instances for A, C
  </code></pre>
  
  <p>In writing this out, we've basically created a proof that every <code>A</code> transitively contains a <code>String</code>.</p>
  
  <p>Now, I want to do this using generic machinery, so I can get it to run on datatypes other than <code>A</code>. And I care about things other than <code>getString</code> too.</p>
  
  <p>Currently, I can construct a type-level predicate that indicates whether a datatype transitively contains a <code>String</code>. I can even build it using generic proof machinery:</p>
  
  <pre><code>type family Or a b where
    Or True a = True
    Or a True = True
    Or a b    = False
  
  type family And a b where
    And True True = True
    And a    b    = False
  
  type family BaseHasString f where
    BaseHasString B = True
    BaseHasString C = True
    BaseHasString x = False
  
  type family Has f t where
    Has f A  = Or (f A) (And (Has f B) (Or (Has f C) (Has f D)))
    Has f x  = f x
  
  type HasString t :: Constraint = (Has BaseHasString t ~ True)
  </code></pre>
  
  <p>(I should also be able to generalize this further using GHC Generics.)</p>
  
  <p>However, now that I have my <code>HasString</code> predicate, I can't figure out how to actually use it.</p>
  
  <p>So, how can I write my <code>getString</code> function?</p>