8 Apr 21:12 2013

## %==%, :==: and type equality in the singletons library

Paul Brauner <polux2001 <at> gmail.com>

2013-04-08 19:12:32 GMT

2013-04-08 19:12:32 GMT

Hello,

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?

Given

data T = C1 | ... | Cn

I can easily derive

data EqT :: T -> T -> * where

EqT :: a ~ b => EqT a b

eqT :: ST a -> ST b -> Maybe (EqT a b)

eqT SC1 SC1 = Just EqT

...

eqT SCn SCn = Just EqT

eqT _ _ = Nothing

but this kind of replicates the boilerplate generated by the singletons library for %==%. However I can't see how to leverage %==% to inhabit eqT since I can't deduce a ~ b from a %==% b == STrue.

Any idea? If there's no way to write eqT using what singletons generates, wouldn't it make sense for it to generate something that relates :==: and ~ ?

Cheers,

Paul

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe <at> haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe