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

[Anthony Clayden]

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

> 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
https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127103.html
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
comparison.
(Which we could write today with Closed Type Families.)
See
https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127090.html
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
account).
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
instance.
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.)


AntC