Wildcards in type synonyms

[Iavor Diatchki]

Hello,

I've implemented such a feature in Cryptol, not GHC, so it is quite doable,
but I think the implementation would be easier if you decided on the
overall design of the feature first.

Some things to consider:
  * these kind of "existential" variable make sense in other type
signatures, not just type synonyms
   * there might be some contexts where you may want to disallow such
wildcards (e. g., in a data declaration)
   * you have to be careful with the scoping of type variables.  For
example, you should not unify an existential/wildcard variable with a type
that refers to variables that are not in scope of the wildcard.  I don't
remember if GHC already has a system for such things, but in Cryptol we
implanted this by having each unification variable keep track of the
quantified variables that it may depend on.

Hope this helps,
Iavor

On Fri, Jul 22, 2022, 09:30 ÉRDI Gergő <gergo at erdi.hu> wrote:

> Hi,
>
> I'd like to implement type synonyms containing wildcards. The idea is
> that if you have `type MySyn a = MyType a _ Int`, then during
> typechecking, every occurrence of `MySyn T` would be expanded into
> `MyType T w123 Int`, with a fresh type (meta)variable `w123`.
>
> One worrying thing I noticed in my initial exploration of the GHC
> codebase is that the Core representation of `Type`s can still contain
> type synonym occurrences. And this doesn't seem like just an artefact
> of sharing the `Type` representation with `TcType`, since the
> `coreView` function also has code to look through type synonyms.
>
> What is the reason for this? I would have expected type synonyms to be
> only relevant during typechecking, and then fully resolved in the
> elaborated Core output. If that were the case, then a new version of
> `expand_syn` could live in `TcM` and take care of making these fresh
> metavariables.
>
> Beside this concrete question, taking a step back, I would also like
> to hear from people who know their way around this part of GHC, what
> they think about this and how they'd approach implementing it.
>
> Thanks,
>          Gergo
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20220722/64b7f9b7/attachment.html>