On Dec 13, 2016, at 1:02 AM, David Feuer wrote:

...

On Tue, Dec 13, 2016 at 12:49 AM, Oleg Grenrus 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