Wildcards in type synonyms

[ÉRDI Gergő]

On Thu, 28 Jul 2022, Simon Peyton Jones wrote:

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

`a_auu :: k_ax9` is the result of typechecking my type argument (the `a` 
in the source type `MySyn a`), so I would expect its kind to work because 
it is computed by parts of GHC that I am not changing.

`w_awX :: k_awW` is the metavariable created during the typechecking of 
the right-hand side of my type macro `type MySyn a = MyData a _ Int`. This
kind is then kept for the fresh metavariable that I try to replace `w_awX` 
with, since I have `w_axc :: k_awW`.

The part that confuses me the most is that the right-hand side seems to 
work just fine on its own:

>       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 I have two versions of my code returning two types from 
`tc_infer_hs_type` that only differ in containing either `w_awX :: k_awW` 
or `w_axc :: k_awW`, and one of them typechecks while the other causes a 
type error.

Typechecks (as long as only used once of course):

```
   TySynWildcard.MyData{tc r3}
     (a{tv auu} Nothing [sk:2] :: (k_ax9{tv} Nothing [tau:2] :: 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}
```

Doesn't typecheck:

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

What is the difference?