At Sun, 26 Jun 2011 00:17:12 +0100, Paterson, Ross wrote:
g1 x y z = if x>y then show x ++ show z else g2 y x
g2 :: (Show a, Ord a) => a -> a -> String g2 | False = \p q -> g1 q p () | otherwise = \p q -> g1 q p 'a' where x = True
It appears to me that GHC is justified. According to 4.5.1 and 4.5.2, g1 by itself constitutes a declaration group. It is considered by itself and is generalized prior to combining it with g2.
Great, now I'm even more confused. 4.5.1 says:
A binding b1 depends on a binding b2 in the same list of declarations if either
1. b1 contains a free identifier that has no type signature and is bound by b2, or
2. b1 depends on a binding that depends on b2.
A declaration group is a minimal set of mutually dependent bindings. Hindley-Milner type inference is applied to each declaration group in dependency order.
So here the first binding (of g1) contains the free identifier g2, which is bound by the second binding. Conversely, the second binding contains g1 free. So the two bindings are mutually dependent, no?
No, the binding of g1 doesn't depend on the binding of g2, because g2 has a type signature (clause 1).
I thought "no type signature" meant no type signature inside b1. Otherwise, you are saying nothing could depend on a binding with a type signature. By that logic, there can be no mutual dependence, and so every declaration with a type signature is its own (singleton) declaration group. But this can't be what the committee was thinking given the following language in section 4.5.2: If the programmer supplies explicit type signatures for more than one variable in a declaration group, the contexts of these signatures must be identical up to renaming of the type variables. Such a restriction would be vacuous if every type signature created a singleton declaration groups. Moreover, section 4.5.5 is also inconsistent with such an interpretation: The monomorphism restriction Rule 1. We say that a given declaration group is unrestricted if and only if: (a): every variable in the group is bound by a function binding or a simple pattern binding (Section 4.4.3.2), and (b): an explicit type signature is given for every variable in the group that is bound by simple pattern binding. If every binding with an explicit type signature is its own declaration group, then why isn't the monomorphism restriction stated more simply as follows? (a): every binding is a function binding, or (b): the group consists of a pattern binding with an explicit type signature. When they say "an explicit type signature is given for every variable in the group..." they have to be thinking there may be more than one of them.
The type of g1 is inferred using the declared type of g2. Then that type is used in inferring a type for g2, which will be compared with its declared signature.
Thanks for the reply, but now I'm now even more confused. Perhaps I should ask if someone can give me a better definition of declaration group, ideally with support in the language spec... David