[ghc-devs]: Explicit inequality evidence

Anthony Clayden anthony_clayden at clear.net.nz
Sun Dec 18 05:38:59 UTC 2016

[transferring to -users, because there's a much wider

> > 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: I’d prefer /~ and :/~:.
And yes, usually discussed with /~ as the type inequality
operator, since at least when ~ was introduced for type
> > ... 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'


More information about the Glasgow-haskell-users mailing list