Ambiguous type with family types

Question

I ran into a problem when the GHC cannot match Foo t and Foo t0 , where it definitely looks like t ~ t0 me. Here is a minimal example:

 {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeFamilies #-} data Foobar :: * -> * where Foobar :: Foo t -> Foobar t type family Foo a :: * class Bar t where f :: Foobar t g :: Foo t -- f = Foobar g 

When uncommenting the last line, the GHC complains:

 Couldn't match expected type 'Foo t' with actual type 'Foo t0' NB: 'Foo' is a type function, and may not be injective The type variable 't0' is ambiguous Relevant bindings include f :: Foobar t (bound at test.hs:13:3) In the first argument of 'Foobar', namely 'g' In the expression: Foobar g 

I understand that Foo not injective, but from my analysis GHC never asked to come up with t from Foo t . It seems that type t is lost in Foobar g , and therefore it cannot match inital Foo t and the new Foo t0 . Is there not enough context? I missed the case when f = Foobar g could not give the correct result?

Any help appreciated!

NB: ScopedTypeVariables and explicit signatures do not help. We add the restriction a ~ Foo t and using a , and the type g in Foobar g does not work either.

It looks like: an ambiguous type error when using type families, and STV does not help . I reviewed the use of Proxy , but I feel that in this case the GHC should be able to understand this.

Answer 1

I understand that Foo not injective, but from my analysis GHC never asked to come up with t from Foo t .

So, you are aware of the ambiguity. Let make explicitly:

 type instance Foo () = Bool type instance Foo Char = Bool instance Bar () where -- I omit the declaration for f g = True instance Bar Char where g = False main = print (g :: Bool) 

Your problem with f = Foobar g is ambiguity.

The bottom line: the definition of f = Foobar g does not mean that g can be selected in the same instance as f . This may apply to another instance!

Consider

 show (x,y) = "(" ++ show x ++ ", " ++ show y ++ ")" 

Above, RHS uses show from another instance of where LHS show .

On your line f = Foobar g GHC reports that g :: Foo t , where t is the same index of the instance of f . However, this is not enough to select an instance for g ! In fact, we could have Foo t ~ Foo t0 for some other t0 , so g can refer to g in instance t0 , causing an ambiguity error.

Note that your code is rejected by GHC 8, even if the last line is commented out, because type g is inherently ambiguous:

 • Couldn't match expected type 'Foo t' with actual type 'Foo t0' NB: 'Foo' is a type function, and may not be injective The type variable 't0' is ambiguous • In the ambiguity check for 'g' To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the class method: g :: forall t. Bar t => Foo t In the class declaration for 'Bar' 

We can follow the suggestion to make GHC 8 softer, for example GHC 7. This will do a code check of your code until we uncomment the last line.

 • Couldn't match expected type 'Foo t' with actual type 'Foo t0' NB: 'Foo' is a type function, and may not be injective The type variable 't0' is ambiguous 

This is the same error as in GHC 7. In GHC 8, we have another luxury: we can explicitly choose t for g as follows:

 class Bar t where f :: Foobar t f = Foobar (g @ t) g :: Foo t 

This requires, of course, a few more extensions. In GHC 7, you need a proxy server to be able to select an instance uniquely.