<div dir="ltr"><div class="gmail_default" style="font-family:tahoma,sans-serif">Hi Gergo</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail_default" style="font-family:tahoma,sans-serif">
I'd like to implement type synonyms containing wildcards. The idea is<br>
that if you have `type MySyn a = MyType a _ Int`, then during<br>
typechecking, every occurrence of `MySyn T` would be expanded into<br>
`MyType T w123 Int`, with a fresh type (meta)variable `w123`.
</div></blockquote><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">I imagine you mean that if you then write</div><div class="gmail_default" style="font-family:tahoma,sans-serif;margin-left:40px">f :: MySyn a -> a -> Int</div><div class="gmail_default" style="font-family:tahoma,sans-serif">then it's exactly as if you wrote (using PartialTypeSignatures)<br></div><div class="gmail_default" style="font-family:tahoma,sans-serif;margin-left:40px">f :: MyType a _ Int -> a -> Int</div><div class="gmail_default" style="font-family:tahoma,sans-serif">today. So if I understand it right, you intend that these type synonyms are second-class citizens: <i>they can occur precisely (and only) where wildcards are allowed to occur today</i>. For example, as Iavor suggests, you'd reject</div><div class="gmail_default" style="font-family:tahoma,sans-serif;margin-left:40px">data T a = MkT (MySyn a)</div><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 do this in a fork of GHC, that's obviously fine. If you want to offer it as a language extension, the best thing would be to write a GHC Proposal. Also you'd get a lot of useful design feedback that way, which might save you implementation cycles.</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="gmail_default" style="font-family:tahoma,sans-serif">
What is the reason for this? I would have expected type synonyms to be<br>
only relevant during typechecking, and then fully resolved in the<br>
elaborated Core output.
</div></blockquote><div><br></div><div style="font-family:tahoma,sans-serif" class="gmail_default">In GHC <b>an Id has only one type</b>. It does not have a "source type" and a "Core type". So we allow Core types to contain synonyms so that when we export that Id the importing scope (e.g. GHCi, and type error messages) can see it. Synonyms can also allow types to take less space. E.g. we have Type, where (if we fully expanded) we'd have to have (TYPE LiftedRep). One could imagine a different design.</div><div style="font-family:tahoma,sans-serif" class="gmail_default"><br></div><div style="font-family:tahoma,sans-serif" class="gmail_default">I would expect that, by the time typechecking is over, all your wildcard synonyms are gone. They really are second class.</div><div style="font-family:tahoma,sans-serif" class="gmail_default"><br></div><div style="font-family:tahoma,sans-serif" class="gmail_default">Just to mention too that the entire "wildcards in type signatures" story is (I think) jolly useful, but it also turned out to be pretty tricky to implement. If you just macro-expand your new synonyms, you won't disturb the wildcard story, but I just wanted to advertise that it's a tricky area.</div><div style="font-family:tahoma,sans-serif" class="gmail_default"><br></div><div style="font-family:tahoma,sans-serif" class="gmail_default">Simon<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, 22 Jul 2022 at 07:30, ÉRDI Gergő <<a href="mailto:gergo@erdi.hu">gergo@erdi.hu</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">Hi,<br>
<br>
I'd like to implement type synonyms containing wildcards. The idea is<br>
that if you have `type MySyn a = MyType a _ Int`, then during<br>
typechecking, every occurrence of `MySyn T` would be expanded into<br>
`MyType T w123 Int`, with a fresh type (meta)variable `w123`.<br>
<br>
One worrying thing I noticed in my initial exploration of the GHC<br>
codebase is that the Core representation of `Type`s can still contain<br>
type synonym occurrences. And this doesn't seem like just an artefact<br>
of sharing the `Type` representation with `TcType`, since the<br>
`coreView` function also has code to look through type synonyms.<br>
<br>
What is the reason for this? I would have expected type synonyms to be<br>
only relevant during typechecking, and then fully resolved in the<br>
elaborated Core output. If that were the case, then a new version of<br>
`expand_syn` could live in `TcM` and take care of making these fresh<br>
metavariables.<br>
<br>
Beside this concrete question, taking a step back, I would also like<br>
to hear from people who know their way around this part of GHC, what<br>
they think about this and how they'd approach implementing it.<br>
<br>
Thanks,<br>
Gergo<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>