Class instance specificity order (was Re: Fundeps and type equality)

[Tyson Whitehead]

On January 11, 2013 13:55:58 Simon Peyton-Jones wrote:
> |  The -XOverlappingInstances flag instructs GHC to allow more than one
> |  instance to match, provided there is a most specific one. For example,
> |  the constraint C Int [Int] matches instances (A), (C) and (D), but the
> |  last is more specific, and hence is chosen. If there is no most-specific
> |  match, the program is rejected."
> |  
> |  What it doesn't says is how "most-specific match" is computed.
> 
> An instance declaration (A) is "more specific" than another (B) iff the
> head of (A) is a substitution instance of (B). For example
> 
> (A)	instance context1 => C [Maybe a]
> (B)	instance context2 => C [b]
> 
> Here (A) is more specific than (B) because we can get (A) from (B) by
> substituting b:=Maybe a.
> 
> Does that make it clear?  If so I will add it to the manual.

Thanks Simon.  That is exactly what I was looking for.  It is clear now.

> |  not cases are so clear.  For example, which of
> |  
> |  instance context1 => C Int b
> |  instance context2 => C a   [[b]]
> |  
> |  does C Int [[Int]] match best against?
> 
> Neither is instance is more specific than the other, so C Int [[Int]] is
> rejected.

This was what I was wondering.

> |  If there isn't currently a good
> |  way to resolve this, I would like to suggest the type-shape measure I
> |  proposed in that paper I wrote up awhile back could be used.
> 
> I think the current design is reasonable, and I don't want to complicate it
> unless there is a very compelling reason to do so.

Applying the type-shape measure to resolve this boils the problem down to what 
unification requires

C Int b   --(b = [[Int]])-->   C Int [[Int]]
C a [[b]]   --(a = Int, b = Int)-->   C Int [[Int]]

The assignments required for the first (b = [] ([] Int)) involve three terms.  
The assignments required for the second (a = Int and b = Int) involve two 
terms.  This means the second wins out as being the simplest.

It's easy to compute, and I believe it completely subsumes GHCs current 
definition of more specific.  The fact that we can get (A) from (B) by doing 
substitutions on (B) implies that something that unifies against both (A) and 
(B) will involve more terms in the substitutions done in unifying against (B).

The complexity of the paper was in the derivation of the measure.  The 
implication of the results is really really simple.  Just count terms.

Cheers!  -Tyson