A question about roles.

Richard Eisenberg eir at cis.upenn.edu
Sun Aug 16 17:01:15 UTC 2015


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 <aeyerstaylor11 at gmail.com> 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 <aeyerstaylor11 at gmail.com> 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
>>> ghc-devs at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> 



More information about the ghc-devs mailing list