Wildcards in type synonyms

[Simon Peyton Jones]

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ő <gergo at 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ő <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?
> >
> >
> >
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20220728/38270d59/attachment.html>