Wildcards in type synonyms

[ÉRDI Gergő]

(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ő <gergo at 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. 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?
> 
> 
>