Stop Using Undecidable Instances

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 -->
About these ads

6 thoughts on “Stop Using Undecidable Instances

  1. 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.

  2. 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.

  3. 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 A a2
    class B where

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s