Let's rework Data.Type.Equality.==

[David Feuer]

On Fri, Aug 11, 2017 at 11:39 AM, Richard Eisenberg <rae at cs.brynmawr.edu> wrote:
> If (==) is to be useful
> in a type system, we would need such a guarantee. (By "useful", I mean that
> this is implementable:
>
>   reifyEq :: forall a b. ((a == b) ~ True, Typeable a, Typeable b)
>           => a :~: b
[The above is edited slightly]

Let's get back to this for a moment. I tried actually implementing
this for the simple polykinded version you suggested on my
differential:

    infix 4 ==
    type family (a :: k) == (b :: k) :: Bool where
      f a == g b = f == g && a == b
      a == a = 'True
      _ == _ = 'False

Sadly, it doesn't seem to be possible to really do it properly. First,
there's no way
to prove (f == g) ~ 'True or (x == y) ~ 'True from just (f x == g y) ~
'True. The latter
reduces to (f == g && x == y) ~ 'True, but (&&) is not a constructive
"and", so we can't
actually extract any information from it. Thus we can't work from top to bottom.

Second, pattern matching on TypeReps can only expose
equality and not inequality (as we have no first-class notion of
inequality). So if we
try to work from bottom to top,

    foo :: TypeRep a -> TypeRep b -> Either ((a == b) :~: 'False) ((a
== b) :~: 'True)

we will get well and thoroughly stuck on the non-recursive cases.

So the only way I see to implement reifyEq is

    reifyEq = case eqTypeRep (typeRep :: TypeRep a) (typeRep :: TypeRep b) of
                Just HRefl -> Refl
                Nothing -> error "unreachable"

That doesn't really seem terribly satisfying.