Thanks, this makes sense and helps.   Is this described in the wobbly types paper, or is paper covering a different topics?  I would like to have a cite-able reference.

Excellent question.   I believe that what I describe below is a restriction of the system described in the POPL'06 paper

                http://research.microsoft.com/%7Esimonpj/papers/gadt/gadt-icfp.pdf

 

At this moment I can't remember when we changed to the additional restrictions below.  I think the reason was that we wanted to avoid the complexity of "fresh" mgus described in the paper, but memory is failing me.  Dimitrios or Stephanie may have a better memory.