[ghc-devs]: Explicit inequality evidence
anthony_clayden at clear.net.nz
Thu Dec 22 01:45:08 UTC 2016
> 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
More information about the Glasgow-haskell-users