CODEWITHSUNDEEP
haskelltypeclass
Pond Premtoon
Pond Premtoon

Reputation: 93

How constraints in the context change instance resolution in Haskell

I am trying to understand how adding a constraint to an instance context changes instance resolution in Haskell. In this example:

class C a where
  f :: a -> [Char]

instance {-# OVERLAPPABLE #-} C a where
  f = const "thing"

instance C Int where
  f = const "int"

instance {-# OVERLAPPING #-} C [a] where
  f [] = "empty list"
  f (x : xs) = "list of " ++ f x

main = do
  putStrLn $ f (1 :: Int)
  putStrLn $ f [(True :: Bool)]
  putStrLn $ f [(1 :: Int)]
  putStrLn $ f [[(1 :: Int)]]

The output is:

int
list of thing
list of thing
list of thing

The last two lines are not what I want. For the 3rd line, it seems that the compiler (or runtime?), when running f for the list instance, doesn't know that a is Int and just uses the default C a instance. Similarly for the last line, it can't figure out that a is another list. However, if I add a context to the list instance:

instance {-# OVERLAPPING #-} (C a) => C [a] where
  f [] = "empty list"
  f (x : xs) = "list of " ++ f x

The output becomes:

int
list of thing
list of int
list of list of int

...which is what I want. Can someone help explain how that constraint changes the instance resolution in this example? Are there any general rules I can look at?

Upvotes: 3

Views: 116

Answers (1)

chi
chi

Reputation: 116139

Essentially, instance selection is performed at compile-time, only. At runtime, there is no type information around, and there is no list of instances stored anywhere to drive the instance selection.

So, what is happening in your instances? Consider the first case:

instance {-# OVERLAPPING #-} C [a] where
  f [] = "empty list"
  f (x : xs) = "list of " ++ f x

Assume that f is passed a list of type [a0] (let's use a fresh variable name for clarity). We then need to type check f x in the last line. Variable x above has type a0, so GHC needs to solve C a0. For that, GHC has to pick some instance. Normally it would refuse to choose instance C a since instance C Int also exists, and GHC does not know whether a0 = Int, so no single instance can be picked as the "definitive" one with only the information at hand.

However, the "overlapping" pragma instructs GHC to pick the single best instance among those that are general enough to solve the constraint. Indeed, that's the best we can do with the information at hand: the only other reasonable option is to raise an error.

In this case, to solve C a0 we need to pick one of the three instances, and only instance C a is general eonugh to match C a0 (after all, a0 could be a non-Int, non-list type). So we pick that.

Instead, using

instance {-# OVERLAPPING #-} (C a) => C [a] where
  f [] = "empty list"
  f (x : xs) = "list of " ++ f x

opens a fourth option to solve C a0, namely using the context C a0 which is available. When f is called, it is being passed an implicit argument carrying a dictionary for C a0 (i.e. the f for the type a0).

So, now GHC has two viable options: solving C a0 using the C a0 context (i.e. using the implicit argument), or resorting to the global instance C a. The first one is more specific, since it applies only to a0 rather than to any type a, so it is considered to be the "best", and chosen.

Upvotes: 5

Related Questions