<div dir="ltr"><div class="gmail_default" style="font-family:tahoma,sans-serif">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?</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">You need to be super-careful about the *level* of wildcards. That is a tricky bit about the whole wildcard implementation.</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">I'm still unconvinced whether this is a good use of your valuable time -- but of course that is up to you.</div><div class="gmail_default" style="font-family:tahoma,sans-serif"><br></div><div class="gmail_default" style="font-family:tahoma,sans-serif">Simon<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Thu, 28 Jul 2022 at 06:53, ÉRDI Gergő <<a href="mailto:gergo@erdi.hu">gergo@erdi.hu</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">(TL;DR: `newMetaTyVarX` gives me type metavars that behave weirdly and I <br>
don't understand why. What shoudl I use instead?)<br>
<br>
OK so I have two half-done implementations now:<br>
<br>
* Doing `HsType`-level substitution in the middle of `tc_infer_hs_type`<br>
(see my exchange with Richard on why this needs to happen in<br>
`tc_infer_hs_type` instead of `rnHsTyKi`)<br>
<br>
* Doing Core `Type`-level substitution in the middle of `tc_infer_hs_type`<br>
<br>
The advantage of the first one is that it works :) The disadvantage is <br>
that it involves storing a `HsType` in a `TyCon`, which in turn means <br>
making it work inter-module will require an `Iface` representation for <br>
`HsType`s.<br>
<br>
Hence the second attempt. I think that would be a more principled solution <br>
anyway. This approach is based on typechecking the macro's right-hand side <br>
into a core `Type`, and storing that, and the list of wildcard-originating <br>
`TyVar`s, in the `TyCon`. At every occurrence site, I take this core <br>
`Type` and apply a substitution on it that is the composition of the <br>
following two:<br>
<br>
* A substitution from macro type synonym type parameters to the type <br>
arguments<br>
* An instantiation of each wildcard variable into a fresh metavariable<br>
<br>
Unfortunately, it is this second step that is tripping me up. If I use <br>
`newMetaTyVarX` to make these "refreshing" metavars, then while the <br>
substitution looks OK when eyeballing it, the resulting <br>
*type* metavariables seem to be handled by GHC as if they were *kind* <br>
metavariables?!<br>
<br>
Here's an example. The source input is:<br>
<br>
```<br>
{-# LANGUAGE NoPolyKinds, NoStarIsType #-} -- Makes it easier to see how it goes wrong<br>
<br>
data MyData a b c = MkMyData a b c<br>
type MySyn a = MyData a _ Int<br>
<br>
f1 :: MyData a b c -> b<br>
f1 (MkMyData _ x _) = x<br>
<br>
f2 :: MySyn a -> Double<br>
f2 = f1<br>
```<br>
<br>
I start with the following "macro type template" (using `-dppr-debug` format):<br>
<br>
```<br>
TySynWildcard.MyData{tc r3}<br>
(a{tv auq} Nothing [sk:1] :: GHC.Types.Type{(w) tc 32Q})<br>
((w_awX{tv} Nothing [tau:0] :: (k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q}))<br>
|> {(co_awY{v} Just 'GHC.Types.Many{(w) d 65I} [lid[CoVarId]] :: GHC.Prim.~#{(w) tc 31I}<br>
GHC.Types.Type{(w) tc 32Q}<br>
GHC.Types.Type{(w) tc 32Q}<br>
(k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q})<br>
GHC.Types.Type{(w) tc 32Q})})<br>
<a href="http://GHC.Types.Int" rel="noreferrer" target="_blank">GHC.Types.Int</a>{(w) tc 3u}<br>
```<br>
<br>
The substitution applied:<br>
<br>
```<br>
[TCvSubst<br>
In scope: InScope {a{tv auu} k_awW{tv} w_axc{tv}}<br>
Type env: [auq :-> (a{tv auu} Nothing [sk:2] :: (k_ax9{tv} Nothing [tau:2] :: GHC.Types.Type{(w) tc 32Q})),<br>
awX :-> (w_axc{tv} Nothing [tau:2] :: (k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q}))]<br>
Co env: []]<br>
```<br>
<br>
Note that the second type substitution, (w_awX :: k_awW) :-> (w_axc :: k_awW) is the <br>
one that should take care of instantiating the wildcard metavariable. And <br>
the result of applying this substitution still looks OK:<br>
<br>
```<br>
TySynWildcard.MyData{tc r3}<br>
(a{tv auu} Nothing [sk:2] :: (k_ax9{tv} Nothing [tau:2] :: GHC.Types.Type{(w) tc 32Q}))<br>
((w_axc{tv} Nothing [tau:2] :: (k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q}))<br>
|> {(co_awY{v} Just 'GHC.Types.Many{(w) d 65I} [lid[CoVarId]] :: GHC.Prim.~#{(w) tc 31I}<br>
GHC.Types.Type{(w) tc 32Q}<br>
GHC.Types.Type{(w) tc 32Q}<br>
(k_awW{tv} Nothing [tau:0] :: GHC.Types.Type{(w) tc 32Q})<br>
GHC.Types.Type{(w) tc 32Q})})<br>
<a href="http://GHC.Types.Int" rel="noreferrer" target="_blank">GHC.Types.Int</a>{(w) tc 3u}<br>
```<br>
<br>
But soon after, typechecking fails:<br>
<br>
```<br>
• Couldn't match type ‘Type’ with ‘Double’<br>
Expected: MyData a Type Int -> Double<br>
Actual: MyData a Type Int -> Type<br>
• In the expression: f1<br>
In an equation for ‘f2’: f2 = f1<br>
```<br>
<br>
So this is weird. Instead of unification solving `w_axc ~ Double`, it <br>
seems `w_axc` is left unrestricted, and then `NoPolyKinds` picks it up as <br>
a kind variable (why?) and defaults it to `Type`.<br>
<br>
As an experiment, I have also tried *not* refreshing `w_awX`, only <br>
substituting in the type arguments. Now, of course, this can't possibly <br>
work as soon as I have more than one occurrence of `MySyn` due to the<br>
interference between the wildcard metavars, but if I only have one, then<br>
the program typechecks. So to me this suggests I'm doing things mostly <br>
right, except that the metavar returned by `newMetaTyVarX` is not fit for <br>
my use case.<br>
<br>
What should I use instead of `newMetaTyVarX` to instantiate / "refresh" <br>
the (wildcard-originating) type metavariables in my "macro type template"?<br>
<br>
Thanks,<br>
Gergo<br>
<br>
<br>
On Mon, 25 Jul 2022, Simon Peyton Jones wrote:<br>
<br>
> I'm afraid I don't understand, but it sounds delicate. By all means try!<br>
> <br>
> Simon<br>
> <br>
> On Mon, 25 Jul 2022 at 11:04, ÉRDI Gergő <<a href="mailto:gergo@erdi.hu" target="_blank">gergo@erdi.hu</a>> wrote:<br>
> On Mon, 25 Jul 2022, Simon Peyton Jones wrote:<br>
><br>
> > Do we have an existing way of substituting types over type<br>
> variables, *in<br>
> > HsType instead of Core Type*?<br>
> ><br>
> ><br>
> > I'm afraid not. Currently HsType is not processed much -- just renamed<br>
> and typechecked<br>
> > into a Type.<br>
><br>
> I wonder if, instead, I could expand the rhs, typecheck it "abstractly"<br>
> (i.e. in the context of the synonym's binders), and THEN do the<br>
> substitution. If I typecheck the rhs for every occurrence, I should get<br>
> fresh metavars for each wildcard, which is pretty much what I want. I just<br>
> have to make sure I don't zonk before the substitution.<br>
><br>
> Does this make sense?<br>
> <br>
> <br>
></blockquote></div>