Re: TypeLits and type families wrt. equality

This works for me (with ScopedTypeVariables):

gabor :: forall a b lhs rhs. (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Proxy (lhs :~: rhs) -> Either (lhs :~: rhs) (a :~: b) gabor a b _ = case sameSymbol a b of Just refl -> Right refl Nothing -> Left (unsafeCoerce Refl)

Does this do what you want? Richard On Jul 27, 2015, at 11:22 AM, Gabor Greif wrote:

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