[ghc-devs]: Explicit inequality evidence

[Anthony Clayden]

> On Dec 13, 2016, at 1:02 AM, David Feuer <david.feuer at
gmail.com> wrote:
> 
>> 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
families, otherwise
>> 
>> 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
point that
> f x /~ f y => x /~ y even if f is a type family is an
excellent one.
>

Hmm, yes except: how would evidence ever arise that f x /~ f
y ?

Would we ever get a 'wanted' constraint to that effect?

More likely, we'd be trying to discriminate between
instances
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
equal,
 and that the type constructors are not familys and are the
same arity.)


AntC