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.