How does IncoherentInstances work?

Question

Playing around with some code:

{-# LANGUAGE FlexibleInstances, OverlappingInstances #-}

class Arity f where
  arity :: f -> Int

instance Arity x where
  arity _ = 0

instance Arity f => Arity ((->) a f) where
  arity f = 1 + arity (f undefined)

Without IncoherentInstances:

ghci> arity foldr
blah blah ambiguous blah blah possible fix blah
ghci> arity (foldr :: (a -> Int -> Int) -> Int -> [a] -> Int)
3
ghci> let f x y = 3 in arity f
2
ghci> arity $ \x y -> 3
2

If we add IncoherentInstances to the list of pragmas, then it can handle foldr without needing a monomorphic type signature, but it gets the wrong answer on lambdas:

ghci> arity foldr
3
ghci> let f x y = 3 in arity f
2
ghci> arity $ \x y -> 3 -- should be 2
0

What is the black magic behind Incoherent Instances? Why does it do what it does here?

Answer 1

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.