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.)
On Apr 8, 2013, at 3:12 PM, Paul Brauner <polux2001@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?
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