# TypeLits and type families wrt. equality

Richard Eisenberg eir at cis.upenn.edu
Mon Jul 27 16:53:08 UTC 2015

```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
>>
>>

```