<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Sep 6, 2021, at 11:21 AM, John Ericson <<a href="mailto:john.ericson@obsidian.systems" class="">john.ericson@obsidian.systems</a>> wrote:</div><br class="Apple-interchange-newline"><div class="">
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8" class="">
<div class=""><p class="">On 9/2/21 11:04 PM, Richard Eisenberg wrote:<br class="">
</p>
<blockquote type="cite" cite="mid:010f017ba99d4730-68884819-acc3-427b-93ef-7c26e3cd0b53-000000@us-east-2.amazonses.com" class="">On
Sep 2, 2021, at 2:56 PM, john.ericson <<a href="mailto:john.ericson@obsidian.systems" class="" moz-do-not-send="true">john.ericson@obsidian.systems</a>>
wrote:
<div class="">
<blockquote type="cite" class=""><br class="Apple-interchange-newline">
<div class="">
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type" class="">
<div class="">
<div style="font-size:10pt;font-family:Verdana,Arial,Helvetica,sans-serif;" class="">Does the most basic e.g.
<div class=""><br class="">
</div>
<div class="">newtype Some f where</div>
<div class=""> MkSome :: forall a. f a -> Some f<br id="br3" class="">
<br class="">
Have one of those problematic equalities?<br id="br3" class="">
</div>
</div>
</div>
</div>
</blockquote>
<div class=""><br class="">
</div>
<div class="">No. That's not a GADT -- the constructor doesn't restrict
anything about `f`.</div>
</div>
</blockquote><p class="">Morally, sure, but GHC doesn't know about this.<br class=""></p></div></div></blockquote><div><br class=""></div><div>Sure it does -- GHC doesn't include an equality constraint as one of the fields of MkSome. This isn't about extensions -- it's about the way the data constructor is interpreted.</div><blockquote type="cite" class=""><div class=""><div class=""><blockquote type="cite" cite="mid:010f017ba99d4730-68884819-acc3-427b-93ef-7c26e3cd0b53-000000@us-east-2.amazonses.com" class=""><div class=""><div class=""><br class="">
</div>
<div class="">I think you're after newtype existentials. I think these
should indeed be possible, because what you propose appears to
be the same as</div>
<div class=""><br class="">
</div>
<div class="">newtype Some f = MkSome (exists a. f a)</div>
<div class=""><br class="">
</div>
<div class="">We can probably support the syntax you wrote, too, but I
don't want to commit to that right now.</div>
</div>
</blockquote><p class="">The syntax I wrote is already basically valid?</p>
<pre class="">data Some f = forall a. Some (f a)
</pre>
<pre class="">data Some f where MkSome :: forall a f. f a -> Some f</pre><p class="">Is accepted</p>
<pre class="">newtype Some f = forall a. Some (f a)
</pre>
<pre class="">newtype Some f where MkSome :: forall a f. f a -> Some f
</pre><p class="">Is not with "A newtype constructor cannot have existential type
variables"</p><p class="">I propose we teach GHC how these "GADTs" in fact merely have
existential variables, and not the FC constraints that require the
extra evaluation for soundness. Than we can get the
operational/runtime benefits of what you propose for cheap. Don't
get me wrong -- the other aspects in the paper this doesn't
address are still quite valuable, but I think this is a useful
stepping stone / removal of artificial restrictions we should do
first.</p><p class="">This sort of thing is brought up in #1965, where it is alleged
this is in fact more difficult than it sounds. All more reason it
is a good stepping stone, I say!<br class=""></p></div></div></blockquote><div><br class=""></div><div>This is more difficult than it sounds. :) Newtypes are implemented via coercions in Core, and coercions are inherently bidirectional. The appearance of an existential in this way requires one-way conversions, which are currently not supported. So, to get what you want, we'd have to modify the core language as in the existentials paper, along with some extra work to automatically add `pack` and `open` -- rather similar to the type inference described in the existentials paper. The bottom line for me is that this seems just as hard as implementing the whole thing, so I see no value in having the stepping stone. If we always wrote out the newtype constructor, then maybe we could use its appearance to guide the `pack` and `open`, but we don't: sometimes, we just use `coerce`. So I really don't think this is any easier than implementing the paper as written. Once that's done, we can come back and add this new feature relatively easily (I think).</div><div><br class=""></div><div>Richard</div><br class=""><blockquote type="cite" class=""><div class=""><div class=""><p class="">
</p><p class="">John</p>
</div>
</div></blockquote></div><br class=""></body></html>