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.

Thanks Simon, these are very useful hints. My plan is to just push ahead on a separate fork, with this "macro semantics", and maybe if it comes out nicer than I'd hope, I'll propose it. So it seems that instead of shoehorning it into the existing type synonyms, a better bet would be to branch off to a separate path quite early (maybe as soon as during renaming), expand them during typechecking, and *not* touch how/when existing "normal" type synonyms are resolved. On Fri, Jul 22, 2022 at 4:14 PM Simon Peyton Jones wrote:

Hi Gergo

...

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

I imagine you mean that if you then write f :: MySyn a -> a -> Int then it's exactly as if you wrote (using PartialTypeSignatures) f :: MyType a _ Int -> a -> Int today. So if I understand it right, you intend that these type synonyms are second-class citizens: they can occur precisely (and only) where wildcards are allowed to occur today. For example, as Iavor suggests, you'd reject data T a = MkT (MySyn a)

If you want to do this in a fork of GHC, that's obviously fine. If you want to offer it as a language extension, the best thing would be to write a GHC Proposal. Also you'd get a lot of useful design feedback that way, which might save you implementation cycles.

...

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.

In GHC an Id has only one type. It does not have a "source type" and a "Core type". So we allow Core types to contain synonyms so that when we export that Id the importing scope (e.g. GHCi, and type error messages) can see it. Synonyms can also allow types to take less space. E.g. we have Type, where (if we fully expanded) we'd have to have (TYPE LiftedRep). One could imagine a different design.

I would expect that, by the time typechecking is over, all your wildcard synonyms are gone. They really are second class.

Just to mention too that the entire "wildcards in type signatures" story is (I think) jolly useful, but it also turned out to be pretty tricky to implement. If you just macro-expand your new synonyms, you won't disturb the wildcard story, but I just wanted to advertise that it's a tricky area.

Simon

On Fri, 22 Jul 2022 at 07:30, ÉRDI Gergő 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

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

On Jul 22, 2022, at 4:53 AM, Simon Peyton Jones wrote:

expand them during typechecking,

