Adding an unused instance fixes a type error

Question

Consider this code:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}

module Foo where

class Foo a

class SomeClass a
instance {-# OVERLAPPABLE #-} (Foo a) => SomeClass a

bar :: (SomeClass a) => a -> Int
bar = const 0

foo :: (SomeClass a) => a -> Int
foo t = let x = bar t in x

Here, foo calls bar, and should be able to do so using the SomeClass constraint in its context. Instead, GHC assumes it must do so using the Foo a => SomeClass a instance:

Foo.hs:16:17:
    Could not deduce (Foo a) arising from a use of ‘bar’
    from the context (SomeClass a)
      bound by the type signature for foo :: SomeClass a => a -> Int
      at Foo.hs:15:8-32
    Possible fix:
      add (Foo a) to the context of
        the inferred type of x :: Int
        or the type signature for foo :: SomeClass a => a -> Int
    In the expression: bar t
    In an equation for ‘x’: x = bar t
    In the expression: let x = bar t in x

There are two ways to fix this:

1. In foo, changing let x = bar t in x to bar t
2. Appending the line instance SomeClass Int to my program

What is going on here? Why is this problem occurring, and why do these fixes work?

---

This example is, of course, simplified by my actual problem. I encountered it during my work on the Cubix framework for multi-language transformation ( arxiv.org/pdf/1707.04600 ).

My actual problem involves a function with a constraint InjF f IdentL FunctionExpL ("f is a language where identifiers may be used to denote the function in a function call"). I have an (overlappable) instance (FunctionIdent :<: f) => InjF f IdentL FunctionExpL, which the typechecker seizes on, giving me a spurious Could not deduce FunctionIdent :<: f error.

This error persists even when there is an instance InjF Foo IdentL FunctionExpL in scope for a specific Foo, so leftaroundabout's answer, which predicts that that other instance should fix the problem, is not the full story.

Answer 1

The reason for this is that the compiler tries to make x as general as possible: it wants it to be (SomeClass a) => Int (notice this would be an ambiguous type if you wrote it out yourself). One way to prevent this kind of weird local type is to enable -XMonoLocalBinds, but I wouldn't really recommend it.

Now, the compiler goes on to typechecking. At that point, there is exactly one instance SomeClass in scope, namely the catch-all (Foo a) => SomeClass a, so there's no ambiguity. (In principle, Haskell completely forbids ambiguity in instance resolution; OVERLAPPABLE subverts this but it only jumps into action when there's actually a need, like when you have an extra instance SomeClass Int.) Therefore, the compiler immediately commits to that instance and thus eliminates (SomeClass a) for the type-checking of c. That it does this is necessary for situations where you actually want a class constraint to be replaced by the constraint of an instance. This may seem useless in the given example, but it's actually crucial when you have instances of the form

instance Bar a => SomeClass (Maybe a)

...which is much more reasonable than your code because that can't be expressed as a superclass constraint, and is perfectly ok without any overlap. If the compiler didn't reduce the constraint resolving down to Bar a in those situations, it could never actually resolve down the Maybe type.

Conlusion: avoid overlapping instances; express class relations by superclass declarations if possible, else reify the constraints into a GADT (which is awkward but gives you exact control where which constraint is going to be used).