Well this is quite complicated. Lets start with the ambiguous error:

```
<interactive>:1:1:
Ambiguous type variable `b0' in the constraint:
(Arity b0) arising from a use of `arity'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: arity foldr
In an equation for `it': it = arity foldr
```

Normally, without overlapping instances, when attempting to match a type against a class, it will compare the type against all instances for that class. If there is exactly one match, it will use that instance. Overwise you will either get a no instance error (eg with `show (*)`

), or an overlapping instances error. For example, if you remove the `OverlappingInstances`

language feature from the above program, you will get this error with `arity (&&)`

:

```
<interactive>:1:1:
Overlapping instances for Arity (Bool -> Bool -> Bool)
arising from a use of `arity'
Matching instances:
instance Arity f => Arity (a -> f)
-- Defined at tmp/test.hs:9:10-36
instance Arity x -- Defined at tmp/test.hs:12:10-16
In the expression: arity (&&)
In an equation for `it': it = arity (&&)
```

It matches `Arity (a -> f)`

, as `a`

can be `Bool`

and `f`

can be `Bool -> Bool`

. It also matches `Arity x`

, as `x`

can be `Bool -> Bool -> Bool`

.

With `OverlappingInstances`

, when faced with a situation when two or more instances can match, if there is a most specific one it will be chosen. An instance `X`

is more specific than an instance `Y`

if `X`

could match `Y`

, but not vice versa.

In this case, `(a -> f)`

matches `x`

, but `x`

does not match `(a -> f)`

(eg consider `x`

being `Int`

). So `Arity (a -> f)`

is more specific than `Arity x`

, so if both match the former will be chosen.

Using these rules, `arity (&&)`

will firstly match `Arity ((->) a f)`

, with `a`

being `Bool`

, and `f`

being `Bool -> Bool`

. The next match will have `a`

being `Bool`

and `f`

being bool. Finally it will end matching `Arity x`

, with `x`

being Bool.

Note with the above function, `(&&)`

result is a concrete type `Bool`

. What happens though, when the type is not concrete? For example, lets look at the result of `arity undefined`

. `undefined`

has the type `a`

, so it isn’t a concrete type:

```
<interactive>:1:1:
Ambiguous type variable `f0' in the constraint:
(Arity f0) arising from a use of `arity'
Probable fix: add a type signature that fixes these type variable(s)
In the expression: arity undefined
In an equation for `it': it = arity undefined
```

You get an abiguous type variable error, just like the one for foldr. Why does this happen? It is because depending on what `a`

is, a different instance would be required. If `a`

was `Int`

, then the `Arity x`

instance should be matched. If `a`

was `Int -> Int`

, then the `Arity ((->) a f)`

instance should be matched. Due to this, ghc refuses to compile the program.

If you note the type of foldr: `foldr :: forall a b. (a -> b -> b) -> b -> [a] -> b`

, you will notice the same problem: the result is not a concrete variable.

Here is where `IncoherentInstances`

comes in: with that language feature enabled, it will ignore the above problem, and just choose an instance that will always match the variable. Eg with `arity undefined`

, `Arity x`

will always match `a`

, so the result will be 0. A similar thing is done at for `foldr`

.

Now for the second problem, why does `arity $ \x y -> 3`

return 0 when `IncoherentInstaces`

is enabled?

This is very weird behaviour. This following ghci session will show how weird it is:

```
*Main> let f a b = 3
*Main> arity f
2
*Main> arity (\a b -> 3)
0
```

This leads me to think that there is a bug in ghc, where `\a b -> 3`

is seen by `IncoherentInstances`

to have the type `x`

instead of `a -> b -> Int`

. I can’t think of any reason why those two expressions should not be exactly the same.