GHC: Ticket #10327: Devise workaround for how infinite types prevent closed type family reduction
http://ghc.haskell.org/trac/ghc/ticket/10327
<p>
Suppose we have
</p>
<pre class="wiki">data a :+: b
type family Inj x y where
Inj a a = True
Inj b (b :+: c) = False
</pre><p>
When we try to reduce <code>Inj f (f :+: g)</code>, it looks like we should just use the second equation. Instead, we fail to reduce. This is because GHC is worried about the possibility of the first equation firing, in the event that <code>f ~ (f :+: g)</code>. This fact can happen only if <code>f</code> is infinitely large. On the surface, this seems impossible, but shenanigans in this area can cause <code>unsafeCoerce</code>. See <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8162" title="#8162: bug: Type unsoundness with type families and UndecidableInstances (closed: fixed)">#8162</a>.
</p>
<p>
I don't see an easy way to fix this, but the fact that GHC can't cope (well) with this example tells me something is wrong. Here is one idea of how to proceed:
</p>
<p>
If we somehow ensure at reduction time that <code>f</code> is finite, we're OK. If we need finiteness in terms, we use <code>deepseq</code>. Can we do this in types? I tentatively say "yes".
</p>
<p>
Imagine the following type family:
</p>
<pre class="wiki">type family Seq (x :: a) (y :: b) :: b
type instance Seq True y = y
type instance Seq False y = y
</pre><p>
To reduce, say, <code>b `Seq` 5</code>, we'd need to know concretely what <code>b</code> is. We can then build <code>Deepseq</code> similarly to how <code>deepseq</code> at the term level works.
</p>
<p>
The closed type family mechanism could then detect cases like <code>Inj</code>, where the whole infinite-type thing is causing trouble. (I conjecture that detecting this is not hard, as there's a specific line in the <code>Unify</code> module that triggers in the worry-about-infinite-types case.) In the case of <code>Inj</code>, something like <code>Inj f (f :+: g)</code> would reduce to <code>f `Deepseq` False</code>. Note that the call to <code>Seq</code> wouldn't be written in the closed type family definition, but would be inserted during reduction as appropriate.
</p>
<p>
This solution is ugly. And it requires magic to define <code>Seq</code> in types (we need an instance for every type!) and weird magic in closed type family reduction. The definition of <code>Deepseq</code> might also benefit from being magical. It would be annoying to explain to users, but no more so than the current crazy story. In general, I don't like this idea much, but I do think it would work.
</p>
<p>
In any case, this ticket is mainly to serve as a placeholder for any future thoughts in this direction. It's quite annoying to have the specter of infinite types cripple otherwise-sensible closed type families.
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/10327
Trac 1.2.2garrettMon, 20 Apr 2015 15:03:19 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/10327#comment:1
http://ghc.haskell.org/trac/ghc/ticket/10327#comment:1
<ul>
<li><strong>cc</strong>
<em>garrett</em> added
</li>
</ul>
TicketsimonpjMon, 20 Apr 2015 21:08:54 GMT
http://ghc.haskell.org/trac/ghc/ticket/10327#comment:2
http://ghc.haskell.org/trac/ghc/ticket/10327#comment:2
<p>
I must be missing something. <code>Inf f (f :+: g)</code> will certainly reduce for any ground <code>f</code> (such as <code>True</code> or <code>False</code>) because then the call will be apart from the first equation so the second can fire.
</p>
<p>
If <code>f</code> is not ground, then it'll still reduce, if <code>f</code> is anything other than <code>f2 :+: g</code>, for the same reason.
</p>
<p>
If <code>f</code> is a variable then yes the reduction is stuck, but that seems fair enough. Reducing it to <code>f `Seq` rhs</code> doesn't get us any further forward (e.g. if we want to unify this with another type) but it does add real new complication.
</p>
<p>
Very unconvinced.
</p>
TicketgoldfireTue, 21 Apr 2015 00:59:42 GMT
http://ghc.haskell.org/trac/ghc/ticket/10327#comment:3
http://ghc.haskell.org/trac/ghc/ticket/10327#comment:3
<p>
Replying to <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/10327#comment:2" title="Comment 2">simonpj</a>:
</p>
<blockquote class="citation">
<p>
Very unconvinced.
</p>
</blockquote>
<p>
As, rest assured, am I.
</p>
<p>
I think to get this to work we would also need a constraint <code>Finite f</code> that means (via magic) that <code>f `Seq` x</code> reduces to <code>x</code>. (Without magic, this would be spelled <code>forall x. f `Seq` x ~ x</code>, but that's a higher-order constraint!)
</p>
<p>
But to really get it to work, we need a totally different idea, as this one is terrible.
</p>
TicketthomieSun, 24 Jan 2016 16:26:27 GMTkeywords set
http://ghc.haskell.org/trac/ghc/ticket/10327#comment:4
http://ghc.haskell.org/trac/ghc/ticket/10327#comment:4
<ul>
<li><strong>keywords</strong>
<em>TypeFamilies</em> added
</li>
</ul>
Ticket