An ambiguous type variable is fixed with a type constraint

Question

I am working on a monadic stream library, and I came across a type that I don't understand. I managed to reduce it to the following example:

{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies #-} class Foo ab where type E ab :: * (>->) :: a -> b -> E ab 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 think, surprises me a little, although maybe not too much. It really surprises me that if I replace the instance with the following, then everything will work:

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

I do not see the difference between the two instance declarations. I assume this is due to the way type variables change. Can someone explain what is happening?

[Beyond this: I see the same when using fundeps.]

Answer 1

Edit : The GHC Instance Resolution User Guide section is a good place to start.

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

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

Now it’s clear why this is not possible? We get the error:

 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 is nothing to see that a ~ Int . Rewrite it:

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

This works great even with your original copy. (Edit: I suspect the following sentence is either useless or misleading, or both.) z' (approximately), where typechecker ends with your rewritten instance definition: it sees an instance for (Bar a) (Bar a') , which requires (a ~ a') , and simply adds this constraint to the call.

Roughly speaking, the resolution of an instance goes from right to left, and sometimes unexpected consequences.

Edit: And the result of resolving from right to left is that instance (x ~ x') => Foo (Bar x) (Bar x') matches any two types x and x' , whether or not x ~ x' valid, Constraint just spreads to the call site. Therefore, you cannot write another instance for certain types. It will overlap, which is prohibited by default, and, in addition, the GHC does not specifically back out when resolving instances. instance Foo (Bar x) (Bar x) , on the other hand, will not be applied if it does not have the same type in both places - the GHC will not invent a constraint because (x ~ y) => M xy does not match with M xx .

Depending on your actual usecase, you can read the documentation for OverlappingInstances . Again, depending on what you are doing, some of the recent innovations in families , such as closed family types , may be relevant.