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

Reply via email to