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