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/d3165c3f37e9455bc7ca88b884cc3...
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ő
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-ty...
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@erdi.hu =-------'