Type inference is broken when dealing with tuple type synonyms

I have GHC 6.10.1 built from the sources. In the whole bugreport, suppose we have

{-# LANGUAGE TypeFamilies #-}

class Coll c where
  type Elem c
  empty :: c
  insert :: Elem c -> c -> c

data ListColl a = L [a]
instance Coll (ListColl a) where
  type Elem (ListColl a) = a
  empty = L []
  insert x (L xs) = L (x:xs)
emptyL :: ListColl a
emptyL = empty

GHCI says

test1 c = insert 0 c
test2 c = insert (0, 0) c

*Main> :t test1
test1 :: (Num (Elem c), Coll c) => c -> c
*Main> :t test2
test2 :: ((Integer, Integer) ~ Elem c, Coll c) => c -> c

Shouldn't be the type of test2 be something like test2 :: (Num a, Num b, (a, b) ~ (Elem c), Coll c) => c -> c ?

When trying

test1 c = insert 0 c
test2 c = insert (0, 0) c
test3 :: ListColl (Float, Float)
test3 = test2 emptyL

we get

*Main> :t test2
test2 : ((Float, Float) ~ Elem c, Coll c) => c -> c

and

test1 c = insert 0 c
test2 c = insert (0, 0) c
test3 :: ListColl (Float, Float)
test3 = test2 emptyL
test3':: ListColl (Int, Int)
test3'= test2 emptyL

    Couldn't match expected type `Int' against inferred type `Float'
      Expected type: Elem (ListColl (Int, Int))
      Inferred type: (Float, Float)
    When generalising the type(s) for `test3''
Failed, modules loaded: none.

and

test1 c = insert 0 c
test2 c = insert (0, 0) c
test4::(Num a, Num b) => ListColl (a, b)
test4 = test2 empty

    Inferred type is less polymorphic than expected
      Quantified type variable `b' escapes
      Quantified type variable `a' escapes
    When trying to generalise the type inferred for `test4'
      Signature type:     forall a b. (Num a, Num b) => ListColl (a, b)
      Type to generalise: ListColl (a, b)
    In the type signature for `test4'
    When generalising the type(s) for `test4'
Failed, modules loaded: none.

When adding explicit type signature test2 :: (Num a, Num b, (a, b) ~ (Elem c), Coll c) => c -> c all above examples works correctly, even if GHCI still says

:t test2
*Main> :t test2
test2 :: ((Integer, Integer) ~ Elem c, Coll c) => c -> c

Last weird thing is

test5 _ = insert 0 emptyL
*Main> :t test5
test5 :: (Num a) => t -> ListColl a

test6 _ = insert (0,0) emptyL
    Ambiguous type variable `t' in the constraint:
      `Num t'
        arising from the literal `0'
                     at /work/skola/haskell/grafy/Bug.hs:32:18
    Probable fix: add a type signature that fixes these type variable(s)

    Ambiguous type variable `t1' in the constraint:
      `Num t1'
        arising from the literal `0'
                     at /work/skola/haskell/grafy/Bug.hs:32:21
    Probable fix: add a type signature that fixes these type variable(s)
Failed, modules loaded: none.

but adding

test6 :: (Num a, Num b, (a, b) ~ (Elem (ListColl c)), Coll (ListColl c)) => foo -> (ListColl c)
test6 _ = insert (0,0) emptyL

once again solves the problem.

Is this really a bug or just a feature :) I understand that in t1 ~ t2, the t1 and t2 can be arbitraty monotypes, so (a, b) should work, even with Num a and Num b, right?

Cheers, Milan Straka

Trac metadata

Trac field	Value
Version	6.10.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture