Partial type synonyms -- first-class!

[ÉRDI Gergő]

Hi Richard,

Thanks for getting back to me! My replies are inline below.

On Thu, 11 Aug 2022, Richard Eisenberg wrote:

> You want a third:
>
> C. invisible parameters that are filled in with a fresh wildcard.
>
> We would need to have some way of writing out the type of such a thing 
> (i.e. what kind would `Syn` have?), but I presume this is possible.

I think there's a tension between this and your suggestion to only add 
implicit parameters as a new `TyConBndrVis`, but more on that below.

>> 2. Using partial type synonyms
>>
>>
>
> This bit also makes sense, but I think users will want more 
> functionality. Specifically, what if a user does not want a wildcard 
> inserted, because they know that the right choice is `Int`? Or maybe 
> they want a *named* wildcard inserted. My experience is that once 
> something can be done implicitly, folks will soon find good reasons to 
> do it explicitly on occasion.

Good point, but I think we can punt on this and not close any doors ahead. 
So today, you would only be able to write `Syn T` to mean `Syn {_} T`, and 
then in the future we can add typechecker support (and new surface 
syntax!) for `Syn {S} T`, without causing any compatibility problems with 
any existing code that doesn't give explicit args for implicit params.

>> 3. Implementation
>>
>>
>>  * When typechecking a type application, implicit arguments get
>>    filled with the result of `tcAnonWildCardOcc`.
>
> What about named wildcards? Even if they're not passed in, perhaps someone wants
>
> type SomeEndo = _t -> _t
>
> where the two types are known to be the same, but we don't know what.

This would be something to support when typechecking the definition, not a 
given application. Your example would still elaborate to

     type SomeEndo {t} = t -> t

it would just use the same implicitly-bound type parameter `t` twice on 
the right-hand side. But when you use `SomeEndo`, the usage would still 
elaborate into a (single) anonymous wildcard argument, i.e.
`SomeEndo {_}`.

My current implementation doesn't support your example, but I think it's 
only because the renamer rejects it. I think if I get it through the 
renamer, it should already work because that `_t` will typecheck into a 
wildcard `TauTv`.

>> 3. Similar to #1, I started just pushing all the way through GHC a
>> change to `AnonArgFlag` that adds a third `ImplArg` flag.
>
> I don't love adding a new constructor to AnonArgFlag, because that's 
> used in terms. Instead, it would be great to localize this new extension 
> to tycon binders somehow.

OK so while I'd love to get away with only changing `TyConBndrVis`, this 
is the part of your email that I don't understand how to do :/

First, when a type application is typechecked, we only have the kind of 
the type constructor, not its binders (and that makes sense, since we 
could be applying something more complex than directly a defined type 
constructor). So if I only add a new `TyConBndrVis` constructor, then I 
have no way of representing this in the `tyConKind` and so no way of 
finding out that I need to put in implicit args in `tcInferTyApps`.

Second, you ask what the kind of `Syn` in e.g. `type Syn a = TC _ a` is. I 
think (supposing `TC :: K -> L -> M`) its kind should be (stealing syntax 
from Agda) something like `{K} -> L -> M`, i.e. a function kind with 
domain `K`, codomain `L -> M`, and a new kind of visibility on the arrow 
itself. But that means it's not just the binder of the implicit parameter 
that has a new visibility, but the arrow as well. And isn't that what 
`AnonArgFlag` is for?

> I think the route you're taking is a reasonable route to your 
> destination, but I'm not yet convinced it's a destination I want GHC to 
> travel to. As I hint above, I think the feature would have to be 
> expanded somewhat to cover its likely use cases, and yet I worry that it 
> will not be widely enough used to make its specification and 
> implementation worthwhile. I'm happy to be convinced otherwise, though.

Fair enough. Although I was hoping that with Dependent Haskell, we would 
have more situations where unification can give useful solutions, and so 
we would want the feature of implicit arguments (even for terms!).

But if there's no appetite from GHC for partial type synonyms, what would 
help me a lot in keeping this maintainable / avoiding churn in chasing 
`master` would be if I can upstream two refactorings that are enablers 
for my implementation but don't actually change any existing behaviour:

* Adding "does it come from a wildcard" flag to `TauTv` 
(https://gitlab.haskell.org/cactus/ghc/-/commit/e8be2cb2b1093275385467741b1297ce91ef7547)

* Changing `isCompleteHsSig` to run in `TcM`, so that its result can 
depend on type constructor details
(https://gitlab.haskell.org/cactus/ghc/-/commit/49f60ef13ad7f63f91519ca88cd8095db0781c92)

* Maybe a third one, depending on what we come up with for the 
representation of these implicit binders

What do you think about this?

Thanks,
 	Gergo