TypeLits and type families wrt. equality

[Richard Eisenberg]

On Jul 27, 2015, at 10:56 AM, Gabor Greif <ggreif at gmail.com> wrote:
>>> 
>>> decideRefl :: Proxy (a :: Symbol) -> Proxy b
>>>              -> Proxy (Equal a b :~: 'False)
>>>              -> Either (Equal a b :~: 'False) (a :~: b)

What's the point of the third Proxy argument? I don't think it adds anything. Perhaps without that the way forward (albeit still with unsafeCoerce) will become clear.

Richard