TypeLits and type families wrt. equality
eir at cis.upenn.edu
Mon Jul 27 14:44:41 UTC 2015
On Jul 27, 2015, at 10:36 AM, Gabor Greif <ggreif at gmail.com> wrote:
> When saying "Big Deal" did you mean
> - highly desirable and somebody should go for it
> - or a terrible amount of work, and who tackles it is probably a
> fool on a hubris trip?
> (I still have my problems deciphering British irony.)
My use of Big Deal here is more your second option, but without so much negativity. :) I'm sure the person who tackled this problem would learn a ton and contribute to programming language research. It's just that we haven't yet found a great motivation for doing so.
> I guess a full-blown solution is too much work for now (also considering
> previous comments from Richard). But what about a simpler construct
> decideRefl :: Proxy (a :: Symbol) -> Proxy b
> -> Proxy (Equal a b :~: 'False)
> -> Either (Equal a b :~: 'False) (a :~: b)
I believe that this function could be written only with the help of unsafeCoerce. Indeed, the `singletons` package provides an `SDecide` instance for the type-lits (which accomplishes a similar, though not identical, goal) via unsafeCoerce.
More information about the ghc-devs