(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ő <ge...@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?
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
