<div dir="ltr">Ben,<div><br></div><div>The suggestion of erroring if the inline pragma was not there was just because I thought it would be better than silently doing something different. But that's just a subjective opinion, it's not core to what I'm proposing.</div><div><br></div><div>Indeed there are two other options:</div><div><br></div><div>1. Make levity polymorphic functions implicitly inline OR</div><div>2. Compile a version which wraps all the levity polymorphism in boxes.</div><div><br></div><div>Either approach would mean the program would still be accepted with or without the pragma. Whether either of them are a good idea is debatable, but it shows it's not necessary to require a pragma.<br><br>So if it's important that excluding a pragma doesn't result in a program being rejected, either of the above options would solve that issue. </div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Oct 9, 2021 at 2:06 AM Ben Gamari <<a href="mailto:ben@smart-cactus.org">ben@smart-cactus.org</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Chris Smith <<a href="mailto:cdsmith@gmail.com" target="_blank">cdsmith@gmail.com</a>> writes:<br>
<br>
> On Fri, Oct 8, 2021 at 10:51 AM Ben Gamari <<a href="mailto:ben@smart-cactus.org" target="_blank">ben@smart-cactus.org</a>> wrote:<br>
><br>
>> In my mind the fundamental problem with this approach is that it means<br>
>> that a program's acceptance by the compiler hinges upon pragmas.<br>
>> This is a rather significant departure from the status quo, where one<br>
>> can remove all pragmas and still end up with a well-formed program.<br>
>> In this sense, pragmas aren't really part of the Haskell language but<br>
>> are rather bits of interesting metadata that the compiler may or may not<br>
>> pay heed to.<br>
>><br>
><br>
> I don't believe this is really the status quo.  In particular, the pragmas<br>
> relating to overlapping instances definitely do affect whether a program<br>
> type-checks or not.<br>
<br>
Yes, this is a fair point. Moreover, the same can be said of<br>
LANGUAGE pragmas more generally. I will rephrase my statement to reflect<br>
what was in my head when I initially wrote it:<br>
<br>
>> In my mind the fundamental problem with this approach is that it means<br>
>> that a program's acceptance by the compiler hinges upon INLINE pragmas.<br>
>> This is a rather significant departure from the status quo, where one<br>
>> can remove all INLINE, INLINEABLE, RULES, and SPECIALISE pragmas and<br>
>> still end up with a well-formed program.<br>
<br>
These pragmas all share the property that they don't change program<br>
semantics but rather merely affect operational behavior. Consequently,<br>
they should not change whether a program should be accepted.<br>
<br>
Cheers,<br>
<br>
- Ben<br>
</blockquote></div>