Wildcards in type synonyms

[ÉRDI Gergő]

On Fri, 22 Jul 2022, Iavor Diatchki wrote:

> 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.

I'm hoping the details pretty much fall out from what it would mean if I 
used the existing PartialTypeSignatures extension to write 'MyData T _ Int`
at those places.

> 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.