Informally, what I see as the defining rule for "closed world" is: "an expression is typed according to the set of definitions that are visible in the context in which it is used". Other possibilities exist, but the nice thing about this is that it is an extension of what happens without overloading. With this definition, given _______________________ __________________________ | module X (f,g) where | | module Y where | | | | | | class A a where | | import X | | f :: a -> a | | | | instance A Int where | | instance A Float where | | f = id | | f x = x + 1.0 | | | | | | g x = f x | | h x = g x | ------------------------- -------------------------- we would infer: g::Int (since the context in g's definition has only f:Int) and thus h::Int in Y (since the context in h's definition has only one g::Int). If "h" was defined as "h x = f x" in Y, *then* it would have a polymorphic type (because there are two instances of "f" in Y). Carlos