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 <li...@richarde.dev> wrote: > > > > > On Jul 25, 2022, at 6:04 AM, ÉRDI Gergő <ge...@erdi.hu> 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 > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs