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