[GHC] #3017: Type inference is broken when dealing with tuple type synonyms

[GHC]

#3017: Type inference is broken when dealing with tuple type synonyms
-------------------------+--------------------------------------------------
Reporter:  straka.milan  |          Owner:          
    Type:  bug           |         Status:  new     
Priority:  normal        |      Component:  Compiler
 Version:  6.10.1        |       Severity:  normal  
Keywords:                |       Testcase:          
      Os:  Linux         |   Architecture:  x86     
-------------------------+--------------------------------------------------
 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

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3017>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler