I’d say a good 5% of the threads on the haskell-cafe mailing list have something to do with the typechecker doing strange unexpected things. And the test code for 100% of these features one of the two lines:

{-# LANGUAGE UndecidableInstances #-} {-# -fallow-undecidable-instances #-}

There was one today asking why the typechecker was getting into an infinite loop… do people not know what *undecidable* means?! (This isn’t as rhetorical as it is phrased, people without a formal CS education probably do not) It seems like Haskell programmers, new and experienced alike, throw around this flag at the drop of a hat whenever a GHC error message suggests it.

STOP IT! You will enjoy Haskell much more if you just stay the heck away from this flag. The most common example I see is superclassing:

class Group g where (%) :: g -> g -> g ... instance Num g => Group g where ...

This is okay only so long as there are no other instances of Group. Let’s say the typechecker comes across an expression of the form `True % False`. `(%)` has the type *Group g => g -> g -> g*, so it will unify *g* with *Bool* and we get the type of the expression as *Group Bool => Bool*. Then we check the constraint *Group Bool*, searching for instances that match. Oh, here’s one, *Group g*. So we pick that instance and add the necessary constraints, and the type becomes *Num Bool => Bool*, which of course fails. The type checker does not backtrack to find another instance `Enum g => Group g` if you defined it, it just dies. If you defined explicitly `Group Bool` then it will probably work because of the order in which it checks for instances, but relying on this is a bad idea. But certainly two instances of this form will always break. The solution is (unfortunately) to use a newtype:

newtype AdditiveGroup g = AdditiveGroup { fromAdditiveGroup :: g } instance Num g => Group (AdditiveGroup g) where ...

In this case it was actually good that you had to do that though, since Num forms more than one group, it’s good to mark which one you mean.

What worries me more is that mtl uses UndecidableInstances, with a simple comment saying:

-- This instance needs -fallow-undecidable-instances, because -- it does not satisfy the coverage condition

No proof, no rationale why this is always solvable. It seems like another “GHC told me to add the flag so I did” (however it probably is not).

</rant> <!-- obviously -->

Do you mean

Argh. Your blog ate my quotemarks. I think you mean

`instance Num g => Group (AdditiveGroup g) where`

.Yeah, I seriously need to upgrade wordpress. And yes, you’re right, thanks.

There’s a big annoying problem: the unification algorithm does not perform the right occur check. It will unify x with t even if t contains some y which depends functionally on x. This is the source of the problem in many examples which loop even when they look structurally recursive. Fix that, and the coverage condition can be weakened. Weaken the coverage condition and you no longer need undecidable instances to write respectable type-level programs. Subtle stuff.

Another (partial) solution: switch to type families.

class MonadState s m | m -> s where

get :: m s

put :: s -> m ()

`instance (MonadState s m) => MonadState s (ReaderT r m) where`

...

becomes (I believe):

class MonadState m where

St m :: *

get :: m (St m)

put :: St m -> m ()

`instance (MonadState m) => MonadState (ReaderT r m) where`

St (ReaderT r m) = St m

...

No need for undecidable instances there, because it falls under the conditions of the termination checker for type families. In general, it seems easier to write type programs using type families without running into the termination checker.

Here is an example, where I ran into undecidable instances. The Code seems to work.

— lots of datas

data D1

data D2

…

data D11

class A where

…

instance A D1

instance A D2

…

instance A D9

— not instance A for D10 and D11

class B where

…

— taking a shortcut because i can provide a generic function for all x’es that are instance of A already: aka undecidable instances

instance A x =>B x where

…

instance B D10 where

…

instance B D11 where

…

instance

instance A a2

class B where

…