TypeLits and type families wrt. equality

[Gabor Greif]

On 7/27/15, Richard Eisenberg <eir at cis.upenn.edu> wrote:
>
> On Jul 27, 2015, at 10:36 AM, Gabor Greif <ggreif at gmail.com> wrote:
>
>> When saying "Big Deal" did you mean
>>  - highly desirable and somebody should go for it
>>  - or a terrible amount of work, and who tackles it is probably a
>> fool on a hubris trip?
>>
>> (I still have my problems deciphering British irony.)
>
> My use of Big Deal here is more your second option, but without so much
> negativity. :) I'm sure the person who tackled this problem would learn a
> ton and contribute to programming language research. It's just that we
> haven't yet found a great motivation for doing so.
>

Okay, agreed.

>>
>> I guess a full-blown solution is too much work for now (also considering
>> previous comments from Richard). But what about a simpler construct
>>
>> decideRefl :: Proxy (a :: Symbol) -> Proxy b
>>               -> Proxy (Equal a b :~: 'False)
>>               -> Either (Equal a b :~: 'False) (a :~: b)
>
> I believe that this function could be written only with the help of
> unsafeCoerce. Indeed, the `singletons` package provides an `SDecide`
> instance for the type-lits (which accomplishes a similar, though not
> identical, goal) via unsafeCoerce.

I doubt it could even be written with unsafeCoerce. It would need some
magic sauce from the compiler,
tapping into the type family normalizer. Consider:

> decideRefl (Proxy :: Proxy "a") (Proxy :: Proxy "b") (Proxy :: Proxy (Equal a b :~: 'True)

This should give a type error (we shouldn't fabricate false evidence!), while

> decideRefl (Proxy :: Proxy "a") (Proxy :: Proxy "b") (Proxy :: Proxy (Equal a b :~: 'False)

should pass the type checker and give Left Refl.

Cheers,

    Gabor

>
> Richard
>
>