title: Creating a completely dependent concatenation
body: <p>A nice true fact about concatenation is that if I know any two variables in the equation:</p>
  
  <pre><code>a ++ b = c
  </code></pre>
  
  <p>Then I know the third.</p>
  
  <p>I would like to capture this idea in my own concat so I use a functional dependency.  </p>
  
  <pre><code>{-# Language DataKinds, GADTs, FlexibleContexts, FlexibleInstances, FunctionalDependencies, KindSignatures, PolyKinds, TypeOperators, UndecidableInstances #-}
  import Data.Kind (Type)
  
  class Concatable
     (m  :: k -&gt; Type)
     (as :: k)
     (bs :: k)
     (cs :: k)
     | as bs -&gt; cs
     , as cs -&gt; bs
     , bs cs -&gt; as
     where
       concat' :: m as -&gt; m bs -&gt; m cs
  </code></pre>
  
  <p>Now I conjure heterogeneous list like so:</p>
  
  <pre><code>data HList ( as :: [ Type ] ) where
    HEmpty :: HList '[]
    HCons  :: a -&gt; HList as -&gt; HList (a ': as)
  </code></pre>
  
  <p>But when I try to declare these as <code>Concatable</code> I have an issue</p>
  
  <pre><code>instance Concatable HList '[] bs bs where
    concat' HEmpty bs = bs
  instance
    ( Concatable HList as bs cs
    )
      =&gt; Concatable HList (a ': as) bs (a ': cs)
    where
      concat' (HCons head tail) bs = HCons head (concat' tail bs)
  </code></pre>
  
  <p>I don't satisfy my third functional dependency.  Or rather the compiler believes we do not.
  This is because the compiler believes that in our second instance it might be the case that <code>bs ~ (a ': cs)</code>.  And it could be the case if <code>Concatable as (a ': cs) cs</code>.</p>
  
  <p>How can I adjust my instances so that all three of the dependencies are satisfied?</p>