Consider the following program, which only compiles with incoherent instances enabled:
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}
main = do
print (g (undefined :: Int))
print (g (undefined :: Bool))
print (g (undefined :: Char))
data True
class CA t where
type A t; type A t = True
fa :: t -> String
instance CA Int where
fa _ = "Int"
class CB t where
type B t; type B t = True
fb :: t -> String
instance CB Bool where
fb _ = "Bool"
class CC t where
type C t; type C t = True
fc :: t -> String
instance CC Char where
fc _ = "Char"
class CAll t t1 t2 t3 where
g :: (t1 ~ A t, t2 ~ B t, t3 ~ C t) => t -> String
instance (CA t) => CAll t True t2 t3 where g = fa
instance (CB t) => CAll t t1 True t3 where g = fb
instance (CC t) => CAll t t1 t2 True where g = fc
When compiling without incoherent instances it claims multiple instances match. This would seem to imply that when incoherent instances are allowed, the instances would be chosen arbitrarily.
Unless I'm exceedingly lucky, this would result in compile errors as the instance constraints in most cases would not be satisfied.
But with incoherent instances I get no compile errors, and indeed get the following output with the "correct" instances chosen:
"Int"
"Bool"
"Char"
So I can only conclude either one of a few things here:
- GHC is backtracking on instance context failures (something it says it doesn't do in it's own documentation)
- GHC actually knows there's only one instance that matches, but isn't brave enough to use it unless one turns on incoherent instances
- I've just got exceedingly lucky (1 in 33 = 27 chance)
- Something else is happening.
I suspect the answer is 4 (maybe combined with 2). I'd like any answer to explain what's going on here, and how much I can rely on this behavior with incoherent instances? If it's reliable it seems I could use this behaviour to make quite complex class hierarchies, that actually behave somewhat like subtyping, e.g. I could say all types of class A and class B are in class C, and an instance writer could make an instance for A without having to explicitly make an instance for C.
Edit:
I suspect the answer has something to do with this in the GHC docs:
- Find all instances I that match the target constraint; that is, the target constraint is a substitution instance of I. These instance declarations are the candidates.
- Eliminate any candidate IX for which both of the following hold:
- There is another candidate IY that is strictly more specific; that is, IY is a substitution instance of IX but not vice versa.
- Either IX is overlappable, or IY is overlapping. (This "either/or" design, rather than a "both/and" design, allow a client to deliberately override an instance from a library, without requiring a change to the library.)
If exactly one non-incoherent candidate remains, select it. If all remaining candidates are incoherent, select an arbitary one. Otherwise the search fails (i.e. when more than one surviving candidate is not incoherent).
If the selected candidate (from the previous step) is incoherent, the search succeeds, returning that candidate.
If not, find all instances that unify with the target constraint, but do not match it. Such non-candidate instances might match when the target constraint is further instantiated. If all of them are incoherent, the search succeeds, returning the selected candidate; if not, the search fails.
Correct me if I'm wrong, but whether incoherent instances is selected or not, in the first step, there's only one instance that "matches". In the incoherent case, we fall out with that "matched" case at step 4. But in the non-incoherent case, we then go to step 4, and even though only one instance "matches", we find other instances "unify". So we must reject.
Is this understanding correct?
And if so, could someone explain exactly what "match" and "unify" mean, and the difference between them?
