Proxy, new Typeable, and type-level equality

[Erik Hesselink]

On Wed, Apr 3, 2013 at 6:08 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:
> Comments? Thoughts?

Edward Kmett 'eq' library uses a different definition of equality, but
can also be an inspiration for useful functions. Particularly, it
includes:

lower :: (f a :~: f b) -> a :~: b

Another question is where all this is going to live? In a separate
library? Or in base? And should it really be in a GHC namespace? The
functionality is not bound to GHC. Perhaps something in data would be
more appropriate.

Erik