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 =-------'