[developers] LKB vs. PET divergences

[John Carroll]

> Alternatively, we have a discrepancy in the glb calculation algorithm, 
> which
> would also be possible, though horrible to fix.  If there's a formal
> definition of glbtype introduction which says whether it is or is not 
> supposed
> to introduce pure types in this situation, then we can decide which 
> behaviour
> is correct.

I also don't have PET available to check, but if the two systems start 
with the same type hierarchy and then introduce glbs I'd be surprised 
if they came out with substantively different results. There's just not 
much freedom to do things differently, or incorrectly.

John