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@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs