GHC: Ticket #5277: Clash between RankNTypes and TypeFamilies
http://ghc.haskell.org/trac/ghc/ticket/5277
<p>
[Note: a more specific summary line is in order for this ticket.]
</p>
<p>
Consider the following program:
</p>
<pre class="wiki">{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
type family F a b :: *
data W a b = W {unW :: F a b}
data T a = T {unT :: forall b. W a b}
-- f :: T a -> F a b
f = unW . unT
</pre><p>
It type checks fine and querying the inferred type for f interactively yields the expected type. However, adding a type signature for f,
</p>
<pre class="wiki">f :: T a -> F a b
f = unW . unT
</pre><p>
results in a typing error:
</p>
<pre class="wiki">Couldn't match type `F a b0' with `F a b'
NB: `F' is a type function, and may not be injective
Expected type: W a b0 -> F a b
Actual type: W a b0 -> F a b0
In the first argument of `(.)', namely `unW'
In the expression: unW . unT
</pre>en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/5277
Trac 1.2stefanSun, 26 Jun 2011 08:56:15 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:1
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:1
<ul>
<li><strong>cc</strong>
<em>stefan@…</em> added
</li>
</ul>
TicketsimonpjSun, 26 Jun 2011 21:55:42 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:2
http://ghc.haskell.org/trac/ghc/ticket/5277#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>
Yes, this is a gotcha with type families. See: <a class="ext-link" href="http://haskell.org/haskellwiki/GHC/Indexed_types#Frequently_asked_questions"><span class="icon"></span>http://haskell.org/haskellwiki/GHC/Indexed_types#Frequently_asked_questions</a>.
</p>
<p>
I don't know how to improve matters.
</p>
TicketstefanSun, 26 Jun 2011 23:22:36 GMT
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:3
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:3
<p>
Thanks for the quick response. It could well be that my brain's just not big enough for this, but I still don't quite get the part where type checking only fails *after* one adds the type signature. My apologies for the inconvenience, but I would really like to understand the issue there.
</p>
TicketsimonpjWed, 29 Jun 2011 11:46:14 GMT
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:4
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:4
<p>
Did you read the FAQ I pointed you at? It (attempts to) explain precisely why the type error occurs only when you add a type signature. Did that not help?
</p>
<p>
If you want the type signature, you need to help the type checker to resolve the ambiguity, thus:
</p>
<pre class="wiki">{-# LANGUAGE ScopedTypeVariables, RankNTypes, TypeFamilies #-}
module T5277 where
type family F a b :: *
data W a b = W {unW :: F a b}
data T a = T {unT :: forall b. W a b}
f :: forall a b. T a -> F a b
f = unW . (unT :: T a -> W a b)
</pre><p>
Simon
</p>
TicketstefanWed, 29 Jun 2011 12:12:42 GMT
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:5
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:5
<p>
I have to admit that from reading the FAQ, I probably wouldn't have figured out leaving out the type signature would help here.
</p>
<p>
I guess the part that I am missing is: why does the compiler pick the "right" equality constraint if the signature is absent.
</p>
TicketsimonpjWed, 29 Jun 2011 13:38:28 GMT
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:6
http://ghc.haskell.org/trac/ghc/ticket/5277#comment:6
<p>
I've elaborated the FAQ a bit; hope that helps.
</p>
Ticket