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

Reply via email to