title: Type errors with Existential types in Haskell
body: <p>I am struggling with existential types in my program. I think I'm trying to do something very reasonable however I cannot get past the typechecker :(</p>
  
  <p>I have a datatype that sort of mimics a Monad</p>
  
  <pre><code>data M o = R o | forall o1. B (o1 -&gt; M o) (M o1)
  </code></pre>
  
  <p>Now I create a Context for it, similar to that described in <a href="http://www.haskell.org/haskellwiki/Zipper">Haskell Wiki article on Zipper</a>, however I use a function instead of a data structure for simplicity -</p>
  
  <pre><code>type C o1 o2 = M o1 -&gt; M o2
  </code></pre>
  
  <p>Now when I try to write a function that splits a data value into its context and subvalue, the typechecker complains -</p>
  
  <pre><code>ctx :: M o -&gt; (M o1 -&gt; M o, M o1)
  ctx (B f m) = (B f, m) -- Doesn't typecheck
  </code></pre>
  
  <p>Error is -</p>
  
  <pre><code>Couldn't match type `o2' with `o1'
    `o2' is a rigid type variable bound by
         a pattern with constructor
           B :: forall o o1. (o1 -&gt; M o) -&gt; M o1 -&gt; M o,
         in an equation for `ctx'
         at delme1.hs:6:6
    `o1' is a rigid type variable bound by
         the type signature for ctx :: M o -&gt; (M o1 -&gt; M o, M o1)
         at delme1.hs:6:1
  Expected type: M o2
    Actual type: M o1
  In the expression: m
  In the expression: (B f, m)
  </code></pre>
  
  <p>However, I can work around it like so -</p>
  
  <pre><code>ctx (B f m) = let (c,m') = ctx m in ((B f) . c, m') -- OK
  </code></pre>
  
  <p>Why does this second definition typecheck but not the first one?</p>
  
  <p>Also, if I try to convert <code>ctx</code> to a complete function by checking for R, I again get a typecheck error -</p>
  
  <pre><code>ctx (R o) = (id, R o) -- Doesn't typecheck
  </code></pre>
  
  <p>Error -</p>
  
  <pre><code>Couldn't match type `o' with `o1'
    `o' is a rigid type variable bound by
        the type signature for ctx :: M o -&gt; (M o1 -&gt; M o, M o1)
        at delme1.hs:7:1
    `o1' is a rigid type variable bound by
         the type signature for ctx :: M o -&gt; (M o1 -&gt; M o, M o1)
         at delme1.hs:7:1
  In the first argument of `R', namely `o'
  In the expression: R o
  In the expression: (id, R o)
  </code></pre>
  
  <p>How can I work around this error?</p>
  
  <p>Any help is appreciated!</p>