Re: Wildcards in type synonyms

Wild guess: you aren't instantiating the kinds of the meta-tyvars to something sensible, so kinds don't line up. Eg. where are k_ax9 and k_awW bound? You need to be super-careful about the *level* of wildcards. That is a tricky bit about the whole wildcard implementation. I'm still unconvinced whether this is a good use of your valuable time -- but of course that is up to you. Simon On Thu, 28 Jul 2022 at 06:53, ÉRDI Gergő wrote:

(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?