Just to expand on this point (haha): your new type macros (distinct from type synonyms) would have to be eagerly expanded during type checking. You say this (quoted above), but I wanted to highlight that this is in opposition to the way today's type synonyms work, which are expanded only when necessary. (Rationale: programmers probably want to retain the very clever synonym name they came up with, which is hopefully easier to reason about.) Interestingly, type macros may solve another problem that has come up recently: Gershom proposed (a quick search couldn't find where this was, but it was around restoring deep-subsumption behavior) a change to the way polytypes work in type synonyms. Specifically, he wondered about, e.g. type T a = forall b. b -> Either a b meaning to take the `forall b` and lift it to the top of whatever type T appears in. So that f :: [a] -> T a would really mean f :: forall a b. [a] -> b -> Either a b and not f :: forall a. [a] -> forall b. b -> Either a b as it does today. With deep subsumption, you can spot the difference between these types only with type applications, but they are incomparable types with simple subsumption. At the time, I didn't understand what the semantics of Gershon's new type synonyms were, but in the context of Gergo's type macros, they make sense. To wit, we could imagine type T a = b -> Either a b Note: b is unbound. This is actually a type *macro*, not a type synonym, and it expands to a form that mentions a free variable b. (Presumably, this b would not capture a b in scope at the usage site.) This macro behavior delivers what Gershom was looking for. I'm not saying Gergo should necessarily implement this new aspect of type macros (that don't mention wildcards), but if this ever does come to a proposal, I think these kind of variables are a new motivator for such a proposal. I'd probably favor some explicit notation to introduce a macro (e.g. `type macro T a = Either _ a`) instead of using a syntactic marker like the presence of a _ or an unbound variable, but we can debate that later. Good luck with the implementation, Gergo! Richard

Do we have an existing way of substituting types over type variables, *in HsType instead of Core Type*?

I'm afraid not. Currently HsType is not processed much -- just renamed and typechecked into a Type. The nearest we have is Note [Handling overloaded and rebindable constructs], in the renamer. That doesn't do what you want, but the HsExpansion idea is close S On Mon, 25 Jul 2022 at 10:18, ÉRDI Gergő wrote:

On Fri, 22 Jul 2022, Simon Peyton Jones wrote:

...

So it seems that instead of shoehorning it into the existing type synonyms, a better bet would be to branch off to a separate path

quite

...

early (maybe as soon as during renaming), expand them during typechecking, and *not* touch how/when existing "normal" type

synonyms

...

are resolved.

That sounds plausible, yes.

Do we have an existing way of substituting types over type variables, *in HsType instead of Core Type*?

On Jul 25, 2022, at 6:04 AM, ÉRDI Gergő wrote:

On Mon, 25 Jul 2022, Simon Peyton Jones wrote:

...

Do we have an existing way of substituting types over type variables, *in HsType instead of Core Type*? I'm afraid not. Currently HsType is not processed much -- just renamed and typechecked into a Type.

I wonder if, instead, I could expand the rhs, typecheck it "abstractly" (i.e. in the context of the synonym's binders), and THEN do the substitution.

Why type-check the RHS at all? Presumably, to give nice error messages. But it looks like this aspect of the plan is inessential. To be clear, I *do* think you should type-check the RHS, but I'm also checking my understanding here. If type-checking the RHS is indeed inessential, then the result of that type-checking (a desugared `Type`) should be discarded.

If I typecheck the rhs for every occurrence, I should get fresh metavars for each wildcard, which is pretty much what I want. I just have to make sure I don't zonk before the substitution.

I see this substitution as happening before any type-checking, so zonking shouldn't be an issue. That is, I would expect a substHsTy :: UniqFM Name (HsType GhcRn) -> HsType GhcRn -> HsType GhcRn to do the work, entirely before type-checking. (Presumably, you don't want the macro-like behavior to extend to fixity resolution. That is, if we have type macro T a = a + b and then write `f :: T Int * Double`, we want `f :: (Int + b) * Double`, not `f :: Int + (b * Double)`. If you indeed want the latter (strange days!), then you'd need to be careful to do the substitution before fixity resolution, just after renaming.) Richard

Does this make sense? _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Yes, your approach makes sense, and you're right that my during-the-renamer approach would struggle a bit. Go with your idea. :) Richard

On Jul 25, 2022, at 9:21 AM, Gergő Érdi wrote:

So my idea from my last email is to avoid the need for `substHsTy`: When `tc_hs_type` encounters a macro occurrence, I would `tcLHsType` the rhs then and there (thereby getting fresh metas for each wildcard), use `substTy` to instantiate with the given type arguments. Then `tc_hs_type` returns that.

Note that this is NOT about typechecking the rhs *for the definition*, but rather, using `tcLHsType` as the function that creates fresh metas for each wildcard.

On Mon, Jul 25, 2022 at 8:58 PM Richard Eisenberg wrote:

...

...

On Jul 25, 2022, at 6:04 AM, ÉRDI Gergő wrote:

On Mon, 25 Jul 2022, Simon Peyton Jones wrote:

...

Do we have an existing way of substituting types over type variables, *in HsType instead of Core Type*? I'm afraid not. Currently HsType is not processed much -- just renamed and typechecked into a Type.

I wonder if, instead, I could expand the rhs, typecheck it "abstractly" (i.e. in the context of the synonym's binders), and THEN do the substitution.

Why type-check the RHS at all? Presumably, to give nice error messages. But it looks like this aspect of the plan is inessential. To be clear, I *do* think you should type-check the RHS, but I'm also checking my understanding here. If type-checking the RHS is indeed inessential, then the result of that type-checking (a desugared `Type`) should be discarded.

...

If I typecheck the rhs for every occurrence, I should get fresh metavars for each wildcard, which is pretty much what I want. I just have to make sure I don't zonk before the substitution.

I see this substitution as happening before any type-checking, so zonking shouldn't be an issue. That is, I would expect a

substHsTy :: UniqFM Name (HsType GhcRn) -> HsType GhcRn -> HsType GhcRn

to do the work, entirely before type-checking.

(Presumably, you don't want the macro-like behavior to extend to fixity resolution. That is, if we have

type macro T a = a + b

and then write `f :: T Int * Double`, we want `f :: (Int + b) * Double`, not `f :: Int + (b * Double)`. If you indeed want the latter (strange days!), then you'd need to be careful to do the substitution before fixity resolution, just after renaming.)

Richard

...

Does this make sense? _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

It sounds awfully special-case to store these type macros in a new field of `TcGblEnv` instead of as just another kind of `TyCon`.

But all this is just in your personal fork of GHC, so you can be as special-case as you like. I'd just plough ahead and do the easiest thing. If you make a proposal, and persuade the committee, we can look again. Until then it's probably not worth us spending a lot of time making the implementation beautiful. Simon On Tue, 26 Jul 2022 at 04:14, ÉRDI Gergő wrote:

On Mon, 25 Jul 2022, Richard Eisenberg wrote:

...

I see this substitution as happening before any type-checking, so zonking shouldn't be an issue. That is, I would expect a

substHsTy :: UniqFM Name (HsType GhcRn) -> HsType GhcRn -> HsType GhcRn

to do the work, entirely before type-checking.

If I were to do this fully during renaming, how do I even find out that a `Name` refers to a type macro? During typechecking I can look up the `TyThing`, see if it's a `MacroTyCon`, and get the rhs from that. But I don't think we store anything about already-renamed declarations during renaming the same way we store info about already-typechecked things during typechecking in `tcg_type_env`.

It sounds awfully special-case to store these type macros in a new field of `TcGblEnv` instead of as just another kind of `TyCon`.