Ambiguous type with type families

Question

I am running into a problem where GHC is not able to match Foo t and Foo t0, where it definitely looks to me like t ~ t0. Here's 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, 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 is not injective, but from my analysis GHC is never asked to come up with t from Foo t. It seems that the type t is lost in Foobar g, and so it can't match the inital Foo t and the new Foo t0. Is the context here not enough? Am I missing a case where f = Foobar g could not yield the correct result?

Any help appreciated!

N.B.: ScopedTypeVariables and explicit type signatures don't seem to help. Adding the constraint a ~ Foo t and using a instead as the type of g in Foobar g doesn't work either.

Looks a lot like: ambiguous type error when using type families, and STV is not helping. I considered using a Proxy, but I feel like in this case GHC should be able to figure it out.

Answer 1

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

So, you realize the ambiguity. Let's make is explicit:

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 in f = Foobar g is related to the ambiguity.

The crux is: the definition f = Foobar g does not imply that g much be picked in the same instance as f. It could refer to a different instance!

Consider

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

Above, the RHS uses of show are from a different instance from the one where the LHS show is.

In your f = Foobar g line, GHC infers that g :: Foo t where t is the same index of the f instance. However, that is not enough to select an instance for g! Indeed, we might have Foo t ~ Foo t0 for some other t0, hence g might refer to the g in the t0 instance, causing an ambiguity error.

Note that your code is rejected by GHC 8 even if the last line is commented out, because the type of 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 more lenient, like GHC 7. This will make your code type check, 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 you saw in GHC 7. In GHC 8, we have another luxury: we can explicitly choose the t for g as follows:

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

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