<div dir="auto">That's great to hear because it looks like this will need all the support it can get to ever be allowed into upstream...</div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Aug 12, 2022, 10:43 Edward Kmett <<a href="mailto:ekmett@gmail.com">ekmett@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">FWIW, Gergo, I've been following what you've been doing pretty closely, so there's at least two of us tracking it in the background. =) I might have some clever(?) (ab)uses for it in the future in my linear haskell code.<div><br></div><div>-Edward</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, Aug 11, 2022 at 10:33 PM ÉRDI Gergő <<a href="mailto:gergo@erdi.hu" target="_blank" rel="noreferrer">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 Richard,<br>
<br>
Thanks for getting back to me! My replies are inline below.<br>
<br>
On Thu, 11 Aug 2022, Richard Eisenberg wrote:<br>
<br>
> You want a third:<br>
><br>
> C. invisible parameters that are filled in with a fresh wildcard.<br>
><br>
> We would need to have some way of writing out the type of such a thing <br>
> (i.e. what kind would `Syn` have?), but I presume this is possible.<br>
<br>
I think there's a tension between this and your suggestion to only add <br>
implicit parameters as a new `TyConBndrVis`, but more on that below.<br>
<br>
>> 2. Using partial type synonyms<br>
>><br>
>><br>
><br>
> This bit also makes sense, but I think users will want more <br>
> functionality. Specifically, what if a user does not want a wildcard <br>
> inserted, because they know that the right choice is `Int`? Or maybe <br>
> they want a *named* wildcard inserted. My experience is that once <br>
> something can be done implicitly, folks will soon find good reasons to <br>
> do it explicitly on occasion.<br>
<br>
Good point, but I think we can punt on this and not close any doors ahead. <br>
So today, you would only be able to write `Syn T` to mean `Syn {_} T`, and <br>
then in the future we can add typechecker support (and new surface <br>
syntax!) for `Syn {S} T`, without causing any compatibility problems with <br>
any existing code that doesn't give explicit args for implicit params.<br>
<br>
>> 3. Implementation<br>
>><br>
>><br>
>>  * When typechecking a type application, implicit arguments get<br>
>>    filled with the result of `tcAnonWildCardOcc`.<br>
><br>
> What about named wildcards? Even if they're not passed in, perhaps someone wants<br>
><br>
> type SomeEndo = _t -> _t<br>
><br>
> where the two types are known to be the same, but we don't know what.<br>
<br>
This would be something to support when typechecking the definition, not a <br>
given application. Your example would still elaborate to<br>
<br>
     type SomeEndo {t} = t -> t<br>
<br>
it would just use the same implicitly-bound type parameter `t` twice on <br>
the right-hand side. But when you use `SomeEndo`, the usage would still <br>
elaborate into a (single) anonymous wildcard argument, i.e.<br>
`SomeEndo {_}`.<br>
<br>
My current implementation doesn't support your example, but I think it's <br>
only because the renamer rejects it. I think if I get it through the <br>
renamer, it should already work because that `_t` will typecheck into a <br>
wildcard `TauTv`.<br>
<br>
>> 3. Similar to #1, I started just pushing all the way through GHC a<br>
>> change to `AnonArgFlag` that adds a third `ImplArg` flag.<br>
><br>
> I don't love adding a new constructor to AnonArgFlag, because that's <br>
> used in terms. Instead, it would be great to localize this new extension <br>
> to tycon binders somehow.<br>
<br>
OK so while I'd love to get away with only changing `TyConBndrVis`, this <br>
is the part of your email that I don't understand how to do :/<br>
<br>
First, when a type application is typechecked, we only have the kind of <br>
the type constructor, not its binders (and that makes sense, since we <br>
could be applying something more complex than directly a defined type <br>
constructor). So if I only add a new `TyConBndrVis` constructor, then I <br>
have no way of representing this in the `tyConKind` and so no way of <br>
finding out that I need to put in implicit args in `tcInferTyApps`.<br>
<br>
Second, you ask what the kind of `Syn` in e.g. `type Syn a = TC _ a` is. I <br>
think (supposing `TC :: K -> L -> M`) its kind should be (stealing syntax <br>
from Agda) something like `{K} -> L -> M`, i.e. a function kind with <br>
domain `K`, codomain `L -> M`, and a new kind of visibility on the arrow <br>
itself. But that means it's not just the binder of the implicit parameter <br>
that has a new visibility, but the arrow as well. And isn't that what <br>
`AnonArgFlag` is for?<br>
<br>
> I think the route you're taking is a reasonable route to your <br>
> destination, but I'm not yet convinced it's a destination I want GHC to <br>
> travel to. As I hint above, I think the feature would have to be <br>
> expanded somewhat to cover its likely use cases, and yet I worry that it <br>
> will not be widely enough used to make its specification and <br>
> implementation worthwhile. I'm happy to be convinced otherwise, though.<br>
<br>
Fair enough. Although I was hoping that with Dependent Haskell, we would <br>
have more situations where unification can give useful solutions, and so <br>
we would want the feature of implicit arguments (even for terms!).<br>
<br>
But if there's no appetite from GHC for partial type synonyms, what would <br>
help me a lot in keeping this maintainable / avoiding churn in chasing <br>
`master` would be if I can upstream two refactorings that are enablers <br>
for my implementation but don't actually change any existing behaviour:<br>
<br>
* Adding "does it come from a wildcard" flag to `TauTv` <br>
(<a href="https://gitlab.haskell.org/cactus/ghc/-/commit/e8be2cb2b1093275385467741b1297ce91ef7547" rel="noreferrer noreferrer" target="_blank">https://gitlab.haskell.org/cactus/ghc/-/commit/e8be2cb2b1093275385467741b1297ce91ef7547</a>)<br>
<br>
* Changing `isCompleteHsSig` to run in `TcM`, so that its result can <br>
depend on type constructor details<br>
(<a href="https://gitlab.haskell.org/cactus/ghc/-/commit/49f60ef13ad7f63f91519ca88cd8095db0781c92" rel="noreferrer noreferrer" target="_blank">https://gitlab.haskell.org/cactus/ghc/-/commit/49f60ef13ad7f63f91519ca88cd8095db0781c92</a>)<br>
<br>
* Maybe a third one, depending on what we come up with for the <br>
representation of these implicit binders<br>
<br>
What do you think about this?<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>
_______________________________________________<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>