More External Core questions

[Aaron Tomb]

On Jul 2, 2007, at 2:28 AM, Simon Peyton-Jones wrote:
> =| 2)  I have the following source file:
> |
> |    %module main:GADTTest
> |      %data main:GADTTest.Term x =
> |        {K :: %forall x a (cozuwild::(x:=:a -> a)) .
> | main:GADTTest.Term x};
> |
> | which is translated into (roughly):
> |    IfaceData {
> |      ifName = main:GADTTest.Term;
> |      ifTyVars = [x, a];
> |      ifCtxt = [];
> |      ifCons = IfDataTyCon [IfCon {
> |                              ifConOcc = K;
> |                              ifConUnivTvs = [x, a];
> |                              ifConExTvs = [cozuwild::(x:=:a -> a)];
> |                              ifConEqSpec = [];
> |                              ifConCtxt = [];
> |                              ifConArgTys = [];
> |                              ...
> |                            }];
>
> That doesn't look right. The UnivTvs of the data type are just 'x'  
> in this case, not 'x' and 'a'.

You're right, and actually the code does get this bit correct. I  
wrote the above translation by hand, so it was my mistake.

> Your goal is to make sure that printing an IfaceConDecl and then  
> reading it in again is the identity function.  Presumably that's  
> not happening here.  You should just use "Show" and then "Read",  
> more or less.  But perhaps you are trying to make a more user- 
> friendly concrete syntax?  Is that what you are trying to do?

The people who originally implemented External Core defined a  
concrete syntax which is pretty close to Read/Show, but not entirely  
so. I'm basically just adding to that syntax when necessary, and  
trying not to change it too much. The old syntax doesn't include all  
of the information present in the internal Iface data constructors.

Things would actually be significantly easier if I dropped backward  
compatibility and essentially just did a Read/Show approach. Since  
very few people seem to have used the old format, compatibility  
probably isn't a big issue. The main reason I'd been avoiding the  
Read/Show approach is that it would make the External Core format  
change whenever the .hi format changes, which seems to happen fairly  
often. I'm not sure that it's really feasible to have a format that  
doesn't have that problem to at least some extent, though.

What do you think? Is a somewhat volatile format ok? If it is, things  
might go much more quickly.

> At the moment, all the equality-coercion info is indeed held in the  
> EqSpec.  If you don't obey that invariant, then indeed odd things  
> may happen.

Ok, that's good to know. I should be straightforward to make that  
happen.

Thanks,
Aaron