[Haskell-cafe] Well-behaved instances, guards [was: [ghc-proposals/cafe] Partially applied type families]

[Anthony Clayden]

> On Tue May 16 01:26:00 UTC 2017, Anthony Clayden wrote:

(Might as well write it up, while it's fresh in my mind.)

>> On Mon May 15 16:20:09 UTC 2017, Richard Eisenberg wrote:

>> I do have to say all this talk has made me think more
>> about apartness constraints in FC, at least.
>> They might be a touch simpler than the current story.
>> 

> The trouble is that the semantics for overlap
> has never been spelled out.
> (Nor, I suspect the criterion for
>  a 'well-behaved' set of instances.
>  I can volunteer that for you.)

A set of instances is well-behaved wrt overlap
iff for each pairing of instances, one of:

1. The instances are apart. (No overlap.)
2. One of the instances is strictly more specific.
   (Total overlap.) IOW the two instances unify,
   producing a substitution; and that substitution
   is exactly the more specific instance.
3. Neither instance is more specific (Partial overlap.)
   IOW the two instances unify, producing a substitution;
   and that substitution is more specific than either.
And
3b. There is a third instance at exactly that substitution.
    So each instance becomes case 2 overlapping that third.

Example:

> class C a b
> instance C Int  b     -- (A)
> instance C Char b    -- (B) apart from (A), case 1
> instance C Int  Int  -- (C) more specific than (A), case 2

> instance C a    Bool   -- (D) partial overlap to (A), case
3
> instance C Int  Bool -- (E) intersect of (A), (D), case 3a
> instance C Char Bool -- (E') 'cos (D) also overlaps (B)

For a compiler to police case 3b is too hard:
* It needs search for a suitable intersecting instance,
  so can't be validated instance-by-instance.
* That intersect might be in a different module,
  so works against separate compilation.
* That intersect (if it's declared), might itself
  not be well-behaved.
* That intersect might not be needed.
  (Perhaps there's no call needing `C Int Bool`.)
  so it would be superfluous to declare it.
  (For this reason GHC doesn't look for such an instance
    until/unless it finds a use site.)
* For the intersect, perhaps the needed definition
  is the same as one of the other instances.
  Say, `C Int Bool` defined same as `C Int b`,
  but different to `C a Bool`.
  There's no way to express that: you must repeat the code.

These difficulties are somewhat relaxed for type families
(not class instances):
If the unifying substitution yields equal rhs's
for the two equations, the instances are accepted. Example

> type instance F Int b = b
> type instance F a Int = a 

Overlap at `F Int Int`. Under either equation the result is
`Int`, so this is accepted.

I suspect that even with a total overlap, case 2;
when GHC is trying to select the instance,
it's in a state of nervous cluelessness
as to the grounds/evidence for why to select an instance.
Particularly if it is to reject the more specific instance:
Is it sure some use site can never unify more specifically?
This must be particularly hard for repeated type vars
(non-linear patterns in the instance head).

> instance C Bool (a, a)   -- vs
> instance C Bool (a, b)


How do instance guards help? 
They eliminate the need to search for case 3a. 
A set of (possibly guarded) instances is well-behaved wrt
overlap 
iff for each pairing of instances, one of:

1. They are apart. (No overlap.)
4. They overlap, so unify producing a substitution;
And
4b. Under that substitution into the guards,
    the guards force the instances apart.

Note no need to consider any other instances. 
Furthermore we can validate looking purely at the instance
decls
 (including guards), we don't need to delay to possibly
ambiguous uses.

Re-work instances (A) to (E) above:

> instance C Int  b | b /~ Int -- (A) guard to de-overlap
(C)
> instance C Char b          -- (B) apart, no need for
guards
> instance C Int  Int         -- (C) most specific, no
guards
> instance C a    Bool | a /~ Int, -- (D) de-overlap (A)
>                                a /~ Char -- also
de-overlap (B)
> -- instance C Int Bool    -- (E) not needed, treat as (A)
> -- instance C Char Bool   -- (E') not needed, treat as (B)

Show how the guards for (D) force it apart from (A):
The instance heads unify to `C Int Bool`.
Substitute {a ~ Int, b ~ Bool} into the guards.
For (A) we get (Bool /~ Int) ==> True.
For (D) we get (Int /~ Int, Int /~ Char) ==> False.
So one guard (at least) is False. They're apart. 

The guards also drive the grounds/evidence 
for resolving overlapping heads. 
Suppose a use site wants `C Char Bool`.

There's two eligible heads: (B), (D).
Substitute wanted {a ~ Char, b ~ Bool} into the guards.
None for (B). For (D) (a /~ Int, a /~ Char) ==> False.
So select (B).

And to take the repeated type var example. Declare:

> instance C Bool (a, b) | a ~ b    -- (F)
> instance C Bool (a, b) | a /~ b   -- (G)

Suppose a use site wants ` C Bool (Int, b')`.
That is, b' is a unification variable,
not yet resolved.
Substitute {a ~ Int, b ~ b'} into the guards.
We have (F) (Int ~ b'); (G) (Int /~ b')
Neither True; neither False.
They do tell us we must improve b',
to resolve the selection.

Instance guards are to apply just as much for type
instances.
(So they can be distributed at associated types.) Example

> type instance F Int b = b
> type instance F a Bool | a /~ Int = a


Rules for guards:
a) The guards are a comma-sep list
    of equal (~) or apart (/~) comparisons.
b) The comparands must be same-kinded.
    (I'll leave the poly kinded case for Richard ;-)
c) Can only use type vars from the head.
    (I.e. not introduce extra vars, which contexts can do.)
d) No type functions -- too hard, and not injective.
e) Can use wildcard `_` as a type place-holder.
f) Can use Type constructors to arbitrary nesting.

As an example of d), the classic

> type instance IsaFunction ((->) a b) = True
> type instance IsaFunction c | c /~ ((->) _ _) = False

Note the False case must match plain `Int` 
and `Maybe c'` and `Either e c'`. 
So putting this is valid but wouldn't be general enough:

> type instance IsaFunction (c a b) | c /~ (->) = False


AntC