On Tue May 30 19:43:30 UTC 2017, Richard Eisenberg wrote:

...

On May 24, 2017, at 3:13 AM, Anthony Clayden wrote:

... Some functions are defined by an ordered set of equations. Some (that is, class methods) are defined by an unordered set of equations, perhaps distributed across modules. Both models are useful.

Sure. Let a 100 schools of thought contend.

...

...

... [equality constraints and equality guards are] different, but I think the equality guard is useless

I agree adds nothing over repeating the typevar. And I've already agreed the potential for confusion with (~) constraints. So noted. I'll include it in the proposal, where a wider audience can bikeshed.

...

I see two main uses/benefits: 1. avoids the need for non-linear patterns in the head

Agreed that it would do this. But why is that important?

I was in part thinking of your wondering-out-loud earlier in the Partially applied thread https://mail.haskell.org/pipermail/haskell-cafe/2017-May/127078.html If we want to part-apply a type Fun which has a non-linear lhs, how does that go with your case-equation style? Adapting that earlier example:

type family F a b where F a a = () -- added an equation F Int b = b F a Bool = a

would really mean

type F a b = case a of _ -> case b of -- ?? _ match-all a -> () -- ?? re-using typevar a Int -> b _ -> case b of Bool -> a _ -> F a b

...

2. visually points up the 'non-apartness' vs an, um. "apartness guard"

(When I was figuring out Andy A-M's 2013 example, I rewrote the non-linear patterns with ~ guards, so I could figure out the apartness guards esp for the semi-apart instances. I posted the later workings to your blog

Somehow, this is more convincing. But I'm still not convinced on this point. Happily, you don't need to convince me -- put in the proposal what you like and then we can debate a concrete design.

...

...

[except as a type-level "let", I suppose].)

They would work as "let", I think:

...

instance Either a a | a ~ SomethingBigAndUgly where ...

Note that the `a` is not introduced in the guard.

Ah, OK. I get you. Equally that could be

instance Either a b | a ~ b, a ~ SomethingBigAndUgly where ..

...

Ok thanks, yes [TypeError] helps. Nevertheless it seems disergonomic to write an instance for a type-equal case, even with a helpful error message; when what you want is: no such instance.

You could always view

...

instance TypeError ... => C Int Bool

as sugar for

...

instance C Int Bool fails

Yes I understand that. But no I don't want any instance. (Sugar on rotten fruit doesn't hide the smell.) There are (or at least used to be) all sorts of side-effects from there in effect being an instance that matched.

...

What I can see will be awkward is backwards compatibility: can a class/type family with guards coexist with CTFs and with classes using overlap?

Sure. There would be no problem with this. The new idea is just that: new. I don't see it as getting rid of anything we already have. Perhaps some day we could think about removing OverlappingInstances, but we certainly don't have to do that at the same time as introducing instance guards. (I do like that name, too.)

OK. Perhaps you're seeing something I can't. To adapt your example from a parallel message, suppose:

module A

class {-# INSTANCEGUARDS #-} C a where ... instance C (Maybe a) | a /~ Int where ... instance C (Maybe Int) where ...

module B -- knows nothing of InstanceGuards import A

instance {-# OVERLAPPABLE #-} C (Maybe Bool) where ...

I want to reject that `(Maybe Bool)` instance. Even though it would legitimately be OVERLAPPABLE by (Maybe a) (that is, without the `a /~ Int` guard). Furthermore I might want a class to be InstanceGuarded, even though the instances I declare don't themselves need guards. (That is, I'm wanting to avoid 'future' overlaps in modules that import the class.)

...

I'll have a crack at the proposal.

Great. Thanks!

(Likely I'll need some help with the protocols.) AntC