<div dir="ltr"><div class="gmail_default" style="font-family:tahoma,sans-serif">Hi Amelia</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><blockquote class="gmail_default gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
I do understand the reasons behind forbidding 'forall's in instance<br>
heads, but I don't see a good reason to forbid instances headed by a<br>
type synonym --- the original concern, writing an instance for a<br>
constraint tuple, is (now) forbidden regardless of whether<br>
'checkValidInstance' uses 'splitTyConApp_maybe', by the call to<br>
'checkValidInstanceHead'. Would a patch allowing instances headed by a<br>
type synonym be welcome, or would this need to go through a proposal? <br></blockquote><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">If you want to change the source language, you definitely need a proposal.</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">I must say that I'm very un-clear what specific change you propose, and why it would be a desirable change.  But elucidating all that is precisely what the GHC proposals process is all about!</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">Simon<br></div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 22 Feb 2024 at 17:06, Amélia Liao <me@amelia.how> 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">Dear ghc-devs,<br>
<br>
Prompted by a toot by Conor McBride [1], I got sent on a rabbit-chase<br>
down the hole that are the restrictions on instance head shapes.<br>
Re-assembling the relevant parts, Conor's trouble arises from code of<br>
the form<br>
<br>
    data Nat<br>
    data CdB (p :: Nat -> *) (m :: Nat) :: * where<br>
<br>
    type Shown (p :: Nat -> *) = forall n. Show (p n)<br>
    instance Shown p => Shown (CdB p) where<br>
      show = ...<br>
<br>
After some shallow investigation, a similar issue came up as #13267,<br>
whose fix adds a note mentioning that the "show is not a method" error<br>
pops up in the renamer, and so is a bit tricky to improve. However, even<br>
after expanding Conor's type synonyms, the type checker now complains<br>
that an instance head can not have a forall.<br>
<br>
I do understand the reasons behind forbidding 'forall's in instance<br>
heads, but I don't see a good reason to forbid instances headed by a<br>
type synonym --- the original concern, writing an instance for a<br>
constraint tuple, is (now) forbidden regardless of whether<br>
'checkValidInstance' uses 'splitTyConApp_maybe', by the call to<br>
'checkValidInstanceHead'. Would a patch allowing instances headed by a<br>
type synonym be welcome, or would this need to go through a proposal?<br>
<br>
I think that it would be mostly straightforward, though laborious, to<br>
implement this; Essentially, changing 'rnMethodBinds' to annotate method<br>
bindings with a set of /all possible/ method 'Name's that match what the<br>
user wrote, together with their classes, and only deciding on the actual<br>
'Name' in 'tcMethods', where we know the actual class name for the<br>
instance head.<br>
<br>
If this work would be welcome, I'd appreciate some pointers on dealing<br>
with TTG before I write a massive pull request that wastes everyone's<br>
time.<br>
<br>
In particular, my immediate thought for storing the extra information<br>
needed is to change the type of 'cid_binds' for 'ClsInstDecl' in<br>
*'GhcRn' only*, but trying this out locally causes quite a bit of<br>
breakage. It might make more sense to add a 'MethodBind' constructor to<br>
'HsBindLR' which is inserted by the renamer, like 'VarBind', and removed<br>
by the type checker; but this /also/ requires quite a bit of code<br>
motion. I'm happy to open an issue on GitLab if discussing possible<br>
implementation ideas would be easier over there.<br>
<br>
Of course, simply allowing instances headed by a type synonym wouldn't<br>
fix Conor's original example, since having 'forall' in an instance head<br>
would still be forbidden. It's my understanding that the reason those<br>
are forbidden is due to nasty interactions with ScopedTypeVariables,<br>
where<br>
<br>
    instance forall a. C a => forall b. D a b where<br>
<br>
brings 'b' into scope in the methods' RHSes, whereas the RHS of a<br>
top-level function with the same signature would /not/ have 'b' in<br>
scope. But given that a higher-ranked type synonym would not bring the<br>
variables it quantifies over into scope /anyway/, is there a reason to<br>
forbid it then?<br>
<br>
Cheers,<br>
Amélia<br>
<br>
[1]: <a href="https://types.pl/@pigworker/111975161248256507" rel="noreferrer" target="_blank">https://types.pl/@pigworker/111975161248256507</a><br>
_______________________________________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org" target="_blank">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>