GHC: Ticket #15248: Coercions from plugins cannot be stopped from floating out
http://ghc.haskell.org/trac/ghc/ticket/15248
<p>
Suppose we have
</p>
<div class="wiki-code"><div class="code"><pre><span class="kr">type</span> <span class="kr">family</span> <span class="p">(</span>a <span class="ow">::</span> <span class="kt">Nat</span><span class="p">)</span> <span class="o"><?</span> <span class="p">(</span>b <span class="ow">::</span> <span class="kt">Nat</span><span class="p">)</span> <span class="ow">::</span> <span class="kt">Bool</span>
</pre></div></div><p>
that computes whether <code>a</code> is less than <code>b</code>, where a type checker plugin does the proof work. For some <code>a</code>, <code>b</code>, and <code>c</code>, if we assume <code>(a <? b) ~ True</code> and <code>(b <? c) ~ True</code>, the plugin can prove <code>(a <? c) ~ True</code>. However, GHC currently provides no way for the plugin to indicate that the proof of <code>(a <? c) ~ True</code> depends on the assumptions. This means that the plugin-produced proof evidence could potentially float out of its desired context, inviting disaster.
</p>
<p>
In term of <code>Coercion</code>s, I propose that the <code>PluginProv</code> constructor of <code>UnivCoProvenance</code> be allowed to include a <code>TyCoVarSet</code> of "free variables" (that is, assumptions) in the proof. Computing the free variables of the enclosing <code>UnivCo</code> would returns these variables, too. It is, of course, up to the plugin to provide the right information here, but plugins generally have enough information to do this correctly (or, at least, to conservatively list all free variables of assumptions as free variables of the conclusion).
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/15248
Trac 1.2.2adamgundryFri, 08 Jun 2018 15:42:10 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:1
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:1
<ul>
<li><strong>cc</strong>
<em>adamgundry</em> added
</li>
</ul>
<p>
In this case, in principle, shouldn't the evidence produced for the plugin directly depend on the evidence for the assumptions? That is, rather than "proving" <code>(a <? c) ~ True</code> by <code>UnivCo</code>, you would "prove"
</p>
<pre class="wiki"> (((a <? b) ~ True, (b <? c) ~ True) => a <? c)
~ (((a <? b) ~ True, (b <? c) ~ True) => True)
</pre><p>
by <code>UnivCo</code> and then instantiate it with your evidence for <code>(a <? b) ~ True</code> and <code>(b <? c) ~ True</code>.
</p>
<p>
That said, your suggestion might make things easier in practice...
</p>
TicketadamgundryFri, 08 Jun 2018 15:42:50 GMTkeywords set
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:2
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:2
<ul>
<li><strong>keywords</strong>
<em>TypeCheckerPlugins</em> added
</li>
</ul>
TicketgoldfireFri, 08 Jun 2018 15:48:54 GMT
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:3
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:3
<p>
But <a class="ticket" href="http://ghc.haskell.org/trac/ghc/ticket/15248#comment:1" title="Comment 1">comment:1</a> seems to require a constrained type in the <code>~</code> relation, which is generally not allowed. I suppose nothing stops a plugin from producing such things (and GHC might even consume them correctly), but I don't think that's explicitly a supported feature. (You can't say that in source Haskell, for example. Even with quantified constraints.)
</p>
TicketsimonpjFri, 08 Jun 2018 16:17:05 GMT
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:4
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:4
<p>
Yes: see <a class="missing ticket" title="ticket comment does not exist">comment:15</a> on <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8095" title="#8095: bug: TypeFamilies painfully slow (new)">#8095</a>, and the discussion on <a class="ext-link" href="https://phabricator.haskell.org/D4766" title="D4766 in Phab"><span class="icon"></span>Phab:D4766</a>. <code>PlugInProv</code> should have a <code>TyCoVarSet</code> just as the (upcoming) <code>ZappedProv</code> does, and for the same reasons.
</p>
TicketbgamariThu, 21 Jun 2018 18:13:35 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:5
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:5
<ul>
<li><strong>milestone</strong>
changed from <em>8.6.1</em> to <em>8.8.1</em>
</li>
</ul>
<p>
These won't be addressed in GHC 8.6.
</p>
Ticketosa1Fri, 28 Dec 2018 06:34:15 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:6
http://ghc.haskell.org/trac/ghc/ticket/15248#comment:6
<ul>
<li><strong>milestone</strong>
changed from <em>8.8.1</em> to <em>8.10.1</em>
</li>
</ul>
<p>
Bumping milestones of low-priority tickets.
</p>
Ticket