Reputation: 3
Consider the following code:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
class X a
class Y a
instance Y Bool
instance (Y a) => X a
instance {-# OVERLAPPING #-} X Int
f :: (X a) => a -> a
f x = x
These LANGUAGE pragma's are needed to write the above instances.
Now, say we want to write a function g:
g :: (Y a) => a -> a
g = f
Without IncoherentInstances or adding {-# INCOHERENT #-} to one of the instances, this doesn't typecheck. But when we do add this, and ask ghci
ghci> :t f
f :: Y a => a -> a
Suddenly the type of 'f' changed?
With this small example, programs still typecheck when I give f an Int (indicating that the above would be merely a 'visual bug', but in a bigger example the same does not typecheck, giving me an error like:
Could not deduce (Y a) arising from a use of 'f
(...)
from the context: (..., X a, ...)
This also happens when we say
h = f
and try to call h with an Int
Upvotes: 0
Views: 75
Reputation: 29193
:type f
does not report the type of the defined entity f
. It reports the type of the expression f
. GHC tries really hard to stamp polymorphism out of expressions. In particular, using f
in an expression triggers simplification of the X a
constraint (as does using any definition with a constraint). Without IncoherentInstances
, GHC refrains from using instance Y a => X a
, because there is another instance that overlaps it, so GHC needs to wait to see which one it should use. This ensures coherence; the only X Int
instance that is ever used is the explicitly "specialized" one. With IncoherentInstances
, you say that you don't care about coherence, so GHC goes ahead and simplifies X a
to Y a
using the polymorphic instance whenever f
appears in an expression. The weird behavior you see where sometimes GHC is OK with using X Int
and sometimes complains that there is no Y Int
is a result of GHC making different internal decisions about when it wants to simplify constraints (you did ask for incoherence!). The command for seeing the type of a definition is :type +v
. :type +v f
should show the type of f
"as declared". Hopefully, you can also see that IncoherentInstances
is a bad idea. Don't use it.
Upvotes: 2