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

[Paul Brauner]

On Mon, Apr 8, 2013 at 9:59 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:

>
>
> 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.)


Ok.


> 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.
>
>
Great!

Paul


>  Richard
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130408/ebd68eec/attachment.htm>