On Apr 8, 2013, at 3:12 PM, Paul Brauner <polux2...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
