Instance resolution corner case

instance_resolution-corner_case.md

Source: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overlapping-instances

As a more substantial example of the rules in action, consider

instance {-# OVERLAPPABLE #-} context1 => C Int b     where ...  -- (A)
instance {-# OVERLAPPABLE #-} context2 => C a   Bool  where ...  -- (B)
instance {-# OVERLAPPABLE #-} context3 => C a   [b]   where ...  -- (C)
instance {-# OVERLAPPING  #-} context4 => C Int [Int] where ...  -- (D)

The constraint C Int [Int]. This constraint matches instances (A), (C) and (D), but the last is more specific, and hence is chosen.

If (D) did not exist then (A) and (C) would still be matched, but neither is most specific. In that case, the program would be rejected, unless IncoherentInstances is enabled, in which case it would be accepted and (A) or (C) would be chosen arbitrarily.

The final bullet (about unifiying instances) makes GHC conservative about committing to an overlapping instance. For example:

f :: [b] -> [b]
f x = ...

Suppose that from the RHS of f we get the constraint C b [b]. But GHC does not commit to instance (C), because in a particular call of f, b might be instantiated to Int, in which case instance (D) would be more specific still. So GHC rejects the program.

This explains why GHC rejects the following

instance {-# OVERLAPPABLE #-} Coat Sunny b where doINeedACoat _ _ = False
instance {-# OVERLAPPING #-} Coat a Cold where doINeedACoat _ _ = True

The only workaround is using INCOHERENT:

instance {-# INCOHERENT #-} Coat Sunny b where doINeedACoat _ _ = False
instance Coat a Cold where doINeedACoat _ _ = True

question.md

instance {-# OVERLAPPABLE #-} C Int b    where c _ _ = ()
instance {-# OVERLAPPING #-} C a   Bool where c _ _ = ()

test :: ()
test = c (10 :: Int) True
-- ^^^^^ Compilation Error

GHC refuses to commit to the overlapping instance, why ?

Overlapping instances requires the winning instance to be more specific than other possible instances. There's an in depth explanation of how the instance search works in the GHC user's guide: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#overlapping-instances.

Read 3)

Constraint resolution:

1. 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.
2. If no candidates remain, the search failes
3. Eliminate any candidate \(IX\) for which there is another candidate \(IY\) such that both of the following hold:
  3.1. \(IY\) is strictly more specific than \(IX\). That is, \(IY\) is a substitution instance of \(IX\) but not vice versa.
  3.2. 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.)
4. If all the remaining candidates are incoherent, the search suceeds, returning an arbitrary surviving candidate.
5. If more than one non-incoherent candidate remains, the search fails.
6. Otherwise there is exactly one non-incoherent candidate; call it the “prime candidate”.
7. Now find all instances, or in-scope given constraints, 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 top-level instances, the search succeeds, returning the prime candidate. Otherwise the search fails.