Re: TypeLits and type families wrt. equality

On 7/27/15, Richard Eisenberg wrote:

On Jul 27, 2015, at 10:56 AM, Gabor Greif 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.

Proxy (Equal a b :~: 'False) is just the specialised version to the general issue I'd like to crack: Proxy a -> Proxy b -> Proxy (<some type-level expression mentioning a and b> :~: ) -> Either (<some type-level expression mentioning a and b> :~: ) (a :~: b) Somehow one has to communicate the equation to the compiler that should be proved under the assumption that a is not unifiable with b. Is this clearer? Sorry for the sloppy definition! Cheers, Gabor

Richard