What does `~` (tilde) mean in an instance context, and why is it necessary to resolve overlap in some cases?

Question

A complication.

Consider the following snippet:

class                        D u a     where printD :: u -> a -> String
instance                     D a a     where printD _ _ = "Same type instance."
instance {-# overlapping #-} D u (f x) where printD _ _ = "Instance with a type constructor."

And this is how it works:

λ printD 1 'a'
...
...No instance for (D Integer Char)...
...

λ printD 1 1
"Same type instance."

λ printD [1] [1]
...
...Overlapping instances for D [Integer] [Integer]
...

λ printD [1] ['a']
"Instance with a type constructor."

Note that the overlapping instances are not resolved, despite the pragma being supplied to this end.

 

A solution.

It took some guesswork to arrive at the following adjusted definition:

class                        D' u a     where printD' :: u -> a -> String
instance (u ~ a) =>          D' u a     where printD' _ _ = "Same type instance."
instance {-# overlapping #-} D' u (f x) where printD' _ _ = "Instance with a type constructor."

It works as I expected the previous to:

λ printD' 1 'a'
...
...No instance for (Num Char)...
...

λ printD' 1 1
"Same type instance."

λ printD' [1] [1]
"Instance with a type constructor."

λ printD' [1] ['a']
"Instance with a type constructor."

 

My questions.

I am having a hard time understanding what is happening here. Is there an explanation?

Particularly, I can put forward two separate questions:

1. Why is the overlap not resolved in the first snippet?
2. Why is the overlap resolved in the second snippet?

But, if the issues are connected, perhaps a single, unified theory would serve explaining this case better.

 

P.S. concerning a close / duplicate vote   I am aware that ~ signifies type equality, and I am consciously using it to obtain the behaviour I need (particularly, printD' 1 'a' not matching). It hardly explains anything concerning specifically the case I presented, where the two ways of stating type equality (the ~ and the instance D a a) lead to two subtly distinct behaviours.

 

---

note   I tested the snippets above with ghc 8.4.3 and 8.6.0.20180810

Answer 1

First: only instance head matters during instance selection: what's on the left of => does not matter. So, instance D a a prevents selection unless they are equal; instance ... => D u a can always be selected.

Now, the overlap pragmas only come into play if one instance is already more "specific" than the other. "Specific", in this case, means "if there exists a substitution of type variables that can instantiate an instance head A to instance head B, then B is more specific than A". In

instance D a a
instance {-# OVERLAPPING #-} D u (f x)

neither is more specific than the other, as there is no substitution a := ? that makes D a a into D u (f x), nor is there any substitution u := ?; f := ?; x := x that makes D u (f x) into D a a. The {-# OVERLAPPING #-} pragma does nothing (at least, pertaining to the problem). So, when resolving the constraint D [Integer] [Integer], the compiler finds both instances to be candidates, neither more specific than the other, and gives an error.

In

instance (u ~ a) => D u a
instance {-# OVERLAPPING #-} D u (f x)

the second instance is more specific than the first one, because the first one can be instantiated with u := u; a := f x to get to the second one. The pragma now pulls its weight. When resolving D [Integer] [Integer], both instances match, the first one with u := [Integer]; a := [Integer], and the second with u := [Integer]; f := []; x := Integer. However, the second is both more specific and OVERLAPPING, so the first one is discarded as a candidate and the second instance is used. (Side note: I think the first instance should be OVERLAPPABLE, and the second instance should have no pragma. This way, all future instances implicitly overlap the catch-all instance, instead of having to annotate each one.)

With that trick, selection is done with the right priority, and then equality between the two arguments is forced anyway. This combination achieves what you want, apparently.

One way to visualize what is happening is a Venn diagram. From the first attempt, instance D a a and instance D u (f x) form two sets, the sets of the pairs of types that each one can match. These sets do overlap, but there are many pairs of types only D a a matches, and many pairs only D u (f x) matches. Neither can be said to be more specific, so the OVERLAPPING pragma fails. In the second attempt, D u a actually covers the entire universe of pairs of types, and D u (f x) is a subset (read: inside) of it. Now, the OVERLAPPING pragma works. Thinking in this way also shows us another way to make this work, by creating a new set that covers exactly the intersection of the first try.

instance D a a
instance D u (f x)
instance {-# OVERLAPPING #-} (f x) (f x)

But I'd go with the one with two instances unless you really need to use this one for some reason.

Note, however, that overlapping instances are considered a bit fragile. As you noticed, it is often tricky to understand which instance is picked and why. One needs to consider all the instances in scope, their priorities, and essentially run a nontrivial selection algorithm in one's mind to understand what's going on. When the instances are defined across multiple modules (including orphans) things become even more complex, because selection rules might differ according to the local imports. This can even lead to incoherence. It is best to avoid them when possible.

See also the GHC manual.