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.