Partial type synonyms -- first-class!

5 Aug 2022

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

ÉRDI Gergő

Gergő Érdi

Richard Eisenberg

ÉRDI Gergő

Edward Kmett

Gergő Érdi

Simon Peyton Jones

tags

participants (5)