[transferring to -users, because there's a much wider discussion]
On Dec 13, 2016, at 15:04, Richard Eisenberg wrote: I've thought about inequality on and off for years now,
The subject has appeared (in various guises) on Haskell forums since well before 2002 [1] -- which went into the 'OutsideIn(X)' model. Search the cafe on 'type disequality', for example.
On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus wrote: First the bike shedding: Id prefer /~ and :/~:.
And yes, usually discussed with /~ as the type inequality operator, since at least when ~ was introduced for type equality.
... but it's a hard nut to crack.
Which is presumably why spj has never shown any interest.
... need evidence of inequality in Core, and a brand-spanking-new type safety proof. ...
One rule of inference that David/Oleg haven't mentioned: If x /~ y and y ~ z then x /~ z. How does this go with (potentially) infinite type (family)s? Thanks Richard for the refs on type safety proofs. I wonder if anything in type safety relies on inequalities? (This would be with, say, overlaps + fundeps extensions.) FunDep 'confluence' (which Richard has re-christened 'coincident overlap' for closed type families), surely relies on proving at some use site that the types can never unify with such-and-such instance (or type family equation). For example if we have instance C a a where ... instance C a b where... We have to prove at a use site that the two types cannot unify, to justify picking the second instance. This goes badly with separate compilation: suppose the `C a a` instance is not visible in every module. I would love type inequality guards on instances to be explored as an alternative approach for overlap. (See some of my reponses to Richard [2].) In my example above: instance C a b | a /~ b where ... So the invisibility of the `C a a` instance would not upset any use sites. [1] Sulzmann and Stuckey 2002 'A theory of Overloading' [2] https://typesandkinds.wordpress.com/2013/04/29/coincident-overlap-in-type-fa... AntC