<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>On 9/2/21 11:04 PM, Richard Eisenberg wrote:<br>
</p>
<blockquote type="cite"
cite="mid:010f017ba99d4730-68884819-acc3-427b-93ef-7c26e3cd0b53-000000@us-east-2.amazonses.com">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>
<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><br class="">
</div>
<div>No. That's not a GADT -- the constructor doesn't restrict
anything about `f`.</div>
</div>
</blockquote>
<p>Morally, sure, but GHC doesn't know about this.<br>
</p>
<p>I tried, and -XGADTSyntax + -XExistenialTypes = -XGADTs it seems.</p>
<blockquote type="cite"
cite="mid:010f017ba99d4730-68884819-acc3-427b-93ef-7c26e3cd0b53-000000@us-east-2.amazonses.com">
<div>
<div><br class="">
</div>
<div>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><br class="">
</div>
<div>newtype Some f = MkSome (exists a. f a)</div>
<div><br class="">
</div>
<div>We can probably support the syntax you wrote, too, but I
don't want to commit to that right now.</div>
</div>
</blockquote>
<p>The syntax I wrote is already basically valid?</p>
<pre>data Some f = forall a. Some (f a)
</pre>
<pre>data Some f where MkSome :: forall a f. f a -> Some f</pre>
<p>Is accepted</p>
<pre>newtype Some f = forall a. Some (f a)
</pre>
<pre>newtype Some f where MkSome :: forall a f. f a -> Some f
</pre>
<p>Is not with "A newtype constructor cannot have existential type
variables"</p>
<p>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>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>
</p>
<p>John</p>
</body>
</html>