Ambiguous type variable fixed with type equality constraint

Question

I'm working on a monadic streaming library and I've run into a type thing I don't understand. I've managed to reduce it to the following example:

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}

class Foo a b where
  type E a b :: *
  (>->) :: a -> b -> E a b

data Bar x

instance Foo (Bar x) (Bar x) where
  type E (Bar x) (Bar x) = Bar x
  (>->) = undefined

x = undefined :: Bar a
y = undefined :: Bar Int

z = x >-> y

When I try to compile it, I get:

No instance for (Foo (Bar a0) (Bar Int))
  arising from a use of ‘>->’
The type variable ‘a0’ is ambiguous
Relevant bindings include
  z :: E (Bar a0) (Bar Int)
    (bound at /usr/local/google/home/itaiz/test/test.hs:17:1)
Note: there is a potential instance available:
  instance Foo (Bar x) (Bar x)
    -- Defined at /usr/local/google/home/itaiz/test/test.hs:10:10
In the expression: x >-> y
In an equation for ‘z’: z = x >-> y

which, I guess, surprises me a little, though maybe not too much. What really does surprise me is that if I replace the instance with the following then everything works:

instance (x ~ x') => Foo (Bar x) (Bar x') where
  type E (Bar x) (Bar x') = Bar x
  (>->) = undefined

I don't see the difference between the two instance declarations. I'm guessing this has something to do with how type variables are scoped. Can someone explain what's going on?

[Aside: I see the same thing when using fundeps instead.]

Answer 1

Edit: The GHC user guide section on instance resolution is a good place to start.

Here's how to break down why this is happening. Your z is roughly equivalent to this:

z :: Bar a -> Bar Int -> E (Bar a) (Bar Int)
z = (>->)

Is it now clearer why it's not possible? The error we get is:

SO26146983.hs:20:5:
    No instance for (Foo (Bar a) (Bar Int)) arising from a use of `>->'
    In the expression: (>->)
    In an equation for `z': z = (>->)

There's nothing to show that a ~ Int. Let's rewrite it:

z' :: (a ~ Int) => Bar a -> Bar Int -> E (Bar a) (Bar Int)
z' = (>->)

This works fine even with your original instance. (Edit: I suspect the following sentence is either unhelpful or misleading or both.) z' is (roughly) where the typechecker ends up with your rewritten instance definition: it sees an instance for (Bar a) (Bar a') which requires (a ~ a'), and just adds that constraint to the call.

Roughly speaking, instance resolution goes right to left, with sometimes-unexpected consequences.

Edit: And the result of the right-to-left resolution is that instance (x ~ x') => Foo (Bar x) (Bar x') matches any two types x and x', whether or not x ~ x' is actually the case. The constraint is just propagated to the call site. So you can't then write another instance for particular types. It would overlap, which is prohibited by default, and furthermore GHC specifically does not backtrack when resolving instances. instance Foo (Bar x) (Bar x) on the other hand won't be applied unless it's the same type at both places--GHC won't invent the constraint, because (x ~ y) => M x y is not the same as M x x.

Depending on your actual usecase, you may want to read the documentation for OverlappingInstances. Again depending on what you're doing, some of the recent innovations in type families, such as closed type families, may be relevant.