David van Balen
David van Balen

Reputation: 3

How do the various "..Instances" pragma's work together, and is there a way around my current problem?

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

Answers (1)

HTNW
HTNW

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

Related Questions