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