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
).
- Look for local (non-quantified) assumptions for
[G] C T
. - Look for local quantified constraints whose conclusions match
C T
. If exactly one matches, select the constraint. Then, check whether any quantified constraints unify withC T
(allowing any variables inC T
to be bound). If any do, abort, complaining about potential incoherence. Otherwise, reduce[W] C T
to the premise of the quantified constraint. - 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 substitutionS
such thatS(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 localI
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:- If
I1 <=spec I2
andI2 <=spec I1
, thenI1 <= I2
islocality(I1) <= locality(I2)
. - If neither
I1 <=spec I2
norI2 <=spec I1
, thenI1 <= I2
islocality(I1) <= locality(I2)
. - Otherwise,
I1 <= I2
ifI1 <=spec I2
.
- If
Here is the proposed instance lookup procedure:
-
Collect all givens
I
(of all localities) that match a target. Call this setIs
. IfIs
is empty, fail. -
Let
I0
be the minimum element ofIs
with respect to<=
. (ConsiderIs
to be set-like, discarding duplicates.) IfI0
is not defined, fail. -
Let
Is'
be the setIs
excludingI0
. Case on the locality ofI0
:-
locality(I0) = 1
: Succeed withI0
(skipping last check, below). -
locality(I0) = 2
: Go on to next step ifIs'
contains only global instances. IfIs'
contains local instances, fail. -
locality(I0) = 3
: Fail if any element inIs'
is a local quantified instance. Go on to next step if, for everyI'
inIs'
, eitherI0
is overlapping orI'
is overlappable.
-
-
Collect all givens (of all localities) that unify with a target, excluding those in
Is
. IfIncoherentInstances
is off and this set contains at least one instances not labeled incoherent, fail. -
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.