Re: TypeLits and type families wrt. equality

27 Jul 2015

      On 7/27/15, Richard Eisenberg  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  wrote:
...
On 7/27/15, Richard Eisenberg  wrote:
...
On Jul 27, 2015, at 10:56 AM, Gabor Greif  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>
               :~: )
 -> Either (<some type-level expression mentioning a and b>
               :~: )
       (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