Partial type synonyms -- first-class!

[Gergő Érdi]

I haven't heard back on this so I pushed ahead on the 3 outstanding
problems by just applying more violence to the code base, basically.

1. For wildcard-originating type variables, I added a flag to the
`TauTv` constructor of `MetaInfo`. The knock-on effects of this change
were smaller than I expected:
https://gitlab.haskell.org/cactus/ghc/-/commit/d3165c3f37e9455bc7ca88b884cc370ca39d07f8

2. It turns out I misunderstood the `Role` situation and they are
actually computed via some weird knot tying from the `TyCon` itself.
So on one hand, I don't really need to do anything to "come up with"
roles for these implicit type parameters. On the other hand, I think
this also means that this breaks the surface syntax for role
declarations, since the user would be expected to give roles for type
parameters they never explicitly added to their tysyns...

3. Similar to #1, I started just pushing all the way through GHC a
change to `AnonArgFlag` that adds a third `ImplArg` flag. It is
handled mostly the same way as an `InvisArg`, except `tcInferTyApps`
can use it to insert wildcard arguments. I don't have a full commit
for this yet.

Beside comments on this approach, I would also like to hear from Simon
& Richard if they agree that with this new approach, this could now be
a real language feature that could get upstreamed once all these
implementation wrinkles are smoothed out.

Thanks,
  Gergo

On Fri, Aug 5, 2022 at 6:17 PM ÉRDI Gergő <gergo at erdi.hu> wrote:
>
> As I mentioned at the end of the original thread (but probably no one
> was interested in this enough to read that far), after a breakthrough
> idea I have now started working on partial type synonyms that are NOT
> just defined using macro expansion semantics, and indeed can be a
> first-class abstraction. I think if I can iron out the wrinkles
> detailed at the bottom of this message, this would be good for a GHC
> proposal.
>
> 1. Defining partial type synonyms
>
> The idea is to typecheck the type synonym declaration
>
>      type Syn a = MyType _ [a] Int
>
> into a type synonym that has some implicit (invisible) type parameters:
>
>      type Syn {w1} a = MyType w1 [a] Int
>
> We don't need to come up with any new design for "what this means":
> this means exactly the same as
>
>      type Syn w1 a = MyType w1 [a] Int
>
> which is something you can already write today. The only difference is
> how `w1` is given at use sites.
>
> 2. Using partial type synonyms
>
> When a partial type synonym is applied, its argument list is expanded
> by adding wildcard arguments for the invisible parameters. So this use
> site:
>
>      Syn Double
>
> is typececked into the type application
>
>      Syn {_} Double
>
> Again, we don't need to come up with any new design for "what this
> means": this is the same as writing `Syn _ Double` into the same
> position, it's just the `_` is not written in the surface syntax.
>
> In particular:
>
>    * The level of the type variable conjured for the `_` is determined
>      fully by where the `Syn Double` occurs, and not at all by the
>      definition of `Syn`
>
>    * Using the type synonym `Syn` is only valid where a wildcard
>      occurrence would be valid. In particular, using `Syn` in a type
>      signature causes the signature itself to be regarded as partial
>      (`isCompleteHsSig` returns `False` for it).
>
> 3. Implementation
>
> I have a proof-of-concept implementation at
> https://gitlab.haskell.org/cactus/ghc/-/compare/master...cactus%2Fpartial-tysyns?from_project_id=1117
>
> I tried to make it as small a change as I could. Its key points are:
>
>    * In the renamer, we allow wildcards in `TySynCtx` context
>
>    * In `tcTySynRhs`, we allow wildcards in the right-hand side,
>      retrieve them from the result of typechecking, and intersperse
>      them with the "normal" type parameters to get a well-scoped
>      telescope.
>
>    * About a third of the lines changed is just a boring refactoring of
>      `isCompleteHsSig` to be able to look up type synonym
>      `TyCon`s. This is needed because a type signature referring to
>      partial type synonyms will be partial itself once those type
>      synonym applications are elaborated.
>
>    * When typechecking a type application, implicit arguments get
>      filled with the result of `tcAnonWildCardOcc`.
>
> Now, my questions about the problems I've encountered along the way. I
> hope these questions are concrete enough that I can get concrete
> answers to them from this list:
>
> 1. How do I find the wildcard-originating tyvars robustly? Currently,
> I am using `candidateQTyVarsWithBinders` but that picks up "regular"
> out-of-scope tyvars as well. I believe this causes a regression of
> #17567; furthermore, it means if the user writes `type Syn a = Foo b` it
> is handled the same as if they wrote `type Syn a = Foo _`, but it would
> be better to reject it instead.
>
> 2. What should the `Role` of these implicit type parameters be? For
> now, I've went with `Nominal` for lack of a better answer.
>
> 3. When typechecking a type application, I need to insert wildcards
> for these implicit arguments. I am currently using `AnonTCB InvisArg`
> binders to represent these implicit type parameters, which means by
> the time I get to `tcInferTyApps`, they would get passed through
> `instantiate` to `tcInstInvisibleTyBinder`. I currently have a
> horrible kuldge here to check, before calling
> `tcInstInivisibleTyBinder`, that the invisible binder's kind doesn't
> meet the preconditions of it; and if it doesn't, I create a wildcard
> instead. But of course, it would be nicer if I could put something in
> the `TcTyConBinder` that identifies these binders properly.
>
> Thanks in advance,
>         Gergo
>
> --
>
>    .--= ULLA! =-----------------.
>     \     http://gergo.erdi.hu   \
>      `---= gergo at erdi.hu =-------'