TypeLits and type families wrt. equality

[Richard Eisenberg]

It sounds like you want this, then:

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

It still uses unsafeCoerce, of course. There isn't really any advantage to baking the use of unsafeCoerce into GHC, as the GHC core would still use unsafeCoerce here. So, I think that -- barring the Big Deal of inventing proper inequality witnesses -- you're a little tied to unsafeCoerce.

Richard

On Jul 27, 2015, at 12:04 PM, Gabor Greif <ggreif at gmail.com> wrote:

> On 7/27/15, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>> 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)
>>> 
>> 
> 
> This is basically what I am doing now. Namely using unsafeCoerce.
> 
> But this is not what I am after. Namely a safe way to exploit negative
> evidence coming from sameSymbol. I want a (weak form of) decidable
> type-level equality, where I either get a witness that a and b are equal
> (just like sameSymbol works now) or alternatively a different witness
> that a type function evaluates to some type under the assumption that
> a is not b. This is the interesting part, as the type family could get stuck
> without this knowledge as my original example illustrates (and also Simon's).
> 
> The goal is not only to obtain *some* witness, but to never obtain a bad
> witness this way (i.e. never get something like 'True :~: 'False).
> 
> Cheers,
> 
>    Gabor
> 
> 
>> 
>> 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
>> 
>>