This code sample doesn't compile.
{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, ScopedTypeVariables #-}
module IncoherentBug where
type family F a where
F () = Int
F a = a
class C a where
c :: a -> Int
instance C Int where
c y = y
instance {-# INCOHERENT #-} Monoid a => C a where
c _ = 0
class TwoPossible a where
x :: a
instance a ~ () => TwoPossible [a] where
x = []
instance TwoPossible Bool where
x = False
f :: (F a -> Int) -> [a] -> ()
f _ _ = ()
test = f (\v -> c v) x
Basically what's happening here is the signature of f requests that the type of x gets resolved to [()], then the type of v is F () which is Int, and finally the first instance of C should be picked. What happens instead is that I get a missing Monoid Int instance error.
The code compiles fine when I change the INCOHERENT instance to an OVERLAPPABLE one. It also works if I annotate v with either Int or F (). It also works if I annotate x (as the parameter to f) with [()].
Is this a bug or am I misunderstanding something here? ghc-mod reports the type F () for v even if I don't annotate it as such. Besides the fact that the error message mentions an Int means that the type checker figured out the correct type for v but for some reason didn't pick the more specific instance.
I should also maybe note that I'm using GHC 8. I don't know if this issue appears in the earlier versions.
GHC is completely correct to reject this code. You have a C (F a) constraint which arises from
f c :: C (F a) => [a] -> ()
When you turn on INCOHERENT , GHC will immediately reduce this to
f c :: Monoid (F a) => [a] -> ()
without even considering the type of the argument. That is what incoherence means - an instantiation could provide a more specific instance, but an incoherent instance matches anyways. And of course the instance ... => C a matches every type, so if your C constraint appears anywhere, that instance will be matched immediately.
With OVERLAPPABLE or the like, the C (F a) constraint cannot be reduced by selecting the Monoid a => C a instance, because the C Int instance could match as well (this is coherence, the opposite of incoherence).
If you want to see yourself, ask GHC for the inferred type of f c with INCOHERENT and OVERLAPPABLE.