[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 
-- 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
> > ... 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 .)
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.
> On Dec 13, 2016, at 1:02 AM, David Feuer <david.feuer at
>> On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus
<oleg.grenrus at iki.fi> wrote:
>> I assume that in your rules, variables are not type
>> x /~ y => f x /~ f y doesn't hold if `f` isn't injective.
(e.g. type family F x where F x = ())
>> other direction is true though.
> I was definitely imagining them as first-class types; your
> f x /~ f y => x /~ y even if f is a type family is an
Hmm, yes except: how would evidence ever arise that f x /~ f
Would we ever get a 'wanted' constraint to that effect?
More likely, we'd be trying to discriminate between
in which picking some instance depends on f x /~ f y.
I don't see that any of the overlap/closed type family work
has got us away from the 'groundedness issues'
observed in the HList paper.
We have to improve both types to a grounded type constructor
to get the evidence they're not equal.
(Or at least that parameters in the same position are not
and that the type constructors are not familys and are the