TypeLits and type families wrt. equality

[Richard Eisenberg]

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 <ggreif at gmail.com> wrote:

> On 7/27/15, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> 
>> 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.
> 
> 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>
>                :~: <some desired result assuming a /= b holds>)
>  -> Either (<some type-level expression mentioning a and b>
>                :~: <some desired result assuming a /= b holds>)
>        (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