[ghc-devs]: Explicit inequality evidence

[Anthony Clayden]

[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: I’d 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-families/

 
AntC