Type signature is too general; missing constraint?
<p>So I tried to ask a general "<a href="https://stackoverflow.com/questions/37101800/how-to-debug-type-level-programs">how do you debug type-level programming problems?</a>" question, and it seems either the question is too general to answer, or maybe it's impossible to debug such things. :-}</p>

<p>On this particular day, the problem that's irking me is a moderately large, complex program. I've managed to boil it down to a reasonably small core that still goes wrong. Here we go:</p>

<pre><code>{-#
  LANGUAGE
    GADTs, MultiParamTypeClasses,
    FlexibleInstances, FlexibleContexts, RankNTypes,
    KindSignatures
#-}

module Minimal where

-------------------------------------------------------------------------------

data Union (t :: * -&gt; *) (ts :: * -&gt; *) x

class Member (x :: * -&gt; *) (ys :: * -&gt; *) where
instance Member x (Union x ys) where
instance (Member x ys) =&gt; Member x (Union y ys) where

-------------------------------------------------------------------------------

data ActM (effects :: * -&gt; *) x
instance Monad (ActM effects) where

-------------------------------------------------------------------------------

data Reader i x where
  Get :: Reader i i

get :: Member (Reader i) req =&gt; ActM req i
get = undefined

runReader :: i -&gt; ActM (Union (Reader i) req) x -&gt; ActM req x
runReader = undefined
</code></pre>

<p>(Aside: I look at that list of language extensions and think to myself "maybe this is just a terrible idea!")</p>

<p>Anyway, the really interesting part is at the bottom. We see that</p>

<pre><code>runReader :: i -&gt; ActM (Union (Reader i) req) x -&gt; ActM req x
</code></pre>

<p>In other words, for any <code>i</code>, <code>runReader</code> takes an action in the <code>ActM</code> monad that has <code>Reader i</code> as one of its possible effects, and returns an action in the <code>ActM</code> monad <em>without</em> that possible effect. Simple, right?</p>

<p>Now if I pass (say) a <code>Char</code> as the first argument, then the reader type is fixed to <code>Char</code>:</p>

<pre><code>runReader 'X' :: ActM (Union (Reader Char) req) x -&gt; ActM req x
</code></pre>

<p>So far, so good. If I just return some data, all is fine:</p>

<pre><code>runReader 'X' (return True) :: ActM req Bool
</code></pre>

<p>(Reassuringly, I also get the correct <em>value</em> as the result!)</p>

<p>But now, what about the <code>get</code> function?</p>

<pre><code>get :: Member (Reader i) req =&gt; ActM req i
</code></pre>

<p>So <code>get</code> is an action in the <code>ActM</code> monad for any set of effects that includes <code>Reader i</code>. And that means that if I pass it to <code>runReader</code> then I get...</p>

<pre><code>runReader 'X' get :: Member (Reader x) (Union (Reader Char) req) =&gt; ActM req x
</code></pre>

<p>...wait, what?!? Why hasn't the compiler figured out that <code>x</code> <em>must</em> be <code>Char</code>?</p>

<p>Indeed, if I add an explicit type signature that says</p>

<pre><code>runReader 'X' get :: ActM req Char
</code></pre>

<p>then it compiles perfectly (and, incidentally, I get the right value output, which is nice). So where am I missing a constraint?</p>