TypeLits and type families wrt. equality

[Gabor Greif]

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