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ő <ge...@erdi.hu> 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ő <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
