GHC: Ticket #11511: Type family producing infinite type accepted as injective
http://trac.haskell.org/trac/ghc/ticket/11511
<p>
A question came up during discussion at University of Wrocław:
</p>
<div class="wiki-code"><div class="code"><pre><span class="kr">type</span> <span class="kr">family</span> <span class="kt">F</span> a <span class="ow">=</span> r <span class="o">|</span> r <span class="ow">-></span> a <span class="kr">where</span>
<span class="kt">F</span> a <span class="ow">=</span> <span class="p">[</span><span class="kt">F</span> a<span class="p">]</span>
</pre></div></div><p>
Should this pass the injectivity check? Currently it does but I don't think this is correct. After all <code>F Bool</code> and <code>F Char</code> both reduce to the same infinite type <code>[[[...]]]</code>, which by definition of injectivity gives us <code>Char ~ Bool</code>. Is this dangerous in practice? It can cause reduction stack overflow (or an infinite loop if you disable that check) but I don't think this can be used to construct unsafe coerce. We'd have to unify two infinite types, which does not seem possible.
</p>
<p>
This is not an implementation problem - this stays faithful to theory developed in injective type families paper. If others agree that this is indeed incorrect then I think the right solution here would be to drop equation (7) from our algorithm in the paper. For generalized injectivity we planned drop that equation anyway. Here's another reason for doing this.
</p>
en-usGHChttp://trac.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://trac.haskell.org/trac/ghc/ticket/11511
Trac 1.2.2adamgundrySat, 30 Jan 2016 21:30:27 GMTcc changed
http://trac.haskell.org/trac/ghc/ticket/11511#comment:1
http://trac.haskell.org/trac/ghc/ticket/11511#comment:1
<ul>
<li><strong>cc</strong>
<em>adamgundry</em> added
</li>
</ul>
<p>
I don't think this is a soundness problem: FC does not have infinite types, only finite approximations thereof, and there is no way to prove the equality of any finite expansions of <code>F Bool</code> and <code>F Char</code>.
</p>
<p>
Here's a hand-wavy argument that injectivity of <code>F</code> is admissible... Suppose we have a minimal coercion <code>F s ~ F t</code>. Then either this is by congruence of type family application (in which case we have <code>s ~ t</code>), or it uses the axiom for <code>F</code> to expand both sides, so there is a smaller coercion <code>[F s] ~ [F t]</code> and hence of <code>F s ~ F t</code> (which contradicts the assumption that our original coercion was minimal). [The ordering on coercions is left as an exercise to the reader.]
</p>
TicketgoldfireSat, 30 Jan 2016 22:28:21 GMT
http://trac.haskell.org/trac/ghc/ticket/11511#comment:2
http://trac.haskell.org/trac/ghc/ticket/11511#comment:2
<p>
Perhaps this counterexample is why I could never finish that proof. I don't believe I ever reached for an assumption of finite types, probably conflating the notion of finite types with terminating type families.
</p>
<p>
What bothers me is that we have no guarantee that FC types are indeed finite. On paper, we just define types inductively and are done with it. But how does this play out in the implementation? Recall that infinite types have led to segfaults before: <a class="closed ticket" href="http://trac.haskell.org/trac/ghc/ticket/8162" title="#8162: bug: Type unsoundness with type families and UndecidableInstances (closed: fixed)">#8162</a>.
</p>
TicketjstolarekSun, 31 Jan 2016 18:04:18 GMT
http://trac.haskell.org/trac/ghc/ticket/11511#comment:3
http://trac.haskell.org/trac/ghc/ticket/11511#comment:3
<blockquote class="citation">
<p>
I think the right solution here would be to drop equation (7) from our algorithm in the paper.
</p>
</blockquote>
<p>
On a second thought I don't think this would be good idea. Doing this would mean that using any type family in the RHS is prohibited for injective type families and we definitely don't want that for generalized injectivity.
</p>
TicketadamgundryMon, 01 Feb 2016 18:08:06 GMT
http://trac.haskell.org/trac/ghc/ticket/11511#comment:4
http://trac.haskell.org/trac/ghc/ticket/11511#comment:4
<blockquote class="citation">
<p>
What bothers me is that we have no guarantee that FC types are indeed finite. On paper, we just define types inductively and are done with it. But how does this play out in the implementation?
</p>
</blockquote>
<p>
I suppose it might be possible to accidentally define an "infinite" type or coercion as a lazy value, but surely Core Lint would go into a loop when checking it? What other problems do you envisage?
</p>
<blockquote class="citation">
<p>
Recall that infinite types have led to segfaults before: <a class="closed ticket" href="http://trac.haskell.org/trac/ghc/ticket/8162" title="#8162: bug: Type unsoundness with type families and UndecidableInstances (closed: fixed)">#8162</a>.
</p>
</blockquote>
<p>
That's a slightly different issue: the type family overlap check was unsound because it treated <code>a</code> and <code>a -> a</code> as apart, even though <code>a ~ a -> a</code> is solvable in the presence of non-terminating type families. Crucially, it is possible to construct a <em>finite</em> proof of <code>a ~ a -> a</code> that contradicts the overlap check. Whereas in this case, the only "proofs" of <code>F Bool ~ F Char</code> are infinite (and hence non-constructible).
</p>
TicketjstolarekFri, 09 Dec 2016 10:44:25 GMT
http://trac.haskell.org/trac/ghc/ticket/11511#comment:5
http://trac.haskell.org/trac/ghc/ticket/11511#comment:5
<p>
I had a talk about injective type families yesterday and it provoked me to rethink this issue. What we do in the pre-unification algorithm is:
</p>
<ol><li>assume that type family applications unify with anything
</li><li>but we look under injective type family applications and unify the arguments
</li></ol><p>
Now, my question is: when we are checking whether <code>F</code> is injective why do we assume that <code>F</code>'s injectivity annotation is true? This is what we're trying to prove and I think we should not assume that as part of our proof. This is exactly what's happening here.
</p>
TicketrwbartonSat, 10 Dec 2016 05:01:56 GMT
http://trac.haskell.org/trac/ghc/ticket/11511#comment:6
http://trac.haskell.org/trac/ghc/ticket/11511#comment:6
<p>
I imagine you have some examples where you need the recursive assumption. For a boring example, imagine converting one (promoted) unary natural number type <code>data N1 = Z1 | S1 N1</code> to another <code>data N2 = Z2 | S2 N2</code>:
</p>
<pre class="wiki">type family F (a :: N1) :: N2 where
F Z1 = Z2
F (S1 n) = S2 (F n)
</pre><p>
That is injective but you need to use the injectivity inductively to prove it.
</p>
<p>
The original example seems fine to me, since you can't prove <code>F Bool ~ F Char</code> (you would need both the "infinite type" <code>[[[...]]]</code> and an infinitely long proof in order to do so).
</p>
TicketjstolarekMon, 12 Dec 2016 09:41:18 GMT
http://trac.haskell.org/trac/ghc/ticket/11511#comment:7
http://trac.haskell.org/trac/ghc/ticket/11511#comment:7
<p>
Yes, certainly what I said is conservative - some injective functions would be rejected. What I'm wondering is whether our current approach is sound from a logical point of view. Perhaps assuming <code>F</code> injective when checking injectivity of <code>F</code> is the reason why Richard couldn't complete the proof we presented in the paper?
</p>
TicketsimonpjWed, 19 Apr 2017 14:27:10 GMTkeywords changed
http://trac.haskell.org/trac/ghc/ticket/11511#comment:8
http://trac.haskell.org/trac/ghc/ticket/11511#comment:8
<ul>
<li><strong>keywords</strong>
<em>InjectiveFamilies</em> added; <em>Injective</em> removed
</li>
</ul>
Ticket