[Haskell-cafe] %==%, :==: and type equality in the singletons library

[Richard Eisenberg]

On Apr 8, 2013, at 3:12 PM, Paul Brauner <polux2001 at gmail.com> wrote:

> from the output of -ddump-splices I dont think it is the case but I'm asking anyway: is there any way to deduce a ~ b from a :==: b? 

Not easily. You would have to write a (potentially recursive) function that explicitly matches singleton constructors, similarly to what you wrote. (You could say that this function is a (potentially inductive) proof that the generated definition of :==: is correct.) I agree that this is boilerplate and could easily be generated. I've added it to the list of features to be included in the next version of singletons. I'm surprised myself that it hasn't occurred to me to include this before.

Richard