<div dir="ltr"><div dir="auto">According to Ben Gamari's wiki page[1], the new Typeable is expected to offer<div dir="auto"><br></div><div dir="auto">eqTypeRep :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Maybe (a :~: b)<br></div><div dir="auto"><br></div><div dir="auto">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.<br></div><div dir="auto"><br></div><div dir="auto">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:</div><div dir="auto"><br></div><div dir="auto">Base rules</div><div>1. f x # a -> b<br></div><div>2. If C is a constructor, then C # f x and C # a -> b<br></div><div>3. If C and D are distinct constructors, then C # D<br></div><br></div><div>Propagation rules<br></div><div dir="auto"><div dir="auto">1. x # y <=> (x -> z) # (y -> z) <=> (z -> x) # (z -> y)</div><div dir="auto">2. x # y <=> (x z) # (y z) <=> (z x) # (z y)</div><div dir="auto">3. If x # y then y # x<br><br></div><div>Irreflexivity<br></div><div>1. x # x is unsatisfiable (this rule would be used for checking patterns).<br></div><div dir="auto"><br></div><div dir="auto">With this hypothetical machinery in place, we could get something like<br></div><div dir="auto"><br></div><div>data a :#: b where<br></div><div>  Unequal :: a # b => Unequal (a :#: b)<br><br></div><div dir="auto"><span style="font-family:sans-serif">eqTypeRep' :: forall k (a :: k) (b :: k). TypeRep a -> TypeRep b -> Either (a :#: b) (a :~: b)<br><br></span></div><div><span style="font-family:sans-serif">Pattern matching on an Unequal constructor would reveal the inequality, allowing closed type families relying on it to reduce.<br><br></span></div><div><span style="font-family:sans-serif">Evidence structure:<br><br></span></div><div dir="auto"><span style="font-family:sans-serif">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.<br><br>[1] <a href="https://ghc.haskell.org/trac/ghc/wiki/Typeable/BenGamari">https://ghc.haskell.org/trac/ghc/wiki/Typeable/BenGamari</a><br></span></div></div>
</div>