title: Haskell: Type inference when using Functional Dependencies with Type Families and GADTs
body: <p>I had to use a lot of extensions to create a safe representation for an embedded language in Haskell. At some point when I introduced mutual functional dependency, the type inference stopped to figure out the correct substitutions for type variables. See the example below:</p>
  
  <pre><code>-- create a bidirectional connection between Unit' and ()
  class Connect t r | t -&gt; r, r -&gt; t where
  data Unit'
  instance Connect Unit' () where
  
  -- define a GADT that has only a MyGADT Unit' instance
  data MyGADT t where
    MyGADT :: () -&gt; MyGADT Unit'
  
  class Clas a where
    type RetTyp a :: *
    eval' :: Connect (RetTyp a) r =&gt; a -&gt; r
  
  instance Clas (MyGADT t) where
    type RetTyp (MyGADT t) = t
    eval' (MyGADT a) = a -- cannot figure out that "a :: ()"
  </code></pre>
  
  <p>The interesting thing is that when I used a TypeFamily for <code>Connect</code> it was fine:</p>
  
  <pre><code>class Connect' t where
    type Repr t :: *
  
  instance Connect' Unit' where
    type Repr Unit' = ()
  
  class Clas' a where
    type RetTyp' a :: *
    eval'' :: Connect' (RetTyp a) =&gt; a -&gt; (Repr (RetTyp' a))
  
  instance Clas' (MyGADT t) where
    type RetTyp' (MyGADT t) = t
    eval'' (MyGADT a) = a -- ok
  </code></pre>
  
  <p>What is the difference between the type resolution in the two cases?</p>