On 10/2/2014 5:21 PM, oleg@okmij.org wrote:
Given
f2 :: Show a => a -> String f2 x = let instance Show Int where show _ = "one" in show x
what should (f2 (1::Int)) return? One answer is that it should still return "one" -- that is, local instances should sort of form a closure (like local variables in the real closure). That is a good answer, but may lead to unpleasant surprises because the fact of the closure is not at all reflected in the type of the function.
Consider
data T = T f3 :: Show a => a -> String f3 x = let instance Show T where show _ = "T" in show x
and take the closure semantics. The type says that to make (f3 T) well-typed, there has to be an instance Show T in scope. The user of f3 has no way to know of the private local instance that is closed over (short of examining the source code). Since the user knows there is no global instance T, the user attempts to define in. The user will be quite surprised to discover that (f3 T) is well-typed but their global instance Show T has no effect. That is true, but even today one can write overly-constrained expressions that don't actually need these constraints. How is `f3` above any different from foo :: Show a => a -> String foo = const "Fooled you, I didn't need Show after all."
However, one could write a more precise type for `f3` which reflects the fact that a `Show` instance is unnecessary for `T`, as follows
class Foo a where instance Foo T where instance Show a => Foo a where f3 :: Foo a => a -> String
(Of course, this requires OverlappingInstances) In fact, it would be useful to have syntactic sugar for this sort of constraint disjunction, for cases like this. We might even extend GHC's type checker to infer such disjunctions, so that `f3`'s type would be inferred to be `Show a \/ (a ~ T) => a -> String`. Thanks for the in-depth analysis and further reading, Gesh P.S. You might want to change your email client's settings, as you don't seem to be sending In-Reply-To headers, which makes threading horrible.