[Haskell-cafe] %==%, :==: and type equality in the singletons library
polux2001 at gmail.com
Mon Apr 8 21:12:32 CEST 2013
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?
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 ~
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe