GHC: Ticket #2235: Bogus occurs check with type families
http://ghc.haskell.org/trac/ghc/ticket/2235
<p>
Consider this program, using type families:
</p>
<pre class="wiki"> data Even; data Odd
type family Flip a :: *
type instance Flip Even = Odd
type instance Flip Odd = Even
data List a b where
Nil :: List a Even
Cons :: a -> List a b -> List a (Flip b)
tailList :: List a b -> List a (Flip b)
tailList (Cons _ xs) = xs
</pre><p>
I get the error (from the HEAD)
</p>
<pre class="wiki"> Occurs check: cannot construct the infinite type: b = Flip (Flip b)
In the pattern: Cons _ xs
In the definition of `tailList': tailList (Cons _ xs) = xs
</pre><p>
There's a bug here -- reporting an occurs check is premature. We should really be able to infer the type
</p>
<pre class="wiki"> tailList :: (b ~ Flip (Flip b)) => List a b -> List a (Flip b)
</pre><p>
But we get the same bogus occurs-check error with this signature.
</p>
<p>
This example also illustrates why we might want closed families. If you look at the type constraints arising from tailList you'll see that you get
<code>(c ~ Flip b, b ~ Flip c)</code>
where c is the existential you get from the GADT match. Now, <em>we</em> know that <code>b = Flip (Flip b)</code> is always true, but GHC doesn't. After all, you could add new type instances
</p>
<pre class="wiki"> type instance Flip Int = Bool
type instance Flip Bool = Char
</pre><p>
and then the equation wouldn't hold. What we really want is a *closed* type family, like this
</p>
<pre class="wiki"> type family Flip a where
Flip Even = Odd
Flip Odd = Even
</pre><p>
(preferably supported by kinds) and even *then* it's not clear whether it's reasonable to expect the compiler to solve the above problem by trying all possiblities. This relates to <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2101" title="#2101: feature request: Allow some form of type-level lemma (new)">#2101</a>
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/2235
Trac 1.2iglooSat, 26 Apr 2008 17:45:23 GMTmilestone set
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:1
<ul>
<li><strong>milestone</strong>
set to <em>6.10 branch</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:37:31 GMTarchitecture changed
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:2
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:2
<ul>
<li><strong>architecture</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketsimonmarTue, 30 Sep 2008 15:51:46 GMTos changed
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:3
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:3
<ul>
<li><strong>os</strong>
changed from <em>Unknown</em> to <em>Unknown/Multiple</em>
</li>
</ul>
TicketchakWed, 01 Oct 2008 06:28:51 GMTstatus changed; resolution set
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:4
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:4
<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>
We agreed that this
</p>
<pre class="wiki">tailList :: (b ~ Flip (Flip b)) => List a b -> List a (Flip b)
</pre><p>
is not the right signature.
</p>
<p>
The new solver doesn't produce the infinite-type error message, but the usual one where it complains about not being able to instantiate a rigid type.
</p>
TicketsimonpjWed, 01 Oct 2008 07:50:56 GMT
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:5
http://ghc.haskell.org/trac/ghc/ticket/2235#comment:5
<p>
Just to fill in the details here. The type of <code>Cons</code> is
</p>
<pre class="wiki">Cons :: forall a b. forall c. (b ~ Flip c) => a -> List a c -> List a b
</pre><p>
The task is this:
</p>
<pre class="wiki">b ~ Flip (Flip b), b ~ Flip c |- List a (Flip b) ~ List a c
</pre><p>
And indeed that isn't provable. If we'd written the type of <code>Cons</code> the other way about, thus:
</p>
<pre class="wiki">Cons :: forall a b. a -> List a (Flip b) -> List a b
</pre><p>
then we could prove it; but doubtless something else would go wrong. To do it right we'd have to give this type to <code>Cons</code>
</p>
<pre class="wiki">Cons :: forall a b c. (b ~ Flip c, c ~ Flip b) => a -> List a c -> List a b
</pre><p>
Which we could. But it seems uncomfortably fragile.
</p>
<p>
Simon
</p>
Ticket