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 |