Explicit inequality evidence

[David Feuer]

According to Ben Gamari's wiki page[1], the new Typeable is expected to
offer

eqTypeRep :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a
:~: b)

Ideally, we'd prefer to get either evidence of equality or evidence of
inequality. The traditional approach is to use Dec (a :~: b), where data
Dec a = Yes a | No (a -> Void). But  a :~: b -> Void isn't strong enough
for all purposes. In particular, if we want to use inequality to drive type
family reduction, we could be in trouble.

I'm wondering if we could expose inequality much as we expose equality.
Under an a # b constraint, GHC would recognize a and b as unequal. Some
rules:

Base rules
1. f x # a -> b
2. If C is a constructor, then C # f x and C # a -> b
3. If C and D are distinct constructors, then C # D

Propagation rules
1. x # y <=> (x -> z) # (y -> z) <=> (z -> x) # (z -> y)
2. x # y <=> (x z) # (y z) <=> (z x) # (z y)
3. If x # y then y # x

Irreflexivity
1. x # x is unsatisfiable (this rule would be used for checking patterns).

With this hypothetical machinery in place, we could get something like

data a :#: b where
  Unequal :: a # b => Unequal (a :#: b)

eqTypeRep' :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Either
(a :#: b) (a :~: b)

Pattern matching on an Unequal constructor would reveal the inequality,
allowing closed type families relying on it to reduce.

Evidence structure:

Whereas (:~:) has just one value, Refl, it would be possible to imagine
richer evidence of inequality. If two types are unequal, then they must be
unequal in some particular fashion. I conjecture that we don't actually
gain much value by using rich evidence here. If the types are Typeable,
then we can explore them ourselves, using eqTypeRep' recursively to locate
one or more differences. If they're not, I don't think we can track the
source(s) of inequality in a coherent fashion. The information we got would
only be suitable for use in an error message. So one option would be to
bundle up some strings describing the known mismatch, and warn the user
very sternly that they shouldn't try to do anything too terribly fancy with
them.

[1] https://ghc.haskell.org/trac/ghc/wiki/Typeable/BenGamari
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20161212/26a99ebb/attachment.html>