8 Apr
2013
8 Apr
'13
3:12 p.m.
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