(TL;DR: `newMetaTyVarX` gives me type metavars that behave weirdly and I don't understand why. What shoudl I use instead?) OK so I have two half-done implementations now: * Doing `HsType`-level substitution in the middle of `tc_infer_hs_type` (see my exchange with Richard on why this needs to happen in `tc_infer_hs_type` instead of `rnHsTyKi`) * Doing Core `Type`-level substitution in the middle of `tc_infer_hs_type` The advantage of the first one is that it works :) The disadvantage is that it involves storing a `HsType` in a `TyCon`, which in turn means making it work inter-module will require an `Iface` representation for `HsType`s. Hence the second attempt. I think that would be a more principled solution anyway. This approach is based on typechecking the macro's right-hand side into a core `Type`, and storing that, and the list of wildcard-originating `TyVar`s, in the `TyCon`. At every occurrence site, I take this core `Type` and apply a substitution on it that is the composition of the following two: * A substitution from macro type synonym type parameters to the type arguments * An instantiation of each wildcard variable into a fresh metavariable Unfortunately, it is this second step that is tripping me up. If I use `newMetaTyVarX` to make these "refreshing" metavars, then while the substitution looks OK when eyeballing it, the resulting *type* metavariables seem to be handled by GHC as if they were *kind* metavariables?! Here's an example. The source input is: ``` {-# LANGUAGE NoPolyKinds, NoStarIsType #-} -- Makes it easier to see how it goes wrong data MyData a b c = MkMyData a b c type MySyn a = MyData a _ Int f1 :: MyData a b c -> b f1 (MkMyData _ x _) = x f2 :: MySyn a -> Double f2 = f1 ``` I start with the following "macro type template" (using `-dppr-debug` format): ``` TySynWildcard.MyData{tc r3} (a{tv auq} Nothing [sk:1] :: GHC.Types.Type{(w) tc 32Q}) ((w_awX{tv} Nothing [tau:0] :: (k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q})) |> {(co_awY{v} Just 'GHC.Types.Many{(w) d 65I} [lid[CoVarId]] :: GHC.Prim.~#{(w) tc 31I} GHC.Types.Type{(w) tc 32Q} GHC.Types.Type{(w) tc 32Q} (k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q}) GHC.Types.Type{(w) tc 32Q})}) GHC.Types.Int{(w) tc 3u} ``` The substitution applied: ``` [TCvSubst In scope: InScope {a{tv auu} k_awW{tv} w_axc{tv}} Type env: [auq :-> (a{tv auu} Nothing [sk:2] :: (k_ax9{tv} Nothing [tau:2] :: GHC.Types.Type{(w) tc 32Q})), awX :-> (w_axc{tv} Nothing [tau:2] :: (k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q}))] Co env: []] ``` Note that the second type substitution, (w_awX :: k_awW) :-> (w_axc :: k_awW) is the one that should take care of instantiating the wildcard metavariable. And the result of applying this substitution still looks OK: ``` TySynWildcard.MyData{tc r3} (a{tv auu} Nothing [sk:2] :: (k_ax9{tv} Nothing [tau:2] :: GHC.Types.Type{(w) tc 32Q})) ((w_axc{tv} Nothing [tau:2] :: (k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q})) |> {(co_awY{v} Just 'GHC.Types.Many{(w) d 65I} [lid[CoVarId]] :: GHC.Prim.~#{(w) tc 31I} GHC.Types.Type{(w) tc 32Q} GHC.Types.Type{(w) tc 32Q} (k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q}) GHC.Types.Type{(w) tc 32Q})}) GHC.Types.Int{(w) tc 3u} ``` But soon after, typechecking fails: ``` • Couldn't match type ‘Type’ with ‘Double’ Expected: MyData a Type Int -> Double Actual: MyData a Type Int -> Type • In the expression: f1 In an equation for ‘f2’: f2 = f1 ``` So this is weird. Instead of unification solving `w_axc ~ Double`, it seems `w_axc` is left unrestricted, and then `NoPolyKinds` picks it up as a kind variable (why?) and defaults it to `Type`. As an experiment, I have also tried *not* refreshing `w_awX`, only substituting in the type arguments. Now, of course, this can't possibly work as soon as I have more than one occurrence of `MySyn` due to the interference between the wildcard metavars, but if I only have one, then the program typechecks. So to me this suggests I'm doing things mostly right, except that the metavar returned by `newMetaTyVarX` is not fit for my use case. What should I use instead of `newMetaTyVarX` to instantiate / "refresh" the (wildcard-originating) type metavariables in my "macro type template"? Thanks, Gergo On Mon, 25 Jul 2022, Simon Peyton Jones wrote:

I'm afraid I don't understand, but it sounds delicate.  By all means try!

Simon

On Mon, 25 Jul 2022 at 11:04, É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. 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.

Does this make sense?