[Haskell-cafe] [ghc-proposals/cafe] Partially applied type families

Anthony Clayden anthony_clayden at clear.net.nz
Wed May 24 10:47:21 UTC 2017

> On Wed May 24 07:57:09 UTC 2017, Alejandro Serrano Mena

> I know I am just jumping in the middle of an already long
> discussion.

Hi Alejandro, your input is very welcome.
I know there have been many posts,
so Richard's right the idea now needs writing up
in detail in one place.

> >
> > Bottom line: You win. I'm convinced. Apartness guards
> >
> > Even better, I think apartness guards would be very easy
> > to implement. All the plumbing is already installed: we
> > basically just have to add a switch. 
> >

> I would like to advise against this idea of apartness
> guards. I've tried myself some years ago, and I remember
> them being quite complicated to describe. ...

That's interesting. What did you try?
How did you test for apartness?

I roughed out the rules a few posts back.
Bottom of
The body of that post has worked examples.

I can also translate guards into Haskell2010 + MPTCs,
providing there's a primitive for type-level type
(Which we could write today with Closed Type Families.)
discussion of (?~). This is essentially the 'case-preparing'
technique from HList [2004].

> The main problem is that apartness may end up
> introducing some sort of backtracking
> in the type checking process -- something
> completely undesirable.

I agree that's not just undesirable, but unacceptable. 
(Backtracking is a weakness of Instance chains IMO.)

With the guards I'm thinking of, an instance either applies
at a usage site or does not (after taking guards into
Or type refinement hasn't advanced enough to decide.
Then that instance remains 'in play'.
This is exactly the same process as currently.

If an instance does apply (with guards)
then it is guaranteed to be the only instance.
IOW all other instances are excluded. So:

> Furthermore, they make the work of
> the overlapping checks much harder.

The guards remove any need for overlapping checks.
Instead the compiler must unify the usage site
with the instance head, then substitute into the guards.
If a guard comes out false under that subst, reject the
If all guards come out true, select the instance.
If some guards come out 'not proven',
it needs more type refinement.

So you can't have OverlappingInstances
as well as InstanceGuards.
(Or at least not for the same class/type family.
 That's a bit of backwards compatibility awkwardness
 I mentioned.)


More information about the Haskell-Cafe mailing list