<div dir="auto">Hello,<div dir="auto"><br></div><div dir="auto">I've implemented such a feature in Cryptol, not GHC, so it is quite doable, but I think the implementation would be easier if you decided on the overall design of the feature first.</div><div dir="auto"><br></div><div dir="auto">Some things to consider:</div><div dir="auto">  * these kind of "existential" variable make sense in other type signatures, not just type synonyms</div><div dir="auto">   * there might be some contexts where you may want to disallow such wildcards (e. g., in a data declaration)</div><div dir="auto">   * you have to be careful with the scoping of type variables.  For example, you should not unify an existential/wildcard variable with a type that refers to variables that are not in scope of the wildcard.  I don't remember if GHC already has a system for such things, but in Cryptol we implanted this by having each unification variable keep track of the quantified variables that it may depend on.</div><div dir="auto"><br></div><div dir="auto">Hope this helps,</div><div dir="auto">Iavor</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jul 22, 2022, 09:30 ÉRDI Gergő <<a href="mailto:gergo@erdi.hu">gergo@erdi.hu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;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" rel="noreferrer">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs</a><br>
</blockquote></div>