More External Core questions

[Simon Peyton-Jones]

| 1) What's the right way to encode the coercion manipulation functions
| such as left, right, and sym as IfaceTypes?

They are just Types, so they'll convert straightforwardly to IfaceTypes.  That must be happening *already* because coercions appear in interface files.

| 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'.

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?

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.

Simon