Improving the Types Example

[DavePearce]

The benchmark examples/types/ has quite a number of limitation which it would be nice to address. For example, it won't simplify (int,int)|(any,int). Similarly, it won't simplify (int,int)&(int,(int,int)) either.

The reason for this is that it needs to handle protons properly. However, handling protons in the presence of recursive types is not straightforward. For example, these types cause a problem \X.(int|X,int) or \X.(int|(X,int),int), etc.

Essentially, in the presence of recursive types, it becomes unclear what exactly the normal form is. In the original paper, we pull unions out all the way to the "top". But, in a recursive type system, there is no "top" per se.