If you're trying to understand core, check out https://github.com/ghc/ghc/blob/master/docs/core-spec/core-spec.pdf which has all the typing rules. It might be helpful.
But your analysis below is spot on. Richard On Aug 16, 2015, at 10:19 AM, Alexander Eyers-Taylor <[email protected]> wrote: > Hello > > I have reread the comment about TyConAppCo and I now understand how it works > and this is all how it should work. I was just slightly confused to start > with. The coercion was representational but the arguments were nominal. > > Thanks > > Alex > > On 16/08/15 13:34, Richard Eisenberg wrote: >> Hi Alex, >> >> Do you have a concrete example? With the -dcore-lint flag, the Core is >> checked, including all the roles. >> >> Thanks, >> Richard >> >> On Aug 16, 2015, at 7:47 AM, Alexander Eyers-Taylor >> <[email protected]> wrote: >> >>> Hello >>> >>> I have noticed in looking at some core that GADT type constructors are >>> often applied with a representational role. These constructors are >>> explicitly marked as nominal. >>> >>> Is this information just ignored at a Core level or is this invalid core? >>> >>> Looking at the code a see that we if we downgrade a TyConAppCo we >>> unconditionally change it to a representational role after changing its >>> children. I think this is where it is introduced. >>> >>> Alex ET >>> _______________________________________________ >>> ghc-devs mailing list >>> [email protected] >>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
