GHC: Ticket #8214: 'Untouchable' error in list comprehension
http://ghc.haskell.org/trac/ghc/ticket/8214
<p>
Hi,
</p>
<p>
I think this program should compile but it doesn't:
</p>
<pre class="wiki">{-# LANGUAGE GADTs #-}
data X a where X :: X Int
foo :: Bool
foo = null [ () | X <- [] ]
</pre><p>
It fails with:
</p>
<pre class="wiki"> Couldn't match expected type `a0' with actual type `()'
`a0' is untouchable
inside the constraints (t_g ~ Int)
bound at a pattern with constructor
X :: X Int,
in a pattern binding in
list comprehension
In the pattern: X
In a stmt of a list comprehension: X <- []
In the first argument of `null', namely `[() | X <- []]'
</pre><p>
If I remove the type declaration GHC compiles without errors and happily infers <code>foo :: Bool</code>.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/8214
Trac 1.2MartijnVanSteenbergenMon, 02 Sep 2013 12:45:31 GMTfailure changed
http://ghc.haskell.org/trac/ghc/ticket/8214#comment:1
http://ghc.haskell.org/trac/ghc/ticket/8214#comment:1
<ul>
<li><strong>failure</strong>
changed from <em>None/Unknown</em> to <em>GHC rejects valid program</em>
</li>
</ul>
TicketsimonpjMon, 02 Sep 2013 14:12:12 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/8214#comment:2
http://ghc.haskell.org/trac/ghc/ticket/8214#comment:2
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>resolution</strong>
set to <em>invalid</em>
</li>
</ul>
<p>
The error message is obscure (I'm sorry about that) but it's right.
</p>
<p>
Consider these two variants
</p>
<pre class="wiki">foo1 = map (\X -> ()) []
foo2 = map f []
where
f X = ()
</pre><p>
(Incidentally, in HEAD it makes no difference whether or not <code>foo</code> has a signature <code>foo :: Bool</code>, nor <code>foo1</code> or <code>foo2</code>.)
</p>
<p>
It's easiest to think about <code>foo2</code>. What is <code>f</code>'s type? Well, you say, <code>f :: X a -> ()</code>. But suppose X had been defined
</p>
<pre class="wiki">data X1 a where X :: X ()
</pre><p>
Then <code>f</code> could also have type <code>f :: X a -> a</code>. This is the classic example of not having most general types for GADTs. GHC isn't clever enough to exploit the fact that in the particular example you give there is only one type; the <a class="ext-link" href="http://haskell.org/haskellwiki/Simonpj/Talk:OutsideIn"><span class="icon"></span>Outside-In algorithm</a> rejects <code>f</code>.
</p>
<p>
In <code>foo</code> the question is "what is the type of <code>[ () | X <- [] ]</code>. If we had type <code>X1</code> then it could be <code>[()]</code> or <code>forall a. [a]</code>. In this case it doesn't matter what the answer is, but if there was overloading involved it might.
</p>
<p>
Solution: tell GHC which type the list has, thus:
</p>
<pre class="wiki">foo = null ([ () | X <- [] ] :: [()])
</pre><p>
This looks a bit stupid in this very cut-down example, but I suspect it'd make more sense in a real program.
</p>
<p>
Simon
</p>
TicketMartijnVanSteenbergenWed, 04 Sep 2013 11:05:35 GMT
http://ghc.haskell.org/trac/ghc/ticket/8214#comment:3
http://ghc.haskell.org/trac/ghc/ticket/8214#comment:3
<p>
Alright Simon, thank you for explaining, this makes sense.
</p>
Ticket