Hi GHC users, Now that the Glorious New type checker can handle local evidence seamlessly, is it a big implementation burden to extend it to deal with local *type class instances* in addition to local *equality constraints*? For example, you could write this: """ f :: Bool f = id < id where instance Ord (a -> b) where _ `compare` _ = LT """ Not only would this prevent instances from "leaking" into all importing modules, but you could refer to *lexically scoped variables* in the type class instance. This would let programmers implement e.g. implicit configurations in the style of Kieslyov and Shan (http://okmij.org/ftp/Haskell/types.html#Prepose) without any mad hackery to tunnel pointers through the type system. Of course, it could lead to problems. For example: """ newtype MyInt = MyInt { unMyInt :: Int } f :: [Int] -> S.Set Int f xs = S.map unMyInt $ S.toList (map MyInt xs) where instance Ord MyInt where x `compare` y = unMyInt x `compare` unMyInt y g :: [Int] -> S.Set Int g xs = S.map unMyInt $ S.toList (map MyInt xs) where instance Ord MyInt where x `compare` y = unMyInt y `compare` unMyInt x main = do let s1 = f [1, 2] s2 = g [1, 2] print $ s1 == s2 -- prints False! print $ S.toList s1 == s2 -- prints True! """ I don't think this is a big problem. It would be up to the users of this extension to do the Right Thing. As Kieslyov and Shan point out, this extension also kills the principal types property - but so do GADTs. Just add more type signatures! Are there big theoretical problems with this extension, or is it just a lack of engineering effort that has prevented its implementation? Max