One of our students had a program that successfully compiled with Hugs but failed to type check in GHC. After adding some type signatures GHC could compile the program as well. The definitions below are not supposed to make sense, (f and g are just identity functions) but illustrate the situation in the students code: 1) the functions f and g are mutually recursive 2) there is a sort of (indirect) polymorphic recursion - the polymorphic types of f and g are instantiated to (Char->Char) f :: a -> a f a | True = a | g 'a' == 'a' = g a g :: a -> a g a | True = a | f 'a' == 'a' = f a The code above is successfully type-checked by both Hugs and GHC. If we remove either the type signature of f or the type signature of g, however, GHC fails to type check the code. Hugs still infers: f,g :: a->a When removing both type signatures GHC and Hugs both infer f,g::Char->Char, as expected. So this code failed in GHC: f :: a -> a f a | True = a | g 'a' == 'a' = g a g a | True = a | f 'a' == 'a' = f a Is this a bug in GHC or a feature of Hugs? I did not check what NHC and other Haskell compilers say about this. Can someone try? Cheers, Arthur
Arthur Baars <arthurb@cs.uu.nl> writes:
f :: a -> a f a | True = a | g 'a' == 'a' = g a
g :: a -> a g a | True = a | f 'a' == 'a' = f a
Is this a bug in GHC or a feature of Hugs? I did not check what NHC and other Haskell compilers say about this. Can someone try?
nhc98 agrees with GHC rather than Hugs. The code above compiles fine. If you omit one type signature, the error is Derived type for Test.f at 4:1 does not match due to: given free variable a is bound to Prelude.Char Derived:(Prelude.Char -> Prelude.Char) Given :(a -> a) If you omit both signatures, f and g are typed as Char->Char. With or without type signatures, nhc98 additionally emits warnings: ====== Warning pattern removal: Alternative at 9:22 is hidden by alternative at 8:7 Alternative at 5:22 is hidden by alternative at 4:7 Regards, Malcolm
In Mark Jones' paper Typing Haskell in Haskell, I found the following example(in the section on binding-groups): f :: Eq a => a -> Bool f x = x==x || g True g y = y<=y || f True According to the paper the inferred type of g should be: g::Ord a => a -> Bool Hugs infers this type but GHC infers the following *ambiguous* type: *Main> :i g -- g is a variable, defined at Test.hs:25 g :: forall a. (Eq a) => Bool -> Bool When adding an explicit type signature for g, Hugs happily accepts the code, but GHC gives the following error: f :: Eq a => a -> Bool f x = x==x || g True g :: Ord a => a -> Bool g y = y<=y || f True Test.hs:24: Couldn't match `{Ord a}' against `{Eq a1}' When matching the contexts of the signatures for g :: forall a. (Ord a) => a -> Bool f :: forall a. (Eq a) => a -> Bool The signature contexts in a mutually recursive group should all be identical When generalising the type(s) for g, f Failed, modules loaded: none. I think the problems are caused by differences in the binding group analysis in Hugs and GHC. Malcolm, could you check what NHC says about the examples above? Cheers, Arthur
Arthur Baars <arthurb@cs.uu.nl> writes:
f :: Eq a => a -> Bool f x = x==x || g True g y = y<=y || f True
According to the paper the inferred type of g should be: g::Ord a => a -> Bool
Hugs infers this type but GHC infers the following *ambiguous* type: g :: forall a. (Eq a) => Bool -> Bool
nhc98 infers the type g :: Bool -> Bool
When adding an explicit type signature for g, Hugs happily accepts the code, but GHC gives an error:
nhc98, like Hugs, accepts the explicit (more general) type signature: g :: Ord a => a -> Bool without complaint. Regards, Malcolm
I believe the incompatibilities are explained thus: In section 4.5.1 of the Haskell Report it only states that "A dependency analysis transformation is first performed to increase polymorphism" But hugs appears to be using a more refined version of the dependency analysis as explained in section 11.6.3 of Mark Jones' paper Typing Haskell in Haskell. Read that section. - Mark Arthur Baars wrote:
In Mark Jones' paper Typing Haskell in Haskell, I found the following example(in the section on binding-groups):
f :: Eq a => a -> Bool f x = x==x || g True g y = y<=y || f True
According to the paper the inferred type of g should be: g::Ord a => a -> Bool
Hugs infers this type but GHC infers the following *ambiguous* type: *Main> :i g -- g is a variable, defined at Test.hs:25 g :: forall a. (Eq a) => Bool -> Bool
When adding an explicit type signature for g, Hugs happily accepts the code, but GHC gives the following error:
f :: Eq a => a -> Bool f x = x==x || g True g :: Ord a => a -> Bool g y = y<=y || f True
Test.hs:24: Couldn't match `{Ord a}' against `{Eq a1}' When matching the contexts of the signatures for g :: forall a. (Ord a) => a -> Bool f :: forall a. (Eq a) => a -> Bool The signature contexts in a mutually recursive group should all be identical When generalising the type(s) for g, f Failed, modules loaded: none.
I think the problems are caused by differences in the binding group analysis in Hugs and GHC.
Malcolm, could you check what NHC says about the examples above?
Cheers, Arthur
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
participants (3)
-
Arthur Baars -
Malcolm Wallace -
Mark Tullsen