Consider using specificity to disambiguate quantified constraints

Summary: Currently, quantified constraints shadow global instances. This ticket proposes to use specificity (in the sense used by overlapping instances) instead of shadowing.

Motivation

This looks like a sensible way of having a datatype that can store something of a type that supports some class interface:

data Some (c :: Type -> Constraint) where
  Some :: c a => a -> Some c

But now I want to write a Show instance. I can do this only when the existential a supports Show. But I don't wish to require that c ~ Show -- maybe c a implies Show a. So I write this:

instance (forall x . c x => Show x) => Show (Some c) where
  showsPrec n (Some a) = showsPrec n a

But now this fails. The problem is that the instance gets expanded to

instance (forall x . c x => Show x) => Show (Some c) where
  showsPrec n (Some a) = showsPrec n a
  show = $dmshow

where $dmshow :: Show a => a -> String is the default method implementation for show. When type-checking this method, GHC needs to satisfy Show (Some c). The context includes two possibilities: the quantified constraint, and the top-level instance declaration. Because local instances (= quantified constraints) shadow global ones, we use the first. So we reduce [W] Show (Some c) to [W] c (Some c), which cannot be solved, leading to disaster.

This example first came to light in #16502 (comment 253501), where it was copied from #17794 (closed).

Taking this new approach will likely fix #16502 and allow the original program in #17202 (closed) to be accepted. See also #16502 (comment 253501) and #16502 (comment 259055) for more test cases.

Background:

The current instance lookup (as documented here) works as follows to solve a [W] C T constraint (for some class C and type T).

1. Look for local (non-quantified) assumptions for [G] C T.
2. Look for local quantified constraints whose conclusions match C T. If exactly one matches, select the constraint. Then, check whether any quantified constraints unify with C T (allowing any variables in C T to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce [W] C T to the premise of the quantified constraint.
3. Same as (2), but using the global instance table.

Proposal:

Use specificity to disambiguate.

• Let <=spec denote a partial order on instance heads. C T1 <=spec C T2 iff there exists a substitution S such that S(T2) = T1 -- just as is used with overlapping instances today.

• Let metavariable I denote givens. These can be non-quantified, quantified (local), or global.

• Define locality(I) be a number that denotes how local I is. The locality of a non-quantified given is 1, of a quantified local given is 2, and of a global is 3.

• Define partial order <= on instances as follows:

  1. If I1 <=spec I2 and I2 <=spec I1, then I1 <= I2 is locality(I1) <= locality(I2).
  2. If neither I1 <=spec I2 nor I2 <=spec I1, then I1 <= I2 is locality(I1) <= locality(I2).
  3. Otherwise, I1 <= I2 if I1 <=spec I2.

Here is the proposed instance lookup procedure:

1. Collect all givens I (of all localities) that match a target. Call this set Is. If Is is empty, fail.

2. Let I0 be the minimum element of Is with respect to <=. (Consider Is to be set-like, discarding duplicates.) If I0 is not defined, fail.

3. Let Is' be the set Is excluding I0. Case on the locality of I0:

   • locality(I0) = 1: Succeed with I0 (skipping last check, below).
   • locality(I0) = 2: Go on to next step if Is' contains only global instances. If Is' contains local instances, fail.
   • locality(I0) = 3: Fail if any element in Is' is a local quantified instance. Go on to next step if, for every I' in Is', either I0 is overlapping or I' is overlappable.

4. Collect all givens (of all localities) that unify with a target, excluding those in Is. If IncoherentInstances is off and this set contains at least one instances not labeled incoherent, fail.

5. Succeed with I0.

Discussion:

This new algorithm is meant to replicate current behavior, except in the scenario where a global instance is more specific than a local one, in which the global instance should be selected. I have tried to capture current behavior w.r.t. incoherent and overlapping instances. In any case, if my algorithm deviates from current behavior w.r.t. incoherent or overlapping instances, this deviation is unintentional.

Another possible approach is to put local and global instances on even footing (that is, set both to have locality 2) but to allow users to explicitly label local instances as overlapping. I prefer the tiered approach above, but there's something simpler about local overlapping instances, in that it's one mechanism to think about.